1  引  言

1. 1  背景

TURBO51的工程背景是TURBO51嵌入式微處理器結(jié)構(gòu)設(shè)計(jì)上采取經(jīng)時(shí)間考驗(yàn)過(guò)的32位機(jī)主流系統(tǒng)結(jié)構(gòu)， 在嚴(yán)格保證對(duì)8051 指令集兼容的前提下，通過(guò)重新定義其處理器核的系統(tǒng)結(jié)構(gòu)來(lái)挖掘處理器結(jié)構(gòu)上的并行性實(shí)現(xiàn)。在傳統(tǒng)8051軟件開(kāi)發(fā)環(huán)境下實(shí)現(xiàn)本要由更高位寬的32位處理器來(lái)完成的工作并完全重用所有現(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)目的開(kāi)發(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í)行過(guò)程中，中斷和異常常會(huì)打斷程序的執(zhí)行， 動(dòng)態(tài)流水線的處理器由于指令的動(dòng)態(tài)亂序執(zhí)行， 但又必須對(duì)外部程序來(lái)說(shuō)是和完全順序執(zhí)行只存在速度的差別而非結(jié)果的差別， 所以它必須能精確地與順序執(zhí)行條件下的例外結(jié)果保持一致。

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

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

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

( 4)驗(yàn)證充分性的衡量: 在驗(yàn)證過(guò)程中根據(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)證， 硬件仿真加速。但總的看來(lái)，由于指令集龐大， 比如， 它的完全無(wú)錯(cuò)的測(cè)試向量的數(shù)量是指令條數(shù)階乘及每個(gè)操作數(shù)， 地址數(shù)階乘。在有限的時(shí)間很難實(shí)現(xiàn)。除非指令和操作數(shù)的所有兩兩組合都已測(cè)試過(guò)，否則， 即便經(jīng)過(guò)了這些驗(yàn)證， 也只能證明在測(cè)試已覆蓋地方正確而不能證明設(shè)計(jì)在任何情況下都正確。

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

模擬驗(yàn)證: 包括RTL仿真和門(mén)級(jí)仿真。這一階段驗(yàn)證的效果很大程度上由測(cè)試激勵(lì)和判定模擬結(jié)果的方法決定。在微處理器驗(yàn)證中， 采用匯編語(yǔ)言編寫(xiě)測(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ì)過(guò)程中，驗(yàn)證與設(shè)計(jì)是一個(gè)整體， TURBO51在進(jìn)行文檔時(shí)序設(shè)計(jì)時(shí)就同時(shí)開(kāi)始針對(duì)正在進(jìn)行的設(shè)計(jì)編寫(xiě)驗(yàn)證計(jì)劃， 設(shè)計(jì)和驗(yàn)證的工作在設(shè)計(jì)文檔和驗(yàn)證計(jì)劃中進(jìn)行精確到每個(gè)時(shí)鐘周期的行為描述和變量定義開(kāi)始，是整個(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è)寄存器讀寫(xiě)和各個(gè)設(shè)計(jì)階段的驗(yàn)證方法， 驗(yàn)證結(jié)果，問(wèn)題分布， 驗(yàn)證策略在此規(guī)定， 并手工編寫(xiě)測(cè)試程序進(jìn)行仿真。在驗(yàn)證文檔中記錄如何判定設(shè)計(jì)正確的與嚴(yán)重設(shè)計(jì)漏洞及原因，并在設(shè)計(jì)文檔中記錄哪些臨界態(tài)已考慮過(guò)了， 為以后懷疑某種情況下有沒(méi)有可能是此出錯(cuò)提供重要依據(jù)。在TURBO51的設(shè)計(jì)中覆蓋率指標(biāo)在文檔階段已經(jīng)引入，每個(gè)設(shè)計(jì)了的邏輯一定要用測(cè)試來(lái)證明有必要這樣設(shè)計(jì)和功能正確。功能設(shè)計(jì)中每個(gè)條件判斷總能在測(cè)試文檔中找到測(cè)這個(gè)條件的方法及判對(duì)標(biāo)準(zhǔn)。很多時(shí)候在寫(xiě)測(cè)試方法時(shí)發(fā)現(xiàn)了很多設(shè)計(jì)中沒(méi)有考慮過(guò)的情況。功能設(shè)計(jì)文檔和以覆蓋率為指導(dǎo)的驗(yàn)證文檔相互作用，使TURBO51在開(kāi)始RTL之前就己經(jīng)完成了時(shí)序設(shè)計(jì)， 寄存器定義及全部塊級(jí)測(cè)試的完全覆蓋，比如在寄存器重命名中多種尋地方式下對(duì)同一物理地址寫(xiě)入的重命名， 亂序發(fā)射， 精確例外。一般說(shuō)來(lái)，越是文檔級(jí)描述的錯(cuò)誤越容易修改， 越是硬件級(jí)的錯(cuò)誤越難于發(fā)現(xiàn)，修改量很大且容易引入其他錯(cuò)誤。

