電子教案soc設計方法與實現(xiàn)-課件第9章

第九章SoC功能驗證郭煒魏繼增郭箏謝憬內容大綱功能驗證概述功能驗證方法與驗證規(guī)劃系統(tǒng)級功能驗證仿真驗證自動化形式驗證基于斷言的驗證內容大綱功能驗證概述功能驗證方法與驗證規(guī)劃系統(tǒng)級功能驗證仿真驗證自動化形式驗證基于斷言的驗證隨著設計的進行，越接近最后的產品，修正一個設計缺陷的成本就會越高不同設計階段修正一個設計缺陷所需費用示意圖驗證的概念在IC設計與制造領域，通常所說的驗證（Verification）和測試（Test）是兩種不同的事驗證在設計過程中確認所設計的正確性通過軟件仿真、硬件模擬和形式驗證等方法進行在流片之前要做的。測試檢測芯片是否存在制造或封裝過程中產生的缺陷。采用測試設備進行檢查功能驗證功能驗證一般是指設計者通過各種方法比較設計完成的電路和設計文檔規(guī)定的功能是否一致，保證邏輯設計的正確性。通常不包括面積、功耗等硬件實現(xiàn)的性能檢測SoC功能驗證的挑戰(zhàn)系統(tǒng)復雜性提高增加驗證難度設計層次提高增加了驗證工作量發(fā)展趨勢：內容大綱功能驗證概述功能驗證方法與驗證規(guī)劃系統(tǒng)級功能驗證仿真驗證自動化形式驗證基于斷言的驗證仿真為基本出發(fā)點的功能驗證方法功能驗證開發(fā)流程制訂驗證計劃功能驗證需求激勵產生策略結果檢測策略驗證開發(fā)提高驗證的效率內容大綱功能驗證概述功能驗證方法與驗證規(guī)劃系統(tǒng)級功能驗證仿真驗證自動化形式驗證基于斷言的驗證系統(tǒng)級功能驗證行為級功能驗證測試數(shù)據(jù)控制流，包括初始化和關閉I/O設備、驗證軟件功能、與外界的通信，等等性能驗證通過性能驗證可以使設計者清楚地知道整個系統(tǒng)的工作速度、功耗等性能方面的指標。協(xié)議驗證根據(jù)總線協(xié)議對各個模塊的接口部分進行驗證系統(tǒng)級驗證系統(tǒng)級的測試平臺邊界條件設計的不連續(xù)處出錯的條件極限情況系統(tǒng)級的測試平臺標準性能指標覆蓋率指標內容大綱功能驗證概述功能驗證方法與驗證規(guī)劃系統(tǒng)級功能驗證仿真驗證自動化形式驗證基于斷言的驗證仿真驗證平臺激勵的生成直接測試激勵：檢測到測試者所希望檢測到的系統(tǒng)缺陷可以快速、準確地產生大量的與實際應用一致的輸入向量隨機測試激勵：檢測到測試者沒有想到的一些系統(tǒng)缺陷帶約束的隨機測試激勵是指在產生隨機測試向量時施加一定的約束，使所產生的隨機測試向量滿足一定的設計規(guī)則。帶約束的隨機激勵生成的例子x1和x2為系統(tǒng)的兩個輸入，它們經過獨熱碼編碼器編碼之后產生與被驗證設計（DUV）直接相連的輸入輸入約束：in[0]+in[1]+in[2]<=1這樣產生的隨機向量就可以保證它們的合法性用SystemVerilog語言寫的帶約束隨機激勵生成例子輸入data的數(shù)量限制在1～1000programautomatictest;

//defineconstraintclassTransaction;

randbit[31:0]src,dst,data[];//Dynamicarray

randcbit[2:0]kind;

//Cyclethroughallkinds

constraintc_len

{

data.size

inside{[1:1000]};}//LimitarraysizeEndclass//instantiationTransactiontr;

//startrandomvectorgenerationinitialbegintr=new();

