TURBO51嵌入式微處理器功能驗(yàn)證

1. 1 背景

TURBO51的工程背景是TURBO51嵌入式微處理器結(jié)構(gòu)設(shè)計(jì)上采取經(jīng)時(shí)間考驗(yàn)過的32位機(jī)主流系統(tǒng)結(jié)構(gòu)， 在嚴(yán)格保證對8051 指令集兼容的前提下，通過重新定義其處理器核的系統(tǒng)結(jié)構(gòu)來挖掘處理器結(jié)構(gòu)上的并行性實(shí)現(xiàn)。在傳統(tǒng)8051軟件開發(fā)環(huán)境下實(shí)現(xiàn)本要由更高位寬的32位處理器來完成的工作并完全重用所有現(xiàn)有軟件資源。在 8051指令級(jí)多種尋址方式混合且指令不定長的現(xiàn)實(shí)下實(shí)現(xiàn)了高性能的體系結(jié)構(gòu)， 亂序發(fā)射， 分支預(yù)測， 精確例外處理， 基于猜測的先行預(yù)取，片上一級(jí)指令高速緩存。處理器系統(tǒng)結(jié)構(gòu)的復(fù)雜給驗(yàn)證提出了很高的要求。而且， 由于TURBO51 是作為SoC 的嵌入式處理器核， 是整個(gè)大規(guī)模SOC 的控制核心和用戶接口， 如果嵌入式處理器設(shè)計(jì)中驗(yàn)證不完善或性能達(dá)不到設(shè)計(jì)要求，都會(huì)導(dǎo)致整個(gè)SoC 項(xiàng)目的開發(fā)致命失敗， 因此對嵌入式處理器的驗(yàn)證在SoC 設(shè)計(jì)中是最重要的部分之一。

一切對高性能體系結(jié)構(gòu)的追求都必須首先建立在以設(shè)計(jì)的正確性為前題才是有意義的。TURBO51的驗(yàn)證面臨三個(gè)主要挑戰(zhàn):

( 1)正確性， 所采用的高性能體系結(jié)構(gòu)也是復(fù)雜和高風(fēng)險(xiǎn)的， 只有設(shè)計(jì)正確才會(huì)帶給SoC 性能上的提升。

( 2)兼容性: 相對于傳統(tǒng)8051， 在程序的執(zhí)行過程中，中斷和異常常會(huì)打斷程序的執(zhí)行， 動(dòng)態(tài)流水線的處理器由于指令的動(dòng)態(tài)亂序執(zhí)行， 但又必須對外部程序來說是和完全順序執(zhí)行只存在速度的差別而非結(jié)果的差別， 所以它必須能精確地與順序執(zhí)行條件下的例外結(jié)果保持一致。

( 3)指令和操作數(shù)空間巨大， 尋址方式復(fù)雜:

8051指令集共有111條指令， 有多種尋址方式和不定的指令長度。另外， 8051指令集還將輸入輸出設(shè)備寄存器與體系結(jié)構(gòu)寄存器作為同種寄存器訪問。

這些都成為了結(jié)構(gòu)設(shè)計(jì)和驗(yàn)證中的難點(diǎn)問題。

( 4)驗(yàn)證充分性的衡量: 在驗(yàn)證過程中根據(jù)發(fā)現(xiàn)錯(cuò)誤的性質(zhì)、原因和數(shù)量分布， 評(píng)估正確性程度和調(diào)整下面的驗(yàn)證計(jì)劃，使驗(yàn)證更深入， 實(shí)現(xiàn)設(shè)計(jì)錯(cuò)誤的快速收斂。

1. 2 微處理器驗(yàn)證現(xiàn)狀

目前世界各處理器公司用于功能驗(yàn)證的方式主要是模擬驗(yàn)證， 形式驗(yàn)證， 硬件仿真加速。但總的看來，由于指令集龐大， 比如， 它的完全無錯(cuò)的測試向量的數(shù)量是指令條數(shù)階乘及每個(gè)操作數(shù)， 地址數(shù)階乘。在有限的時(shí)間很難實(shí)現(xiàn)。除非指令和操作數(shù)的所有兩兩組合都已測試過，否則， 即便經(jīng)過了這些驗(yàn)證， 也只能證明在測試已覆蓋地方正確而不能證明設(shè)計(jì)在任何情況下都正確。

形式驗(yàn)證是指通過數(shù)學(xué)方法證明設(shè)計(jì)的完備性， 即這種方法下的樣本空間是測試對象所有可能的狀態(tài)。A rithSMV， * PHDD。由于狀態(tài)樣本空間巨大， 它只用設(shè)計(jì)屬性檢查工具， 目前僅用于局部邏緝驗(yàn)證。