這個(gè)階段可以較容易用排列組合等進(jìn)行形式驗(yàn)證進(jìn)行完全的情況覆蓋， 排除了絕大部分嚴(yán)重錯(cuò)誤，而且用于仿真的手工編寫(xiě)的測(cè)試程序也用于此后的驗(yàn)證中。RTL不過(guò)是文檔的一個(gè)V erilog 描述的翻譯過(guò)程， 因此RTL并不是TURBO51設(shè)計(jì)最重要的地方，只是要按功能設(shè)計(jì)文檔和代碼檢查的要求可很快完成，但期間要用綜合結(jié)果指導(dǎo)對(duì)流水線負(fù)載平衡并在細(xì)節(jié)上進(jìn)一步調(diào)整， 但每一處與原功能設(shè)計(jì)文檔描述不同的RTL修改首先是修改功能及驗(yàn)證文檔，再次審核通過(guò)后才能改動(dòng)RTL 代碼。仿真和RTL編寫(xiě)是一體的， 在Turbo51 驗(yàn)證中分為模塊、宏模塊、系統(tǒng)級(jí)3個(gè)階段。只有在一個(gè)階段的設(shè)計(jì)和驗(yàn)證及文檔完全達(dá)到計(jì)劃要求，即代碼檢查和代碼覆蓋率后才能再開(kāi)始下一階段工作， 這樣使得錯(cuò)誤得以快速收斂。這期間把錯(cuò)誤分為高風(fēng)險(xiǎn)區(qū)錯(cuò)誤和低風(fēng)險(xiǎn)區(qū)錯(cuò)誤。出現(xiàn)不正常時(shí)首先從影響程序運(yùn)行走向的高風(fēng)險(xiǎn)區(qū)開(kāi)始排查，排除高風(fēng)險(xiǎn)區(qū)的錯(cuò)誤后再去找低風(fēng)險(xiǎn)區(qū)錯(cuò)誤。模塊級(jí)RTL 模擬仿真完成后就是宏模塊級(jí)， 指令流水線， LOAD /STORE， Cache等， 再下來(lái)是系統(tǒng)級(jí)RTL 仿真。在Turbo51 的設(shè)計(jì)驗(yàn)證中， 只有在TURBO51 整個(gè)的RTL代碼規(guī)范檢驗(yàn)代碼覆蓋率達(dá)到RTL模擬仿真對(duì)覆蓋率的要求并通過(guò)設(shè)計(jì)描述文檔與驗(yàn)證文檔相結(jié)合的審議通過(guò)后才可以再進(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 仿真中模擬， 而不是用來(lái)發(fā)現(xiàn)調(diào)試應(yīng)在仿真中排除的問(wèn)題。

3  形式驗(yàn)證

形式驗(yàn)證的好處是它能遍歷全部狀態(tài)空間， 可以實(shí)現(xiàn)驗(yàn)證的完備。它在設(shè)計(jì)行為描述規(guī)格書(shū)中就開(kāi)始使用，用于高風(fēng)險(xiǎn)區(qū)的存貯訪問(wèn)， 高速緩存， 分支預(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é)證明， 然后再開(kāi)始編寫(xiě)功能行為描述和驗(yàn)證計(jì)劃。這種方式可以使出錯(cuò)影響大但狀態(tài)空間不大的邏輯達(dá)到完全正確，而且后來(lái)的事實(shí)也證明， 通過(guò)形式的設(shè)計(jì)在此后的所有測(cè)試激勵(lì)下沒(méi)有出現(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à)性比較。

4  RTL模擬仿真和覆蓋率及代碼風(fēng)格檢查

4. 1  RTL仿真

在功能時(shí)序文檔和制定RTL 模擬仿真計(jì)劃時(shí)，RTL編寫(xiě)和模擬仿真在每個(gè)子模塊， 宏模塊， 系統(tǒng)級(jí)設(shè)計(jì)功能行為描述和驗(yàn)證計(jì)劃完成后才開(kāi)始， 每個(gè)子模塊RTL編碼完成后放入用行為級(jí)描述的模型進(jìn)行仿真， 再用EDA 工具提供的代碼檢查工具作RTL代碼檢查， 再仿真直到達(dá)到代碼覆蓋率， 然后層層向上做宏模塊和系統(tǒng)級(jí)的RTL 代碼檢查和基于代碼覆蓋率的仿真。驗(yàn)證的主要排錯(cuò)和測(cè)試在這個(gè)階段進(jìn)行， 包括檢查是否與8051標(biāo)準(zhǔn)完全兼容的驗(yàn)證， 高風(fēng)險(xiǎn)區(qū)的驗(yàn)證和運(yùn)行操作系統(tǒng)及應(yīng)用程序。

這里面使用了兩個(gè)標(biāo)準(zhǔn)， 即由EDA工具給出的測(cè)試激勵(lì)對(duì)已設(shè)計(jì)邏輯的代碼覆蓋率和自己定義的臨界功能覆蓋率。

在模擬仿真中， 對(duì)臨界指令組合采用手工匯編語(yǔ)言編寫(xiě)激勵(lì)。在兼容性測(cè)試中， 包括指令集測(cè)試，位尋址空間遍歷，上電測(cè)值測(cè)試， 寄存器文件讀寫(xiě)遍歷， LS變量RAM 遍歷， 代碼空間分頁(yè)切換，中斷控制， 8051標(biāo)準(zhǔn)外設(shè)， 定計(jì)， IO， 擴(kuò)展外設(shè)驗(yàn)證， SOC 總線讀寫(xiě)， PWM 脈寬調(diào)制， 在線程序燒入， 基礎(chǔ)應(yīng)用:

軟件I2C讀寫(xiě)， 從外部讀取64KB 數(shù)據(jù)和系統(tǒng)測(cè)試，基于操作系統(tǒng)的遙控按鍵解碼和對(duì)片上其它器件的參數(shù)讀取。在此期間使用閃存的仿真模型，對(duì)于指令集測(cè)試， 在現(xiàn)有商用軟件開(kāi)發(fā)環(huán)境下創(chuàng)建測(cè)試激勵(lì)， 對(duì)全部111條指令， 按 標(biāo)準(zhǔn)8051手冊(cè)上對(duì)每條指令的執(zhí)行結(jié)果值， 按分支目標(biāo)， 分支方向， 對(duì)標(biāo)識(shí)位的影響這幾個(gè)方面進(jìn)行測(cè)試。先在基準(zhǔn)平臺(tái)上進(jìn)行單步運(yùn)行，記下每條指令的每種狀態(tài)值， 再將這些值作為正確依據(jù)， 執(zhí)行完一項(xiàng)比較一項(xiàng)結(jié)果， 如相同就繼續(xù)向前， 同時(shí)一條IO 輸出一個(gè)方波，如不同則進(jìn)入本條指令結(jié)果， 標(biāo)記， 分支的死循環(huán)， 通過(guò)查這個(gè)死循環(huán)地址便可快速定位是錯(cuò)在哪條指令的什么地方， 同時(shí)另一IO輸出另一種方波。此程序先在基準(zhǔn)平臺(tái)運(yùn)行通過(guò)，不進(jìn)死循環(huán)， 再把它轉(zhuǎn)成數(shù)據(jù)文件導(dǎo)入仿真模型。寄存器文件讀寫(xiě)也是依據(jù)8051手冊(cè)， 區(qū)分不同尋址方式對(duì)應(yīng)的寄存器文件。在測(cè)試結(jié)果中，最重要的一個(gè)觀測(cè)點(diǎn)是指令提交地址寄存器， 它記錄了真正的處理器運(yùn)行走向， 只要它未出現(xiàn)異常， 這個(gè)測(cè)試項(xiàng)就認(rèn)為無(wú)嚴(yán)重錯(cuò)誤。RTL模擬在TURBO51中分為測(cè)試激勵(lì)生成， 結(jié)果檢測(cè)和覆蓋率分析三個(gè)部分。TURBO51采用了手工編寫(xiě)臨界條件和基礎(chǔ)測(cè)試程序，通過(guò)后再運(yùn)行實(shí)際應(yīng)用程序和操作系統(tǒng)。此階段完成的標(biāo)準(zhǔn)是對(duì)代碼和功能覆蓋率的檢查。在模塊級(jí)RTL的編寫(xiě)過(guò)程中一邊對(duì)代碼風(fēng)格和仿真測(cè)試覆蓋率進(jìn)行檢查，同時(shí)進(jìn)行綜合以測(cè)試關(guān)鍵路徑對(duì)設(shè)計(jì)時(shí)序的滿足。作為輔助驗(yàn)證， 自動(dòng)指令生成指令庫(kù)， 指令生成控制器生成的測(cè)試激勵(lì)同時(shí)也在一個(gè)行為級(jí)8051指令集模擬器仿真模型中一起運(yùn)行， 逐條進(jìn)行結(jié)果比較， 當(dāng)發(fā)現(xiàn)結(jié)果不一致時(shí)對(duì)指令進(jìn)行記錄，當(dāng)發(fā)現(xiàn)分支不一致時(shí)仿真停止或仿真量到達(dá)一定規(guī)模時(shí)也停止仿真， 供查看代碼覆蓋率用。

4. 2  覆蓋率和代碼風(fēng)格檢查 

基于模擬仿真的驗(yàn)證的困難是無(wú)論采用的測(cè)試激勵(lì)是來(lái)自真實(shí)應(yīng)用還是指令自動(dòng)生成， 都無(wú)法證明整個(gè)處理器不出錯(cuò)。因此TURBO51仿真驗(yàn)證的完成標(biāo)準(zhǔn)是在錯(cuò)誤收斂了的情況下增加更多的測(cè)試向量， 使EDA 工具提供的設(shè)計(jì)邏輯覆蓋率達(dá)到塊級(jí)100%和表達(dá)式級(jí)93% ， 功能覆蓋率達(dá)到100% 。

功能覆蓋率的測(cè)試是設(shè)計(jì)規(guī)格書(shū)中定義的全部行為和驗(yàn)證計(jì)劃的全部臨界點(diǎn)。在進(jìn)行覆蓋率檢查的過(guò)程中，可以得出目前的總覆蓋率和對(duì)一個(gè)模塊中某個(gè)狀態(tài)未被測(cè)試向量覆蓋的邏緝和輸入值， 它指明了漏洞存在， 指導(dǎo)手工編寫(xiě)直接針對(duì)未覆蓋邏緝的測(cè)試。另外代碼覆蓋在TURBO51的設(shè)計(jì)中也被用于排除冗余或重復(fù)的邏輯， 節(jié)省不必要的關(guān)鍵路徑開(kāi)銷和邏輯資源。代碼檢查: 代碼檢查使用EDA 工具所提供的功能。使代碼在綜合中不會(huì)產(chǎn)生異常， 使模擬仿真的結(jié)果與FPGA 不一致。在這里用形式驗(yàn)證工具對(duì)修改后和修改前的代碼進(jìn)行等價(jià)性比較。表1是各大模塊的RTL 仿真代碼覆蓋率， 表2是主要模塊在不同測(cè)試激勵(lì)下的代碼塊覆蓋率和表達(dá)式覆蓋率。均由Cadence Incisive 給出。

表1  主要模塊代碼測(cè)式覆概率。

表2  主要模塊在不同的測(cè)試激勵(lì)下的覆蓋率

5  物理原型驗(yàn)證

物理原型驗(yàn)證是AS IC 設(shè)計(jì)中通常采用的另一種重要的驗(yàn)證手段。它是將RTL 描述通過(guò)針對(duì)FPGA目標(biāo)器件的綜合及優(yōu)化， 布局布線及優(yōu)化并同時(shí)進(jìn)行了靜態(tài)時(shí)序分析后形成ASIC 設(shè)計(jì)的另一種物理實(shí)現(xiàn)形式。它能比RTL 模擬仿真更接近真實(shí)的AS IC， 能在系統(tǒng)板上在功能上完全取代ASIC 進(jìn)行工作， 但最高速度一般比ASIC 慢一半以上。在這些都完成并通過(guò)了設(shè)計(jì)描述文檔和驗(yàn)證文檔的審核后進(jìn)行FPGA 硬件加速仿真，完全在系統(tǒng)應(yīng)用環(huán)境下檢驗(yàn)兼容性及正確性并做出初步性能*測(cè)。相對(duì)于仿真而言， 它能在提高系統(tǒng)運(yùn)行速度上提高幾個(gè)數(shù)量級(jí)。

TURBO51的FPGA 驗(yàn)證的前提是設(shè)計(jì)已經(jīng)過(guò)了關(guān)鍵點(diǎn)的形式驗(yàn)證， 完成了塊覆蓋率為100% 的RTL仿真及代碼檢查且錯(cuò)誤已收斂完畢， 故對(duì)FPGA驗(yàn)證的首要目的是通過(guò)運(yùn)行和真實(shí)應(yīng)用環(huán)境完全相同的完整目標(biāo)應(yīng)用系統(tǒng)驗(yàn)證兩步的錯(cuò)誤估計(jì)是否正確并配合其他SOC 模塊作SOC 協(xié)同驗(yàn)證。因?yàn)閷?duì)有的仿真做起來(lái)不方便的系統(tǒng)驗(yàn)證在FPGA 平臺(tái)上很方便驗(yàn)證。在TURBO51的FPGA 驗(yàn)證中， 充分利用了FPGA 上的剩余資源， 用于實(shí)時(shí)定位與監(jiān)測(cè)TURBO51的FPGA 實(shí)現(xiàn)版每個(gè)時(shí)鐘的狀態(tài)及其運(yùn)行狀態(tài)， 這其實(shí)已使原本認(rèn)為FPGA 上難于定位錯(cuò)誤的缺陷大為改觀， 在真實(shí)環(huán)境下運(yùn)行系統(tǒng)提供了非常接近RTL仿真的調(diào)試能力的觀測(cè)窗口。這里依然首先選用了指令提交地址和指令取指地址，累加器， B 寄存器， 程序狀態(tài)字PSW， 重定序緩沖狀態(tài)， 例外處理標(biāo)識(shí)， 寫(xiě)回總線，提交總線位為主要觀察點(diǎn)， 顯示每個(gè)時(shí)鐘的狀態(tài)， 將它們協(xié)同SOC 其它模塊的輸出， 示波器觀測(cè)輸出波形結(jié)果一起形成FPGA 驗(yàn)證結(jié)果。TURBO51在FPGA 驗(yàn)證時(shí)工作在60MH z， 除運(yùn)行全部手工編寫(xiě)的用于模擬仿真的測(cè)試程序外， 還成功連續(xù)兩百小時(shí)運(yùn)行全部現(xiàn)有量產(chǎn)的基于RTOS商用系統(tǒng)及其極限條件， 沒(méi)有發(fā)現(xiàn)嚴(yán)重錯(cuò)誤。通過(guò)對(duì)寄存器值的實(shí)時(shí)監(jiān)測(cè)發(fā)現(xiàn)十處以內(nèi)的外設(shè)非致命錯(cuò)， 比如GPIO 與外設(shè)輸入輸出復(fù)用。