if(!tr.randomize())$finish;transmit(tr);endendprogram響應的檢查可視化的波形檢查：直觀，但不適用于復雜系統(tǒng)設計自動比對檢查：通過相應的檢測模型或驗證模型來自動完成輸出結果的比對覆蓋率的檢測覆蓋率數(shù)據(jù)通常是在多個仿真中收集的覆蓋率的模型由針對結構覆蓋率（StructuralCoverage）和功能覆蓋率（FunctionalCoverage）兩種目標而定義的模型所組成?？杉毣癁椋合逘顟B(tài)機覆蓋率（FSMCoverage）表達式覆蓋率（ExpressionCoverage）交叉覆蓋率（CrossCoverage）斷言覆蓋率（AssertionCoverage）用SystemVerilog語言寫的覆蓋率檢測的例子programautomatictest(busifc.TBifc);classTransaction;

randbit[31:0]src,dst,data;

randenum{MemRd,MemWr,CsrRd,CsrWr,

IoRd,IoWr,Intr,Nop}

kind;

endclass

covergroupCovKind;

coverpointtr.kind;//Measurecoverage

endgroup

Transactiontr=new();//Instantiatetransaction

CovKind

ck=new(); //Instantiategroup

initialbegin

repeat(32)begin//Runafewcycles

if(!tr.randomize())$finish;

ifc.cb.kind<=tr.kind;//transmittransaction

ifc.cb.data<=tr.data;//intointerface

ck.sample();//Gathercoverage

@ifc.cb;//Waitacycle

end

endendprogram內容大綱功能驗證概述功能驗證方法與驗證規(guī)劃系統(tǒng)級功能驗證仿真驗證自動化形式驗證基于斷言的驗證形式驗證形式驗證（FormalVerification）靜態(tài)形式驗證（StaticFormalVerification）和半形式驗證（Semi-FormalVerification）靜態(tài)形式驗證不需要施加激勵，也不需要通過仿真來驗證。目前，SoC設計中常用的靜態(tài)形式驗證方法是相等性檢查。半形式驗證是一種混合了仿真技術與形式驗證技術的方法。常用的半形式驗證是混合屬性檢查或模型檢查，它將形式驗證的完整性與仿真的速度、靈活性相結合。靜態(tài)形式驗證相等性檢查（EquivalentCheck）對設計進行覆蓋率100％的快速驗證主要是檢查組合邏輯的功能相等性不需要測試平臺和測試矢量，不需要進行仿真可用于比較RTL與RTL、RTL與門級、門級與門級的功能相等性，被廣泛應用于版圖提取的網表與RTL代碼比較，特別是做完ECO后要進行網表和修改后的RTL的相等性檢查。半形式驗證半形式驗證（Semi-FormalVerification）仿真和形式驗證形結合，如混合模型檢查（ModelChecking）或屬性檢查（PropertyChecking）的方法。內容大綱功能驗證概述功能驗證方法與驗證規(guī)劃系統(tǒng)級功能驗證仿真驗證自動化形式驗證基于斷言的驗證基于斷言的驗證仿真驗證面臨的問題：可觀測性和可控制性合適的輸入矢量能夠激活錯誤錯誤要能夠以某種預期的形式輸出采用斷言描述設計的行為，在仿真時起到監(jiān)控作用，當監(jiān)控的屬性出現(xiàn)錯誤時，立刻觸發(fā)錯誤的產生，增加了設計在仿真時的可觀測性問題。也可以用在形式屬性檢查中作為要驗證的屬性。屬性檢查（PropertyCheck）時，是對整個狀態(tài)空間進行搜索，能夠控制到每一個信號并能指出錯誤的具體位置，解決了設計驗證時的可控制性和可觀察性問題。驗證實現(xiàn)所花費的時間與驗證的質量斷言的作用斷言的作用斷言語言及工具的使用斷言語言CorSystemCSystemVerilogAssertion(SVA)PropertySpecificationLanguage(PSL)(IBM,basedonSugar)OpenVerificationLibrary(OVL)Verilog,VHDLSVA（SystemVerilogAssertion）例子用Verilog實現(xiàn)的檢查器：always@(posedgeA)begin

repeat(1)@(posedgeclk);fork:A_to_Bbegin@(posedgeB)$display(“SUCCESS:Barrivedintime\n”,$time);disableA_to_B;endbeginrepeat(1)@(posedgeclk)@(posedgeB)display(“SUCCESS:Barrivedintime\n”,$time);disableA_to_B;endbeginrepeat(2)@(posedgecl