TURBO51嵌入式微處理器功能驗證

1. 1 背景

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

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

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

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

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

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

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

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

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

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

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

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

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

2 TURBO51的驗證方法

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

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

3 形式驗證

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

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