當(dāng)然， 每改一次RTL或監(jiān)視寄存器都需要重新進(jìn)行FPGA 燒寫(xiě)文件的生成， TURBO51耗時(shí)近兩小時(shí)， 故它仍然不可能取代仿真。完成FPGA 驗(yàn)證后做準(zhǔn)備流片的工廠提供的工藝標(biāo)準(zhǔn)單元庫(kù)綜合及靜態(tài)時(shí)序分析， 交出網(wǎng)表做后端布局布線， 完成后再用帶門(mén)延時(shí)的后端門(mén)級(jí)網(wǎng)表進(jìn)行門(mén)級(jí)仿真，最后編寫(xiě)樣片基臺(tái)測(cè)試程序。

6  驗(yàn)證結(jié)果分析

由于最初在制定實(shí)現(xiàn)的方法和制定驗(yàn)證計(jì)劃時(shí)是同步進(jìn)行的， 致使整個(gè)設(shè)計(jì)階段的錯(cuò)誤累積。在TURBO51的設(shè)計(jì)和驗(yàn)證中， 首先用形式驗(yàn)證將最高風(fēng)險(xiǎn)的存貯訪問(wèn)， 高速緩存， 分支預(yù)測(cè)， 動(dòng)態(tài)執(zhí)行， 例外處理中的最高風(fēng)險(xiǎn)組合進(jìn)行完備證明，使錯(cuò)誤得以排除。在此后的驗(yàn)證中， 凡經(jīng)形式驗(yàn)證正確的部分再未出現(xiàn)過(guò)異常， 如圖1所示。

