SoC的功能驗(yàn)證

隨著設(shè)計(jì)的進(jìn)行，越接近最后的產(chǎn)品，修正一個(gè)設(shè)計(jì)缺陷的成本就會(huì)越高。

不同設(shè)計(jì)階段修正一個(gè)設(shè)計(jì)缺陷所需費(fèi)用示意圖

1.功能驗(yàn)證概述

在IC設(shè)計(jì)與制造領(lǐng)域，通常所說的驗(yàn)證（Verification）和測(cè)試（Test）是兩種不同的事

驗(yàn)證

在設(shè)計(jì)過程中確認(rèn)所設(shè)計(jì)的正確性

通過軟件仿真、硬件模擬和形式驗(yàn)證等方法進(jìn)行

在流片之前要做的。

測(cè)試

檢測(cè)芯片是否存在制造或封裝過程中產(chǎn)生的缺陷。

采用測(cè)試設(shè)備進(jìn)行檢查

功能驗(yàn)證

功能驗(yàn)證一般是指設(shè)計(jì)者通過各種方法比較設(shè)計(jì)完成的電路和設(shè)計(jì)文檔規(guī)定的功能是否一致，保證邏輯設(shè)計(jì)的正確性。

通常不包括面積、功耗等硬件實(shí)現(xiàn)的性能檢測(cè)。

SoC功能驗(yàn)證的挑戰(zhàn)

系統(tǒng)復(fù)雜性提高增加驗(yàn)證難度

設(shè)計(jì)層次提高增加了驗(yàn)證工作量

發(fā)展趨勢(shì)

2.功能驗(yàn)證方法與驗(yàn)證規(guī)劃

仿真為基本出發(fā)點(diǎn)的功能驗(yàn)證方法

功能驗(yàn)證開發(fā)流程制訂驗(yàn)證計(jì)劃

功能驗(yàn)證需求

激勵(lì)產(chǎn)生策略

結(jié)果檢測(cè)策略

驗(yàn)證開發(fā)

提高驗(yàn)證的效率

功能驗(yàn)證開發(fā)流程

3.系統(tǒng)級(jí)功能驗(yàn)證

行為級(jí)功能驗(yàn)證

測(cè)試數(shù)據(jù)控制流，包括初始化和關(guān)閉I/O設(shè)備、驗(yàn)證軟件功能、與外界的通信，等等

性能驗(yàn)證

通過性能驗(yàn)證可以使設(shè)計(jì)者清楚地知道整個(gè)系統(tǒng)的工作速度、功耗等性能方面的指標(biāo)。

協(xié)議驗(yàn)證

根據(jù)總線協(xié)議對(duì)各個(gè)模塊的接口部分進(jìn)行驗(yàn)證

系統(tǒng)級(jí)的測(cè)試平臺(tái)

邊界條件

設(shè)計(jì)的不連續(xù)處

出錯(cuò)的條件

極限情況

系統(tǒng)級(jí)的測(cè)試平臺(tái)標(biāo)準(zhǔn)

性能指標(biāo)

覆蓋率指標(biāo)

4.仿真驗(yàn)證自動(dòng)化

激勵(lì)的生成

直接測(cè)試激勵(lì)：檢測(cè)到測(cè)試者所希望檢測(cè)到的系統(tǒng)缺陷

可以快速、準(zhǔn)確地產(chǎn)生大量的與實(shí)際應(yīng)用一致的輸入向量

隨機(jī)測(cè)試激勵(lì)：

檢測(cè)到測(cè)試者沒有想到的一些系統(tǒng)缺陷帶約束的隨機(jī)測(cè)試激勵(lì)是指在產(chǎn)生隨機(jī)測(cè)試向量時(shí)施加一定的約束，使所產(chǎn)生的隨機(jī)測(cè)試向量滿足一定的設(shè)計(jì)規(guī)則。

帶約束的隨機(jī)激勵(lì)生成的例子