模擬驗(yàn)證: 包括RTL仿真和門級(jí)仿真。這一階段驗(yàn)證的效果很大程度上由測試激勵(lì)和判定模擬結(jié)果的方法決定。在微處理器驗(yàn)證中， 采用匯編語言編寫測試激勵(lì)，運(yùn)行操作系統(tǒng)， 應(yīng)用程序和隨機(jī)生成測試向量。

硬件加速仿真: 為克服模擬仿真驗(yàn)證速度慢的缺點(diǎn)，采用FPGA 的物理原型驗(yàn)證可以在流片前運(yùn)行操作系統(tǒng)和應(yīng)用程序， 進(jìn)一步在系統(tǒng)級(jí)驗(yàn)證正確性。

2 TURBO51的驗(yàn)證方法

TURBO51在設(shè)計(jì)中用到了形式驗(yàn)證、模擬仿真和硬件加速仿真。采用自底向上的子模塊級(jí)驗(yàn)證再自頂向下的宏模塊及系統(tǒng)級(jí)驗(yàn)證的方法。在整個(gè)設(shè)計(jì)過程中，驗(yàn)證與設(shè)計(jì)是一個(gè)整體， TURBO51在進(jìn)行文檔時(shí)序設(shè)計(jì)時(shí)就同時(shí)開始針對正在進(jìn)行的設(shè)計(jì)編寫驗(yàn)證計(jì)劃， 設(shè)計(jì)和驗(yàn)證的工作在設(shè)計(jì)文檔和驗(yàn)證計(jì)劃中進(jìn)行精確到每個(gè)時(shí)鐘周期的行為描述和變量定義開始，是整個(gè)設(shè)計(jì)和驗(yàn)證最重要的部分。由于TURBO51的設(shè)計(jì)要保證對傳統(tǒng)8051指令集的后向兼容， TURBO51采用兩臺(tái)可進(jìn)行單步調(diào)試的8051硬件仿真器，兩片傳統(tǒng)8051， 兩片采用了簡單流水結(jié)構(gòu)的改進(jìn)版8051 作為正確標(biāo)尺。測試激勵(lì)在此先逐一運(yùn)行，并將其運(yùn)行結(jié)果作為界定執(zhí)行正確和兼容正確的標(biāo)準(zhǔn)。每個(gè)模塊在每個(gè)時(shí)鐘周期的每個(gè)寄存器讀寫和各個(gè)設(shè)計(jì)階段的驗(yàn)證方法， 驗(yàn)證結(jié)果，問題分布， 驗(yàn)證策略在此規(guī)定， 并手工編寫測試程序進(jìn)行仿真。在驗(yàn)證文檔中記錄如何判定設(shè)計(jì)正確的與嚴(yán)重設(shè)計(jì)漏洞及原因，并在設(shè)計(jì)文檔中記錄哪些臨界態(tài)已考慮過了， 為以后懷疑某種情況下有沒有可能是此出錯(cuò)提供重要依據(jù)。在TURBO51的設(shè)計(jì)中覆蓋率指標(biāo)在文檔階段已經(jīng)引入，每個(gè)設(shè)計(jì)了的邏輯一定要用測試來證明有必要這樣設(shè)計(jì)和功能正確。功能設(shè)計(jì)中每個(gè)條件判斷總能在測試文檔中找到測這個(gè)條件的方法及判對標(biāo)準(zhǔn)。很多時(shí)候在寫測試方法時(shí)發(fā)現(xiàn)了很多設(shè)計(jì)中沒有考慮過的情況。功能設(shè)計(jì)文檔和以覆蓋率為指導(dǎo)的驗(yàn)證文檔相互作用，使TURBO51在開始RTL之前就己經(jīng)完成了時(shí)序設(shè)計(jì)， 寄存器定義及全部塊級(jí)測試的完全覆蓋，比如在寄存器重命名中多種尋地方式下對同一物理地址寫入的重命名， 亂序發(fā)射， 精確例外。一般說來，越是文檔級(jí)描述的錯(cuò)誤越容易修改， 越是硬件級(jí)的錯(cuò)誤越難于發(fā)現(xiàn)，修改量很大且容易引入其他錯(cuò)誤。

