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