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)格保證對(duì)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í)多種尋址方式混合且指令不定長(zhǎng)的現(xiàn)實(shí)下實(shí)現(xiàn)了高性能的體系結(jié)構(gòu)， 亂序發(fā)射， 分支預(yù)測(cè)， 精確例外處理， 基于猜測(cè)的先行預(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ā)致命失敗， 因此對(duì)嵌入式處理器的驗(yàn)證在SoC 設(shè)計(jì)中是最重要的部分之一。

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

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

8051指令集共有111條指令， 有多種尋址方式和不定的指令長(zhǎng)度。另外， 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ò)的測(cè)試向量的數(shù)量是指令條數(shù)階乘及每個(gè)操作數(shù)， 地址數(shù)階乘。在有限的時(shí)間很難實(shí)現(xiàn)。除非指令和操作數(shù)的所有兩兩組合都已測(cè)試過，否則， 即便經(jīng)過了這些驗(yàn)證， 也只能證明在測(cè)試已覆蓋地方正確而不能證明設(shè)計(jì)在任何情況下都正確。

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

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

硬件加速仿真: 為克服模擬仿真驗(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í)開始針對(duì)正在進(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ì)要保證對(duì)傳統(tǒng)8051指令集的后向兼容， TURBO51采用兩臺(tái)可進(jìn)行單步調(diào)試的8051硬件仿真器，兩片傳統(tǒng)8051， 兩片采用了簡(jiǎn)單流水結(jié)構(gòu)的改進(jìn)版8051 作為正確標(biāo)尺。測(cè)試激勵(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ī)定， 并手工編寫測(cè)試程序進(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ì)了的邏輯一定要用測(cè)試來證明有必要這樣設(shè)計(jì)和功能正確。功能設(shè)計(jì)中每個(gè)條件判斷總能在測(cè)試文檔中找到測(cè)這個(gè)條件的方法及判對(duì)標(biāo)準(zhǔn)。很多時(shí)候在寫測(cè)試方法時(shí)發(fā)現(xiàn)了很多設(shè)計(jì)中沒有考慮過的情況。功能設(shè)計(jì)文檔和以覆蓋率為指導(dǎo)的驗(yàn)證文檔相互作用，使TURBO51在開始RTL之前就己經(jīng)完成了時(shí)序設(shè)計(jì)， 寄存器定義及全部塊級(jí)測(cè)試的完全覆蓋，比如在寄存器重命名中多種尋地方式下對(duì)同一物理地址寫入的重命名， 亂序發(fā)射， 精確例外。一般說來，越是文檔級(jí)描述的錯(cuò)誤越容易修改， 越是硬件級(jí)的錯(cuò)誤越難于發(fā)現(xiàn)，修改量很大且容易引入其他錯(cuò)誤。

這個(gè)階段可以較容易用排列組合等進(jìn)行形式驗(yàn)證進(jìn)行完全的情況覆蓋， 排除了絕大部分嚴(yán)重錯(cuò)誤，而且用于仿真的手工編寫的測(cè)試程序也用于此后的驗(yàn)證中。RTL不過是文檔的一個(gè)V erilog 描述的翻譯過程， 因此RTL并不是TURBO51設(shè)計(jì)最重要的地方，只是要按功能設(shè)計(jì)文檔和代碼檢查的要求可很快完成，但期間要用綜合結(jié)果指導(dǎo)對(duì)流水線負(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模擬仿真對(duì)覆蓋率的要求并通過設(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)證不是依賴下一階段測(cè)試發(fā)現(xiàn)本應(yīng)在上個(gè)階段發(fā)現(xiàn)并解決的錯(cuò)誤，而是只用下階段確認(rèn)上階段目標(biāo)的完成。FPGA 驗(yàn)證的目的是用于測(cè)試長(zhǎng)時(shí)間在真實(shí)環(huán)境下運(yùn)行應(yīng)用程序， 因?yàn)楫吘购芏鄬?duì)外部信號(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ù)測(cè)， 動(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ī)死鎖。在這里首先就是對(duì)是否有且僅有的幾種狀態(tài)進(jìn)行數(shù)學(xué)證明， 然后再開始編寫功能行為描述和驗(yàn)證計(jì)劃。這種方式可以使出錯(cuò)影響大但狀態(tài)空間不大的邏輯達(dá)到完全正確，而且后來的事實(shí)也證明， 通過形式的設(shè)計(jì)在此后的所有測(cè)試激勵(lì)下沒有出現(xiàn)異常。

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