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

1. 1 背景

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

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

( 1)正確性， 所采用的高性能體系結構也是復雜和高風險的， 只有設計正確才會帶給SoC 性能上的提升。

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

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

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

這些都成為了結構設計和驗證中的難點問題。

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

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

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

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

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

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

2 TURBO51的驗證方法

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

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

3 形式驗證

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

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