基于斷言語言SVA的設計驗證方法

摘 要:基于斷言SVA的驗證是一種有價值的主流驗證技術。斷言特別適合于描述時序特性和因果特性。作為System Verilog的重要組成部分，SVA提供了豐富的斷言指令，能有效地提高驗證測試工作的質量和效率。在此，首先介紹斷言驗證語言SVA，通過與Verilog驗證對比，說明SVA在時序特性和因果特性驗證上的優勢，證明基于斷言的驗證是SoC設計驗證的一種有效方法，能夠有效地提高驗證效率。

關鍵詞:驗證方法; SVA; 時序特性; 因果特性

中圖分類號:TN710 文獻標識碼:A

文章編號:1004-373X(2010)10-0005-03

Verification Method of SVA Language

ZHA Xin

(Shanghai Jiaotong University， Shanghai 200335， China)

Abstract: Verification based on SVA(system verilog assertion) is a valuable mainstream verification technology. SVA is especially propitious to the description of time-sequence characteristics and causality. As an important part of SystemVerilog， SVA which can effectively improve the quality and efficiency of verification work provides abundant assertion instructions. In this paper， the assertion language SVA is introduced， and an example verified by Verilog and SVA is provided to describe the preponderance of SVA in time-sequence characteristics and causality. It proves that SVA verification is a effective method for SoC design verification， and can improve the verification efficiency.

Keywords: verification; method; SVA; time-sequence charouteristic; causal property

0 引 言

隨著芯片設計規模的不斷擴大，以及設計復雜度的上升，SoC設計技術已經成為一種發展趨勢。根據Collett國際公司2003年的調查，造成芯片流片失敗的原因有很多，其中大約有70%的原因是來自于SoC設計本身的功能驗證不足[1]。

SoC設計需要面對的瓶頸已不再是設計時間，而是驗證時間，驗證工作已經占到了整個項目工作量的70%以上，保證芯片功能的正確性已成為SoC和ASIC設計中的最大挑戰。同時，也出現了許多新的驗證方法和理論，如基于斷言的驗證、覆蓋率導向的驗證、可約束的隨機激勵、事務級驗證等[2-5]。其中，基于斷言的驗證是硬件設計功能驗證的一種有效方法。

作為一種對設計對象的屬性或行為特性的描述，斷言并不是新的概念。隨著硬件描述語言應用于硬件設計，斷言的方法也被引入設計驗證當中。VHDL語言中的關鍵詞Assert使設計者可以在代碼中方便地加入斷言;各種新的驗證語言，如Vera，PSL以及SystemVerilog對斷言都有更好的支持[3，6-7]。隨著硬件描述語言Verilog的廣泛應用，SVA(system verilog assertion)在設計驗證中越來越被重視和應用。另外，各種仿真工具對Verilog和System Verilog的支持，尤其是斷言在形式驗證中的應用，使基于斷言語言SVA的驗證方法在設計驗證中發揮了越來越重要的作用。

1 基于斷言語言SVA的驗證方法

1.1 斷言語言SVA

Accellera委員會已經將Systerm Verilog 3.1定為一個標準，斷言語言被納入System Verilog，成為標準的一部分，即SVA。SVA允許把斷言應用到設計中的一系列工具，它具有豐富的語法，可在序列和斷言中支持時間概念。設計者可以對硬件的期待進行編碼，可以創建對硬件功能設計的詳細驗證。

對于一個設計模型的功能，可以用多個可能的邏輯事件之組合來表達。這些事件可以是在同一個時鐘周期邊緣被求值，也可以經過多個時鐘周期之后求值。SVA中用序列對時態行為邏輯事件組合進行仿真。序列是一個以時間為序的布爾表達式列表。用關鍵詞:“sequence”來定義。對于復雜的有序行為，可以在屬性(property)的定義中描述。在property的定義中，可以將多個序列邏輯或時序地組合起來生成更復雜的序列，以表達復雜的有序行為[8]。

序列sequence的語法格式如下:

sequence names;

;

endsequence

屬性property的語法格式如下:

property namep;

;or

;

endproperty

屬性是仿真過程中被檢驗的單元，它必須在仿真過程中用斷言來發揮作用。SVA提供關鍵詞“assert”來檢查屬性。建立屬性并對其斷言的步驟如圖1所示。

圖1 建立屬性并對其斷言的步驟

SVA中有2類斷言:實時斷言和并發斷言。實時斷言遵循仿真事件執行時的語義，它們是帶有System Verilog關鍵詞Assert作為前導的Verilog過程語句。實時斷言在過程仿真中具有立即求值特性;并發斷言使用順序結構描述時態行為，可以在任何位置調用。以下是并發斷言和實時斷言的例子:

Abf:assert property (@posedge clk) not (a b));//并發斷言