這個(gè)階段可以較容易用排列組合等進(jìn)行形式驗(yàn)證進(jìn)行完全的情況覆蓋， 排除了絕大部分嚴(yán)重錯(cuò)誤，而且用于仿真的手工編寫的測試程序也用于此后的驗(yàn)證中。RTL不過是文檔的一個(gè)V erilog 描述的翻譯過程， 因此RTL并不是TURBO51設(shè)計(jì)最重要的地方，只是要按功能設(shè)計(jì)文檔和代碼檢查的要求可很快完成，但期間要用綜合結(jié)果指導(dǎo)對流水線負(fù)載平衡并在細(xì)節(jié)上進(jìn)一步調(diào)整， 但每一處與原功能設(shè)計(jì)文檔描述不同的RTL修改首先是修改功能及驗(yàn)證文檔，再次審核通過后才能改動(dòng)RTL 代碼。仿真和RTL編寫是一體的， 在Turbo51 驗(yàn)證中分為模塊、宏模塊、系統(tǒng)級(jí)3個(gè)階段。只有在一個(gè)階段的設(shè)計(jì)和驗(yàn)證及文檔完全達(dá)到計(jì)劃要求，即代碼檢查和代碼覆蓋率后才能再開始下一階段工作， 這樣使得錯(cuò)誤得以快速收斂。這期間把錯(cuò)誤分為高風(fēng)險(xiǎn)區(qū)錯(cuò)誤和低風(fēng)險(xiǎn)區(qū)錯(cuò)誤。出現(xiàn)不正常時(shí)首先從影響程序運(yùn)行走向的高風(fēng)險(xiǎn)區(qū)開始排查，排除高風(fēng)險(xiǎn)區(qū)的錯(cuò)誤后再去找低風(fēng)險(xiǎn)區(qū)錯(cuò)誤。模塊級(jí)RTL 模擬仿真完成后就是宏模塊級(jí)， 指令流水線， LOAD /STORE， Cache等， 再下來是系統(tǒng)級(jí)RTL 仿真。在Turbo51 的設(shè)計(jì)驗(yàn)證中， 只有在TURBO51 整個(gè)的RTL代碼規(guī)范檢驗(yàn)代碼覆蓋率達(dá)到RTL模擬仿真對覆蓋率的要求并通過設(shè)計(jì)描述文檔與驗(yàn)證文檔相結(jié)合的審議通過后才可以再進(jìn)行FPGA 驗(yàn)證。所以TURBO51設(shè)計(jì)驗(yàn)證的底線是在FPGA 硬件原形驗(yàn)證前至少排除全部會(huì)引起死機(jī)或兼容性的這類嚴(yán)重錯(cuò)誤。TURBO51的設(shè)計(jì)驗(yàn)證不是依賴下一階段測試發(fā)現(xiàn)本應(yīng)在上個(gè)階段發(fā)現(xiàn)并解決的錯(cuò)誤，而是只用下階段確認(rèn)上階段目標(biāo)的完成。FPGA 驗(yàn)證的目的是用于測試長時(shí)間在真實(shí)環(huán)境下運(yùn)行應(yīng)用程序， 因?yàn)楫吘购芏鄬ν獠啃盘?hào)的響應(yīng)不易在RTL 仿真中模擬， 而不是用來發(fā)現(xiàn)調(diào)試應(yīng)在仿真中排除的問題。

3 形式驗(yàn)證

形式驗(yàn)證的好處是它能遍歷全部狀態(tài)空間， 可以實(shí)現(xiàn)驗(yàn)證的完備。它在設(shè)計(jì)行為描述規(guī)格書中就開始使用，用于高風(fēng)險(xiǎn)區(qū)的存貯訪問， 高速緩存， 分支預(yù)測， 動(dòng)態(tài)執(zhí)行， 例外處理中最高風(fēng)險(xiǎn)組合的完備性證明。比如在TURBO51 的片內(nèi)一級(jí)指令高速緩存的替換策略設(shè)計(jì)時(shí)，必須要處理每個(gè)可能的狀態(tài)，吞則可能會(huì)出現(xiàn)狀態(tài)機(jī)死鎖。在這里首先就是對是否有且僅有的幾種狀態(tài)進(jìn)行數(shù)學(xué)證明， 然后再開始編寫功能行為描述和驗(yàn)證計(jì)劃。這種方式可以使出錯(cuò)影響大但狀態(tài)空間不大的邏輯達(dá)到完全正確，而且后來的事實(shí)也證明， 通過形式的設(shè)計(jì)在此后的所有測試激勵(lì)下沒有出現(xiàn)異常。

形式驗(yàn)證在TURBO51 驗(yàn)證中的另一個(gè)地方是在進(jìn)行RTL代碼風(fēng)格檢查的時(shí)候用形式驗(yàn)證工具對修改前后的RTL進(jìn)行功能比較， 另外類似的做法也用于物理網(wǎng)表與前端網(wǎng)表的等價(jià)性比較。