x1和x2為系統(tǒng)的兩個(gè)輸入，它們經(jīng)過獨(dú)熱碼編碼器編碼之后產(chǎn)生與被驗(yàn)證設(shè)計(jì)（DUV）直接相連的輸入

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

這樣產(chǎn)生的隨機(jī)向量就可以保證它們的合法性。

用SystemVerilog語言寫的帶約束隨機(jī)激勵(lì)生成例子

輸入data的數(shù)量限制在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

響應(yīng)的檢查

可視化的波形檢查：直觀，但不適用于復(fù)雜系統(tǒng)設(shè)計(jì)

自動(dòng)比對(duì)檢查：通過相應(yīng)的檢測(cè)模型或驗(yàn)證模型來自動(dòng)完成輸出結(jié)果的比對(duì)

覆蓋率的檢測(cè)

覆蓋率數(shù)據(jù)通常是在多個(gè)仿真中收集的.

覆蓋率的模型由針對(duì)結(jié)構(gòu)覆蓋率（Structural Coverage）和功能覆蓋率（Functional Coverage）兩種目標(biāo)而定義的模型所組成。

可細(xì)化為：

限狀態(tài)機(jī)覆蓋率（FSM Coverage）
表達(dá)式覆蓋率（Expression Coverage）
交叉覆蓋率（Cross Coverage）
斷言覆蓋率（Assertion Coverage）

用SystemVerilog語言寫的覆蓋率檢測(cè)的例子

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.形式驗(yàn)證

形式驗(yàn)證（Formal Verification）

靜態(tài)形式驗(yàn)證（Static Formal Verification）和半形式驗(yàn)證（Semi-Formal Verification）

靜態(tài)形式驗(yàn)證不需要施加激勵(lì)，也不需要通過仿真來驗(yàn)證。目前，SoC設(shè)計(jì)中常用的靜態(tài)形式驗(yàn)證方法是相等性檢查。

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

相等性檢查（Equivalent Check）

對(duì)設(shè)計(jì)進(jìn)行覆蓋率100％的快速驗(yàn)證

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

不需要測(cè)試平臺(tái)和測(cè)試矢量，不需要進(jìn)行仿真

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

半形式驗(yàn)證（Semi-Formal Verification）

仿真和形式驗(yàn)證形結(jié)合，如混合模型檢查（Model Checking）或?qū)傩詸z查（Property Checking）的方法。

6.基于斷言的驗(yàn)證

仿真驗(yàn)證面臨的問題：可觀測(cè)性和可控制性

合適的輸入矢量能夠激活錯(cuò)誤

錯(cuò)誤要能夠以某種預(yù)期的形式輸出

采用斷言描述設(shè)計(jì)的行為，在仿真時(shí)起到監(jiān)控作用，當(dāng)監(jiān)控的屬性出現(xiàn)錯(cuò)誤時(shí)，立刻觸發(fā)錯(cuò)誤的產(chǎn)生，增加了設(shè)計(jì)在仿真時(shí)的可觀測(cè)性問題。

也可以用在形式屬性檢查中作為要驗(yàn)證的屬性。屬性檢查（Property Check）時(shí)，是對(duì)整個(gè)狀態(tài)空間進(jìn)行搜索，能夠控制到每一個(gè)信號(hào)并能指出錯(cuò)誤的具體位置，解決了設(shè)計(jì)驗(yàn)證時(shí)的可控制性和可觀察性問題。

驗(yàn)證實(shí)現(xiàn)所花費(fèi)的時(shí)間與驗(yàn)證的質(zhì)量

斷言的作用

斷言語言及工具的使用

斷言語言

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

SVA（SystemVerilog Assertion）例子

用Verilog實(shí)現(xiàn)的檢查器：

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實(shí)現(xiàn)的檢查器：

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

基于斷言的驗(yàn)證

在屬性檢查中使用斷言

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

在仿真中使用斷言

審核編輯 ：李倩