圖1  錯(cuò)誤時(shí)間累計(jì)統(tǒng)計(jì)。

這樣使得全部的高風(fēng)險(xiǎn)錯(cuò)誤在RTL仿真的中期已經(jīng)全部排除并且大多數(shù)都由手工編寫(xiě)的測(cè)試激勵(lì)完成。由于8051指令集指令死角空間相對(duì)較小，手工編寫(xiě)可行。其中大部分RTL 仿真發(fā)現(xiàn)的錯(cuò)是IO設(shè)備錯(cuò)誤與處理器指令執(zhí)行部分無(wú)關(guān)。如圖2所示， 錯(cuò)誤99. 7% 百分比在FPGA 驗(yàn)證前已收斂，故可認(rèn)定前面工作扎實(shí)有效。假如一個(gè)設(shè)計(jì)如果在FPGA 驗(yàn)證階段錯(cuò)誤還未能收斂完， 還能發(fā)現(xiàn)大量新增錯(cuò)誤尤其是嚴(yán)重錯(cuò)誤的話， 這說(shuō)明仿真及行為模型描述與驗(yàn)證計(jì)劃都存在嚴(yán)重問(wèn)題，應(yīng)退回去重走一遍， 否則流片風(fēng)險(xiǎn)較大。

圖2  不同驗(yàn)證階段發(fā)現(xiàn)的錯(cuò)誤分布統(tǒng)計(jì)。

7  總結(jié)和未來(lái)工作

TURBO51嵌入式微處理器使用了上述多種驗(yàn)證方法使得越嚴(yán)重的錯(cuò)誤得到了越早的收斂， 加上高的RTL代碼覆蓋率及長(zhǎng)時(shí)間在FPGA 上成功運(yùn)行了全部目標(biāo)應(yīng)用程序及所有仿真測(cè)試程序， 表明設(shè)計(jì)正確且兼容性完備， 使TURBO51嵌入式微處理器順利采用富士通微電子(日本) 90nmCMOS 工藝一次流片成功。但另一方面， 可配置約束的自動(dòng)隨機(jī)指令序列已在更復(fù)雜的處理器驗(yàn)證中越來(lái)越廣泛地采用， TURBO51的驗(yàn)證中在這一方面目前還處于初級(jí)階段， 這將是以后的主要改進(jìn)方向。