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

1. 1 背景

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

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

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

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

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

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

這些都成為了結構設計和驗證中的難點(diǎn)問(wèn)題。

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

1. 2 微處理器驗證現狀

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

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

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

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

2 TURBO51的驗證方法

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

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

3 形式驗證

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

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