隨著設計的進行，越接近最后的產品，修正一個設計缺陷的成本就會越高。

不同設計階段修正一個設計缺陷所需費用示意圖

1.功能驗證概述

在IC設計與制造領域，通常所說的驗證（Verification）和測試（Test）是兩種不同的事

驗證

在設計過程中確認所設計的正確性

通過軟件仿真、硬件模擬和形式驗證等方法進行

在流片之前要做的。

測試

檢測芯片是否存在制造或封裝過程中產生的缺陷。

采用測試設備進行檢查

功能驗證

功能驗證一般是指設計者通過各種方法比較設計完成的電路和設計文檔規定的功能是否一致，保證邏輯設計的正確性。

通常不包括面積、功耗等硬件實現的性能檢測。

SoC功能驗證的挑戰

系統復雜性提高增加驗證難度

設計層次提高增加了驗證工作量

發展趨勢

2.功能驗證方法與驗證規劃

仿真為基本出發點的功能驗證方法

功能驗證開發流程制訂驗證計劃

功能驗證需求

激勵產生策略

結果檢測策略

驗證開發

提高驗證的效率

功能驗證開發流程

3.系統級功能驗證

行為級功能驗證

測試數據控制流，包括初始化和關閉I/O設備、驗證軟件功能、與外界的通信，等等

性能驗證

通過性能驗證可以使設計者清楚地知道整個系統的工作速度、功耗等性能方面的指標。

協議驗證

根據總線協議對各個模塊的接口部分進行驗證

系統級的測試平臺

邊界條件

設計的不連續處

出錯的條件

極限情況

系統級的測試平臺標準

性能指標

覆蓋率指標

4.仿真驗證自動化

激勵的生成

直接測試激勵：檢測到測試者所希望檢測到的系統缺陷

可以快速、準確地產生大量的與實際應用一致的輸入向量

隨機測試激勵：

檢測到測試者沒有想到的一些系統缺陷帶約束的隨機測試激勵是指在產生隨機測試向量時施加一定的約束，使所產生的隨機測試向量滿足一定的設計規則。

帶約束的隨機激勵生成的例子

x1和x2為系統的兩個輸入，它們經過獨熱碼編碼器編碼之后產生與被驗證設計（DUV）直接相連的輸入

輸入約束：in[0] + in[1] + in[2] <= 1

這樣產生的隨機向量就可以保證它們的合法性。

用SystemVerilog語言寫的帶約束隨機激勵生成例子

輸入data的數量限制在1～1000

programautomatictest; //defineconstraint classTransaction; randbit[31:0]src,dst,data[];//Dynamicarray randcbit[2:0]kind;//Cyclethroughallkinds constraintc_len {data.sizeinside{[1:1000]};}//Limitarraysize Endclass //instantiation Transactiontr; //startrandomvectorgeneration initialbegin tr=new(); if(!tr.randomize())$finish; transmit(tr); end endprogram

響應的檢查

可視化的波形檢查：直觀，但不適用于復雜系統設計

自動比對檢查：通過相應的檢測模型或驗證模型來自動完成輸出結果的比對

覆蓋率的檢測

覆蓋率數據通常是在多個仿真中收集的.

覆蓋率的模型由針對結構覆蓋率（Structural Coverage）和功能覆蓋率（Functional Coverage）兩種目標而定義的模型所組成。

可細化為：

限狀態機覆蓋率（FSM Coverage）
表達式覆蓋率（Expression Coverage）
交叉覆蓋率（Cross Coverage）
斷言覆蓋率（Assertion Coverage）

用SystemVerilog語言寫的覆蓋率檢測的例子

programautomatictest(busifc.TBifc); classTransaction; randbit[31:0]src,dst,data; randenum{MemRd,MemWr,CsrRd,CsrWr,I oRd,IoWr,Intr,Nop}kind; endclass covergroupCovKind; coverpointtr.kind;//Measurecoverage endgroup Transactiontr=new();//Instantiatetransaction CovKindck=new();//Instantiategroup initialbegin repeat(32)begin//Runafewcycles if(!tr.randomize())$finish; ifc.cb.kind<=?tr.kind;???//?transmit?transaction???????? ??????ifc.cb.data?<=?tr.data;???//???into?interface???????? ??????ck.sample();??????????????//?Gather?coverage??????? ??????@ifc.cb;??????????????????//?Wait?a?cycle??????? ???end????? end endprogram

5.形式驗證

形式驗證（Formal Verification）

靜態形式驗證（Static Formal Verification）和半形式驗證（Semi-Formal Verification）

靜態形式驗證不需要施加激勵，也不需要通過仿真來驗證。目前，SoC設計中常用的靜態形式驗證方法是相等性檢查。

半形式驗證是一種混合了仿真技術與形式驗證技術的方法。常用的半形式驗證是混合屬性檢查或模型檢查，它將形式驗證的完整性與仿真的速度、靈活性相結合。

相等性檢查（Equivalent Check）

對設計進行覆蓋率100％的快速驗證

主要是檢查組合邏輯的功能相等性

不需要測試平臺和測試矢量，不需要進行仿真

可用于比較RTL與RTL、RTL與門級、門級與門級的功能相等性，被廣泛應用于版圖提取的網表與RTL代碼比較，特別是做完ECO后要進行網表和修改后的RTL的相等性檢查。

半形式驗證（Semi-Formal Verification）

仿真和形式驗證形結合，如混合模型檢查（Model Checking）或屬性檢查（Property Checking）的方法。

6.基于斷言的驗證

仿真驗證面臨的問題：可觀測性和可控制性

合適的輸入矢量能夠激活錯誤

錯誤要能夠以某種預期的形式輸出

采用斷言描述設計的行為，在仿真時起到監控作用，當監控的屬性出現錯誤時，立刻觸發錯誤的產生，增加了設計在仿真時的可觀測性問題。

也可以用在形式屬性檢查中作為要驗證的屬性。屬性檢查（Property Check）時，是對整個狀態空間進行搜索，能夠控制到每一個信號并能指出錯誤的具體位置，解決了設計驗證時的可控制性和可觀察性問題。

驗證實現所花費的時間與驗證的質量

斷言的作用

斷言語言及工具的使用

斷言語言

C or SystemC
SystemVerilog Assertion (SVA)
Property Specification Language (PSL) (IBM, based on Sugar)
Open Verification Library (OVL)
Verilog, VHDL

SVA（SystemVerilog Assertion）例子

用Verilog實現的檢查器：

always@(posedgeA) beginrepeat(1)@(posedgeclk); fork:A_to_B begin@(posedgeB) $display(“SUCCESS:Barrivedintime ”,$time); disableA_to_B; end begin repeat(1)@(posedgeclk) @(posedgeB) display(“SUCCESS:Barrivedintime ”,$time); disableA_to_B; end begin repeat(2)@(posedgeclk) display(“ERROR:Bdidn’tarriveintime ”,$time); disableA_to_B; end end

用SVA實現的檢查器：

assertproperty (@(posedgeclk)A|->##[1:2]B);

基于斷言的驗證

在屬性檢查中使用斷言

在屬性檢查中，最重要的就是屬性描述。

在仿真中使用斷言

審核編輯 ：李倩