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