1 引 言
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í)多種尋址方式混合且指令不定長的現(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條指令,， 有多種尋址方式和不定的指令長度,。另外,， 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è)試長時(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à)性比較,。
4 RTL模擬仿真和覆蓋率及代碼風(fēng)格檢查
4. 1 RTL仿真
在功能時(shí)序文檔和制定RTL 模擬仿真計(jì)劃時(shí)，RTL編寫和模擬仿真在每個(gè)子模塊,， 宏模塊,， 系統(tǒng)級(jí)設(shè)計(jì)功能行為描述和驗(yàn)證計(jì)劃完成后才開始， 每個(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ì)臨界指令組合采用手工匯編語言編寫激勵(lì)。在兼容性測(cè)試中,， 包括指令集測(cè)試,，位尋址空間遍歷，上電測(cè)值測(cè)試,， 寄存器文件讀寫遍歷,， LS變量RAM 遍歷， 代碼空間分頁切換,，中斷控制,， 8051標(biāo)準(zhǔn)外設(shè)， 定計(jì),， IO,， 擴(kuò)展外設(shè)驗(yàn)證， SOC 總線讀寫,， PWM 脈寬調(diào)制,， 在線程序燒入， 基礎(chǔ)應(yīng)用:
軟件I2C讀寫,， 從外部讀取64KB 數(shù)據(jù)和系統(tǒng)測(cè)試,，基于操作系統(tǒng)的遙控按鍵解碼和對(duì)片上其它器件的參數(shù)讀取。在此期間使用閃存的仿真模型,，對(duì)于指令集測(cè)試,， 在現(xiàn)有商用軟件開發(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),， 通過查這個(gè)死循環(huán)地址便可快速定位是錯(cuò)在哪條指令的什么地方,， 同時(shí)另一IO輸出另一種方波。此程序先在基準(zhǔn)平臺(tái)運(yùn)行通過,，不進(jìn)死循環(huán),， 再把它轉(zhuǎn)成數(shù)據(jù)文件導(dǎo)入仿真模型。寄存器文件讀寫也是依據(jù)8051手冊(cè),， 區(qū)分不同尋址方式對(duì)應(yīng)的寄存器文件,。在測(cè)試結(jié)果中，最重要的一個(gè)觀測(cè)點(diǎn)是指令提交地址寄存器,， 它記錄了真正的處理器運(yùn)行走向,， 只要它未出現(xiàn)異常， 這個(gè)測(cè)試項(xiàng)就認(rèn)為無嚴(yán)重錯(cuò)誤,。RTL模擬在TURBO51中分為測(cè)試激勵(lì)生成,， 結(jié)果檢測(cè)和覆蓋率分析三個(gè)部分。TURBO51采用了手工編寫臨界條件和基礎(chǔ)測(cè)試程序,，通過后再運(yùn)行實(shí)際應(yīng)用程序和操作系統(tǒng),。此階段完成的標(biāo)準(zhǔn)是對(duì)代碼和功能覆蓋率的檢查。在模塊級(jí)RTL的編寫過程中一邊對(duì)代碼風(fēng)格和仿真測(cè)試覆蓋率進(jìn)行檢查,，同時(shí)進(jìn)行綜合以測(cè)試關(guān)鍵路徑對(duì)設(shè)計(jì)時(shí)序的滿足,。作為輔助驗(yàn)證， 自動(dòng)指令生成指令庫,， 指令生成控制器生成的測(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)證的困難是無論采用的測(cè)試激勵(lì)是來自真實(shí)應(yīng)用還是指令自動(dòng)生成， 都無法證明整個(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ī)格書中定義的全部行為和驗(yàn)證計(jì)劃的全部臨界點(diǎn),。在進(jìn)行覆蓋率檢查的過程中，可以得出目前的總覆蓋率和對(duì)一個(gè)模塊中某個(gè)狀態(tài)未被測(cè)試向量覆蓋的邏緝和輸入值,， 它指明了漏洞存在,， 指導(dǎo)手工編寫直接針對(duì)未覆蓋邏緝的測(cè)試。另外代碼覆蓋在TURBO51的設(shè)計(jì)中也被用于排除冗余或重復(fù)的邏輯,， 節(jié)省不必要的關(guān)鍵路徑開銷和邏輯資源,。代碼檢查: 代碼檢查使用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 描述通過針對(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 慢一半以上,。在這些都完成并通過了設(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ān)鍵點(diǎn)的形式驗(yàn)證,， 完成了塊覆蓋率為100% 的RTL仿真及代碼檢查且錯(cuò)誤已收斂完畢,， 故對(duì)FPGA驗(yàn)證的首要目的是通過運(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ì)有的仿真做起來不方便的系統(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í),， 寫回總線，提交總線位為主要觀察點(diǎn),， 顯示每個(gè)時(shí)鐘的狀態(tài),， 將它們協(xié)同SOC 其它模塊的輸出， 示波器觀測(cè)輸出波形結(jié)果一起形成FPGA 驗(yàn)證結(jié)果,。TURBO51在FPGA 驗(yàn)證時(shí)工作在60MH z,， 除運(yùn)行全部手工編寫的用于模擬仿真的測(cè)試程序外， 還成功連續(xù)兩百小時(shí)運(yùn)行全部現(xiàn)有量產(chǎn)的基于RTOS商用系統(tǒng)及其極限條件,， 沒有發(fā)現(xiàn)嚴(yán)重錯(cuò)誤,。通過對(duì)寄存器值的實(shí)時(shí)監(jiān)測(cè)發(fā)現(xiàn)十處以內(nèi)的外設(shè)非致命錯(cuò)， 比如GPIO 與外設(shè)輸入輸出復(fù)用,。
當(dāng)然,， 每改一次RTL或監(jiān)視寄存器都需要重新進(jìn)行FPGA 燒寫文件的生成， TURBO51耗時(shí)近兩小時(shí),， 故它仍然不可能取代仿真,。完成FPGA 驗(yàn)證后做準(zhǔn)備流片的工廠提供的工藝標(biāo)準(zhǔn)單元庫綜合及靜態(tài)時(shí)序分析， 交出網(wǎng)表做后端布局布線,， 完成后再用帶門延時(shí)的后端門級(jí)網(wǎng)表進(jìn)行門級(jí)仿真,，最后編寫樣片基臺(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)的存貯訪問,， 高速緩存,， 分支預(yù)測(cè)， 動(dòng)態(tài)執(zhí)行,， 例外處理中的最高風(fēng)險(xiǎn)組合進(jìn)行完備證明,，使錯(cuò)誤得以排除。在此后的驗(yàn)證中,， 凡經(jīng)形式驗(yàn)證正確的部分再未出現(xiàn)過異常,， 如圖1所示。
圖1 錯(cuò)誤時(shí)間累計(jì)統(tǒng)計(jì)。
這樣使得全部的高風(fēng)險(xiǎn)錯(cuò)誤在RTL仿真的中期已經(jīng)全部排除并且大多數(shù)都由手工編寫的測(cè)試激勵(lì)完成,。由于8051指令集指令死角空間相對(duì)較小,，手工編寫可行。其中大部分RTL 仿真發(fā)現(xiàn)的錯(cuò)是IO設(shè)備錯(cuò)誤與處理器指令執(zhí)行部分無關(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ò)誤的話， 這說明仿真及行為模型描述與驗(yàn)證計(jì)劃都存在嚴(yán)重問題,，應(yīng)退回去重走一遍,， 否則流片風(fēng)險(xiǎn)較大。
圖2 不同驗(yàn)證階段發(fā)現(xiàn)的錯(cuò)誤分布統(tǒng)計(jì),。
7 總結(jié)和未來工作
TURBO51嵌入式微處理器使用了上述多種驗(yàn)證方法使得越嚴(yán)重的錯(cuò)誤得到了越早的收斂,， 加上高的RTL代碼覆蓋率及長時(shí)間在FPGA 上成功運(yùn)行了全部目標(biāo)應(yīng)用程序及所有仿真測(cè)試程序， 表明設(shè)計(jì)正確且兼容性完備,， 使TURBO51嵌入式微處理器順利采用富士通微電子(日本) 90nmCMOS 工藝一次流片成功,。但另一方面， 可配置約束的自動(dòng)隨機(jī)指令序列已在更復(fù)雜的處理器驗(yàn)證中越來越廣泛地采用,， TURBO51的驗(yàn)證中在這一方面目前還處于初級(jí)階段,， 這將是以后的主要改進(jìn)方向。