如何選擇正確的芯片驗(yàn)證方法
加入技術(shù)交流群
3 現(xiàn)有驗(yàn)證技術(shù)及發(fā)展趨勢(shì)
目前可使用的驗(yàn)證方法及技術(shù)如圖2所示。
3.1 動(dòng)態(tài)功能驗(yàn)證
使用最為廣泛的功能驗(yàn)證方法是動(dòng)態(tài)的，之所以被稱為動(dòng)態(tài)是因?yàn)檩斎雸D形/激勵(lì)信號(hào)是在一段時(shí)間(幾個(gè)時(shí)鐘周期)內(nèi)生成并應(yīng)用于設(shè)計(jì)的，相應(yīng)結(jié)果會(huì)被用于與參考/黃金模型進(jìn)行比較，以檢驗(yàn)其與規(guī)范之間的一致性。
仿真器通常用于計(jì)算所有的信號(hào)值，并將其與指定的期望值進(jìn)行比較。目前，有兩類可供選擇的仿真器：
1)基于周期的仿真器：這類仿真器不管在時(shí)鐘周期內(nèi)發(fā)生了什么事情，它只是在每個(gè)周期內(nèi)對(duì)單脈沖信號(hào)進(jìn)行一次求值，由于執(zhí)行時(shí)間很短這類仿真器的速度通常很快。
2)基于事件的仿真器：這類仿真器在時(shí)鐘周期內(nèi)或者在時(shí)鐘邊界捕獲事件，并在設(shè)計(jì)中傳播這些事件，直到系統(tǒng)達(dá)到穩(wěn)態(tài)。
3.2 隨機(jī)/定向功能驗(yàn)證
在一個(gè)有時(shí)間限制的仿真過程中，動(dòng)態(tài)仿真器只能驗(yàn)證芯片的典型行為，而不能驗(yàn)證所有可能的行為，這是動(dòng)態(tài)仿真的主要缺陷。出現(xiàn)這個(gè)問題的主要原因是對(duì)芯片的定向測(cè)試是針對(duì)已知的測(cè)試空間，而不是未知的測(cè)試空間進(jìn)行的。即使是僅對(duì)已知測(cè)試空間的測(cè)試也要花費(fèi)很長(zhǎng)時(shí)間。例如，假設(shè)推出每個(gè)運(yùn)算數(shù)需要一個(gè)時(shí)鐘，為了驗(yàn)證一個(gè)能對(duì)兩個(gè) 32 位操作數(shù)進(jìn)行加和運(yùn)算的簡(jiǎn)單加法器的測(cè)試空間就需要 232x232個(gè)時(shí)鐘周期。隨著邏輯運(yùn)算越來越復(fù)雜，驗(yàn)證空間也會(huì)相應(yīng)增加。因此出現(xiàn)了隨機(jī)動(dòng)態(tài)仿真，通過為設(shè)計(jì)提供隨機(jī)激勵(lì)信號(hào)來增加驗(yàn)證的測(cè)試空間，這樣能夠使驗(yàn)證覆蓋的功能空間最大化。但當(dāng)設(shè)計(jì)規(guī)模很大且非常復(fù)雜時(shí)，隨機(jī)測(cè)試空間會(huì)變得無限。為了解決這個(gè)問題，更高級(jí)的驗(yàn)證語言，如 Open-VERA、E 與SVL (SystemC 驗(yàn)證庫(kù))被推出。這些語言引入了諸如約束隨機(jī)激勵(lì)信號(hào)、隨機(jī)激勵(lì)信號(hào)分配與電抗性測(cè)試平臺(tái)等概念。伴隨著這些語言的運(yùn)用，出現(xiàn)了一些用于對(duì)其進(jìn)行解釋的工具，如VERA、Specman與 OSCI 內(nèi)核( Concentric System Studio ，CCSS)。
除了引入隨機(jī)化功能以外，新的驗(yàn)證語言和工具還通過減少公司在構(gòu)建不同測(cè)試場(chǎng)合/方案所花費(fèi)的時(shí)間，來提高生產(chǎn)率。例如，測(cè)試方案可以采用最高的抽象級(jí)來編寫，并能夠通過采用功能強(qiáng)大的面向?qū)ο笮徒Y(jié)構(gòu)而擴(kuò)展至任何較低的抽象級(jí)。
當(dāng)應(yīng)用動(dòng)態(tài)驗(yàn)證時(shí)，通常需要估計(jì)所覆蓋的、可以量化的功能空間，包括：經(jīng)過驗(yàn)證的代碼行數(shù)(行覆蓋率)，經(jīng)過測(cè)試的邏輯表達(dá)式個(gè)數(shù)(表達(dá)式覆蓋率)，一個(gè) FSM 設(shè)計(jì)中能夠達(dá)到的狀態(tài)數(shù)(FSM 覆蓋率)，在一個(gè)仿真運(yùn)行中可以雙向變換的端口及寄存器數(shù)目(變換覆蓋率)，以及設(shè)計(jì)代碼中覆蓋的邏輯通道數(shù)目(通道覆蓋率)。以上可以使用 Code Coverage 及 Lint 工具來實(shí)現(xiàn)。
3.3 斷言
設(shè)計(jì)者將斷言用作一個(gè)占位符，用來描述與設(shè)計(jì)相關(guān)聯(lián)的假設(shè)及工作特性(包括暫時(shí)的特性)。如果設(shè)計(jì)滿足或未滿足規(guī)范或假設(shè)，則斷言將會(huì)在一個(gè)動(dòng)態(tài)仿真過程中被觸發(fā)。斷言還可在形式/靜態(tài)功能驗(yàn)證環(huán)境中使用。
3.4 混合功能驗(yàn)證
在該方法中通常執(zhí)行動(dòng)態(tài)仿真，仿真結(jié)果被用作靜態(tài)驗(yàn)證的輸入。在靜態(tài)驗(yàn)證過程中，在設(shè)計(jì)中傳播的是邏輯方程式/符號(hào)，而不象在動(dòng)態(tài)仿真中那樣傳遞數(shù)值。這種方法雖然不像形式驗(yàn)證詳盡周全，但卻具有比純動(dòng)態(tài)仿真更高的效率。
3.5 靜態(tài)功能驗(yàn)證
在靜態(tài)功能驗(yàn)證中，不向設(shè)計(jì)施加輸入激勵(lì)，而是將設(shè)計(jì)映射在一個(gè)圖形結(jié)構(gòu)中，用雙擇判決圖(BDD)或其他數(shù)學(xué)表示方法來描述所有時(shí)間周期內(nèi)的設(shè)計(jì)功能。利用這種圖形結(jié)構(gòu)來證實(shí)或反駁屬性可以驗(yàn)證這些數(shù)學(xué)表達(dá)式，這是通過順著或逆著信號(hào)流來傳遞數(shù)值，以確定數(shù)學(xué)結(jié)構(gòu)中的矛盾式來完成的。
現(xiàn)有的工具通過以下兩種方式來滿足靜態(tài)驗(yàn)證市場(chǎng)的需求：
1) 使用斷言：這是在模型/設(shè)計(jì)當(dāng)中規(guī)范并公式化的設(shè)計(jì)約束(使用SystemVerilog、Open-VERA、Verilog和VHDL等設(shè)計(jì)/驗(yàn)證語言)。
2) 使用屬性：這允許使用屬性語言(如PSL和Sugar)對(duì)屬性進(jìn)行規(guī)范。
3.6 等效性驗(yàn)證
為了確認(rèn)門級(jí)表示法與HDL實(shí)現(xiàn)是相同的，需要實(shí)施等效性檢驗(yàn)，使用匹配點(diǎn)并比較這些匹配點(diǎn)之間的邏輯。檢驗(yàn)中會(huì)生成一個(gè)數(shù)據(jù)結(jié)構(gòu)并比較在相同的輸入模式下得出的輸出數(shù)值模式，如果這些輸出數(shù)值模式不相同，那么表示法(這里指門級(jí)和RTL級(jí))就不是等效的。當(dāng)表示法中的一個(gè)經(jīng)過了某種類型的變換時(shí)，等效性檢驗(yàn)有時(shí)會(huì)在兩個(gè)門級(jí)網(wǎng)表或兩個(gè)RTL級(jí)實(shí)現(xiàn)之間進(jìn)行。
造成設(shè)計(jì)表達(dá)式差異的一些實(shí)際原因包括：
1) 綜合算法／探索式方法：根據(jù)對(duì)綜合工具的約束條件(區(qū)域、時(shí)間、功率)不同，綜合工具會(huì)對(duì)邏輯運(yùn)算進(jìn)行優(yōu)化，以得到適當(dāng)?shù)拈T級(jí)表式。為此，綜合工具將采用探索式方法和邏輯最小化算法。
2) 抽象級(jí)：在采用HDL來實(shí)現(xiàn)設(shè)計(jì)時(shí)，由于語言的局限性或是缺乏(不具備)對(duì)綜合工具如何解釋特定語言結(jié)構(gòu)并將其變換為門級(jí)表式的預(yù)測(cè)能力，因此，HDL實(shí)現(xiàn)有可能與設(shè)計(jì)者意圖存在一定的差異。
評(píng)論