Ajs:assert (a b);//實時斷言

關鍵詞property區分并發斷言與實時斷言。

1.2 使用斷言語言SVA驗證的好處

使用斷言的最大好處是為SoC設計驗證提供了良好的可觀察性，可以比較容易地發現潛在電路設計的內部錯誤。傳統的驗證方法是首先產生適當的激勵輸入到DUV(design under verification)中，然后在輸出端口確認數據傳輸的正確性。同時，也存在著這樣一種可能性，即產生的輸入激勵觸發了某種設計漏洞，但這種錯誤并沒有傳遞到設計的輸出端。如果在驗證代碼中嵌入斷言，就可以在更接近產生漏洞的地方將其檢測出來。

另外，斷言SVA驗證提供了良好的可控制性，可以產生多且有效的測試向量，提高電路驗證功能的正確性。在驗證過程中，可以覆蓋電路各種可能發生例外的情況，提高驗證效率。

使用斷言SVA驗證可以對一個給定輸入的設計期望行為進行精確的描述，從而可以更方便地描述輸入/輸出行為、總線協議以及設計中一些復雜的關系。基于斷言的驗證語言，SVA可以使用簡潔的語言結構來建立精確的時序表達式。通過檢查這些表達式是否發生，可以很簡單地進行功能覆蓋的檢查，并且這種覆蓋率分析針對跨多個時序周期的一個時間序列或者整個傳輸。傳統覆蓋分析要專門為覆蓋分析而寫大量的代碼，而斷言的覆蓋分析可以直接使用在協議檢查或者事件描述中用到的時序表達式，因此編碼會更加靈活、簡潔。

2 舉例說明

采用一個簡單的時序為例，通過傳統硬件描述語言Verilog的驗證設計與斷言語言SVA的驗證設計進行比較，說明SVA在驗證中的簡潔、精確描述。

在SoC的設計中，很多模塊都會與memory有數據傳輸，在與memory的bus線上一定有輸入到memory的時鐘信號(如圖2中的spidmack)，以及選擇信號(spidmacs)和讀使能信號(spidmard)。

圖2 時序要求

從圖2所示的波形圖來看，spidmacs和spidmard信號都以spidmack為周期的，并且spidmacs和spidmard都是只有1個時鐘周期，并且在時序上spidmard要比spidmacs晚1個時鐘周期。

用Verilog來設計驗證，首先spidmacs信號和spidamrd信號分別需要一個計數器(cscnt rdcnt)，用以保證spidmacs和spidmard信號的周期數為1。另外需要一個對spidmard的檢測控制信號(csrdctrl)，這個信號是控制spidmard信號是否在spidmacs信號后1個周期產生，并且這個控制信號的時鐘周期數必須為1，這才符合時序要求。最后，需要一個判斷是否有錯的判斷信號(csrderror)。具體設計如下:

reg [1:0] cscnt;

always@(posedge spidmack，posedge rstsva)

begin

if(rstsva) cscnt <= 2′h0;

else if(spidmacs) cscnt <= cscnt + 1′b1;

else if(~spidmacs) cscnt <= 2′h0;

end

cscnt信號是對spidmacs為“1”的計數，如果spidmacs為“0”，cscnt會自動清為0。

Reg [1:0] rdcnt;

always@(posedge spidmack，posedge rstsva)

begin

if(rstsva) rdcnt <= 2′h0;

else if(spidmard)rdcnt <= rdcnt + 1′b1;

else if(~spidmard) rdcnt <= 2′h0;

end

rdcnt信號是對spidmard為“1”的計數，如果spidmard為“0”，rdcnt會自動清為0。

Reg csrdctrl;

always@(posedge spidmack，posedge rstsva)

begin

if(rstsva) csrdctrl <= 1′b0;

else if(spidmacs (~spidmard)) csrdctrl <= 1′b1;

else if((~spidmacs) spidmard) csrdctrl <= 1′b0;

end

csrdctrl信號在spidmacs為“1”且spidmard為“0”時，置為“1”;在spidmacs為“0”且spidmard為“1”時，清為“0”，這個信號是表示從spidmacs為“1”到spidmard為“1”的過程。要確定這個過程的時間間隔是1個周期，這就必須有1個計數器對其進行計數，用計數器的值來判斷是否滿足1個周期的時序要求。計數器設計如下:

reg [1:0] csrdcnt;

always@(posedge spidmack，posedge rstsva)

begin

if(rstsva) csrdcnt<= 2′h0;

else if(csrdctrl) csrdcnt <= csrdcnt + 1′b1;

else if(~csrdctrl) csrdcnt <= 2′h0;

end

要檢測spidmacs和spidmard信號是否符合時序要求，還必須建立查錯機制，也就是檢測錯誤的判斷，設計如下:

reg csrderror;

always@(posedge spidmack，posedge rstsva)

begin

if(rstsva) csrderror <= 1′b0;

else if(spidmacs spidmard) csrderror<= 1′b1;

else if((cscnt == 2′h2) || (rdcnt == 2′h2) ||

(csrdcnt == 2′h2))

csrderror <= 1′b1;

else if(csrderror) csrderror <= 1′b0;

end

從上面verilog的設計可以看出，為了驗證spidmacs和spidmard信號的時序，Verilog用了5個always語句來實現。一旦這2個信號在設計時序上有變動，則在Verilog設計驗證代碼的維護和修改上也將與這5個always語句有關，代碼量是很大的。

基于斷言語言SVA的詳細驗證設計如下:

property pcsrd;

@(posedge spidmack)

MYMrose (spidmacs) |->

(!spidmard) ##1 (spidmard (!spidmacs)) ##1 (!spidmard);

endproperty

acsrd : assert property (pcsrd);

這個屬性描述的是以spidmacs的上升沿為觸發點的。在spidmacs為“1”的同時，spidmard為“0”，1個時鐘周期后，spidmacs為“0”且spidmard為“1”，再1個時鐘周期后spidmard為“0”。SVA提供的斷言字assert，若斷言滿足屬性(property)中的時序要求，則判斷成功，否則判斷失敗。

上述用SVA語言描述在VCS仿真環境下的仿真結果如圖3所示，黑粗線表示上述斷言發生。

圖3 仿真結果

3 仿真結果

從上面的設計比較可以看出，Verilog作為一種過程語言不能很好地控制時序，并且語言的過程性使得測試在同一時間段內發生的并行事件相當困難。隨著檢驗數量的增加，維護代碼將變得很困難，而且Verilog語言沒有提供內嵌的機制來提供功能覆蓋的數據，必須自己設計實現這部分代碼。

SVA是一種描述性語言，可以很好地描述時序相關的狀況，語言描述性本質使的能夠對時間實現卓越的控制。SVA代碼的簡潔實現，使得描述精確，易于維護，且SVA提供內嵌函數來測試特定的設計情況，并且提供了一些構造來自動收集功能覆蓋數據。

4 結 語

基于斷言語言SVA的驗證方法，有著傳統驗證所無法比擬的優勢。SVA對待測模塊信號間時序關系上描述的便利性，大大提高了模塊功能驗證的效率，保證了模塊功能的正確性，提高了被驗證模塊的可觀性和可控性。利用SVA斷言驗證能夠在錯誤發生時將其及時捕獲，允許設計人員迅速明確發生錯誤的設計段落，從而大大簡化了糾錯工作，幫助設計者調整設計，縮短開發周期。

參考文獻

[1]張志敏，傅亮.SoC設計驗證技術發展綜述[EB/OL].[2004-04-06].http://Iib.ict.ac.cn.

[2]丁婷婷，申敏.分層式驗證平臺及覆蓋率技術在SoC上的應用[J].北京電子科技學院學報，2007，15(2):55-57.

[3]馬博，韓俊剛.采用PSL的基于斷言的驗證[J].計算機工程，2007(2):217-219.

[4]劉有耀，韓俊剛.基于事務斷言驗證及SDH芯片驗證平臺[J].微計算機信息，2007，23(14):310-312.

[5]楊弢，羅春，楊軍.基于矢量隨機生成和斷言的LCD控制器的驗證[J].電子工程師，2006(3):4-6.

[6]劉曉，楊軍.基于斷言的SRAM控制器功能驗證[J].電子工程師，2007(2):23-25.

[7]慕長林.斷言驗證技術在VERA中的應用與研究[J].科技資訊，2009(1):20.

[8]VIJAYARAGHAVAN Srikanth， RAMANATHAN Mey-yappan. System Verilog Assertions應用指南[M].陳俊杰，譯.北京:清華大學出版社，2006.

[9]閆沫，張媛.基于System Verilog語言的設計驗證技術[J].現代電子技術，2008，31(6):8-11.

[10]徐中偉，李海波.面向斷言的測試數據生成方法及其應用[J].同濟大學學報:自然科學版，2007(7):659-663.

[11]劉有耀，韓俊剛.屬性說明語言在基于斷言的硬件驗證中的應用[J].微電子學與計算機，2006，23(5):109-111，114.

[12]徐盛，章瑋，金釗.基于斷言的驗證方法在總線協議驗證中的應用[J].電子設計應用，2006(11):88-90.

[13]FOSTER Harry， KROLNIK A， LACEY D. Assertion based design[M]. 2nd ed. New York: Kluwer Academic Publishers， 2004.

[14]勞豐，郭立.斷言語言SVA在硬件功能驗證中的應用[J].電子技術，2008，45(7):45-47.