sva 基礎語法

時間 2019-11-10

標籤 sva 基礎語法简体版

原文原文鏈接

斷言assertion被放在verilog設計中，方便在仿真時查看異常狀況。當異常出現時，斷言會報警。通常在數字電路設計中都要加入斷言，斷言佔整個設計的比例應很多於30%。如下是斷言的語法：編程

1. SVA的插入位置：在一個.v文件中：

module ABC ();

rtl 代碼

SVA斷言

endmodule

注意：不要將SVA寫在enmodule外面。

2. 斷言編寫的通常格式是：

【例】斷言名稱1：assert property(事件1) //沒有分號

$display("........",$time); //有分號

else

$display("........",$time); //有分號

斷言名稱2：assert property(事件2)

$display("........",$time);

else

$display("........",$time);

斷言的目的是：判定「事件1」和「事件2」會發生，若是發生了，就記錄爲pass，若是沒發生，就記錄爲fail。注意：上例中沒有if，只有else，斷言自己就充當if的做用。

上例中，事件1和事件2能夠用兩種方式來寫：

(1) 序列塊： sequence name;

。。。。。。。。。;

endsequence

(2) 屬性塊： property name;

。。。。。。。。。;

endsequence

從定義來說，sequence塊用於定義一個事件（磚），而property塊用於將事件組織起來，造成更復雜的一個過程（樓）。sequence塊的內容不能爲空，你寫亂字符都行，但不能什麼都沒有。sequence也能夠包含另外一個sequence, 如：

sequence s1;

s2(a,b);

endsequence //s1和s2都是sequence塊

sequence塊和property塊都有name，使用assert調用時都是：「assert property(name);」

在SVA中，sequence塊通常用來定義組合邏輯斷言，而property通常用來定義一個有時間觀念的斷言，它會經常調用sequence，一些時序操做如「|->」只能用於property就是這個緣由。

注：如下介紹的SVA語法，既能夠寫在sequence中，也能夠寫在property中，語法是通用的。

3. 帶參數的property、帶參數的sequence

property也能夠帶參數，參數能夠是事件或信號，調用時寫成：assert property (p1(a,b))

被主sequence調用的從sequence也能帶參數，例如從sequence名字叫s2，主sequence名字叫s1:

sequence s1;

s2(a,b);

endsequence

4. property內部能夠定義局部變量，像正常的程序同樣。

property p1;

int cnt;

.....................

endproperty

【注】在介紹語法以前，先強調寫斷言的通常格式：

通常，斷言是基於時序邏輯的，單純進行組合邏輯的斷言不多見，由於太費內存（時序邏輯是每一個時鐘週期判斷一次，而組合邏輯倒是每一個時鐘週期內判斷屢次，內存吃不消）。

所以，寫斷言的通常規則是： time + event，要判定發生什麼event，首先要指定發生event的時間，例如

每一個時鐘上升沿 + 發生某事

某信號降低時 + 發生某事

5. 語法1：信號（或事件）間的「組合邏輯」關係：

(1) 常見的有：&&, ||, !, ^

(2) a和b哪一個成立都行，但若是都成立，就認爲是a成立：firstmatch(a||b)，與「||」基本相同，不一樣點是當a和b都成立時，認爲a成立。

(3) a ? b:c ———— a事件成功後，觸發b，a不成功則觸發c

6. 語法2：在「時序邏輯」中判斷獨立的一根信號的行爲：

@ (posedge clk) A事件; ———— 當clk上升沿時，若是發生A事件，斷言將報警。

邊沿觸發內置函數：(假設存在一個信號a)

$rose( a );———— 信號上升

$fell( a );———— 信號降低

$stable( a );———— 信號值不變

7. 語法3：在「時序邏輯」中判斷多個事件/信號的行爲關係：

(1) intersect(a,b)———— 判定a和b兩個事件同時產生，且同時結束。

(2) a within b ———— 判定b事件發生的時間段裏包含a事件發生的時間段。

(3) a ##2 b ———— 判定a事件發生後2個單位時間內b事件必定會發生。

a ##[1:3] b ———— 判定a事件發生後1~3個單位時間內b事件必定會發生。

a ##[3:$] b ———— 判定a事件發生後3個週期時間後b事件必定會發生。

(4) c throughout (a ##2 b) ———— 判定在a事件成立到b事件成立的過程當中，c事件「一直」成立。

(5) @ (posedge clk) a |-> b ———— 判定clk上升沿後，a事件「開始發生」，同時，b事件發生。

(6) @ (posedge clk) a.end |-> b ———— 判定clk上升沿後，a事件執行了一段時間「結束」後，同時，b事件發生。

注："a |-> b" 在邏輯上是一個判斷句式，即：

if a

else

succeed;

所以，一旦 a 發生，b 必須發生，斷言才成功。若是a沒發生，走else，一樣成功。

(7) @ (posedge clk) a |=> b ———— 判定clk上升沿後，a事件開始發生，下一個時鐘沿後，b事件開始發生。

(8) @ (posedge clk) a |=>##2b ———— 判定clk上升沿後，a事件開始發生，下三個時鐘沿後，b事件開始發生。

(9) @ (posedge clk) $past(a,2) == 1'b1 ———— 判定a信號在2個時鐘週期「之前」，其電平值是1。

(10) @ (posedge clk) a [*3] ———— 判定「@ (posedge clk) a」在連續3個時鐘週期內都成立。

@ (posedge clk) a [*1:3] ———— 判定「@ (posedge clk) a」在連續1~3個時鐘週期內都成立。

@ (posedge clk) a [->3] ———— 判定「@ (posedge clk) a」在非連續的3個時鐘週期內都成立。

舉一個複雜點的例子：

property ABC;

int tmp;

@(posedge clk) ($rose(a),tmp = b) |-> ##4 (c == (tmp*tmp+1)) ##3 d[*3];

endproperty

上例的一個property說明：當clk上升沿時，斷言開始。首先判定信號a由低變高，將此時的信號b的值賦給變量tmp，4個時鐘週期後，判定信號c的值是4個週期前b^2+1，再過3個週期，判定信號d必定會起來，再過3個週期，信號d又起來一次。。。。。。。只有這些判定都成功，該句斷言成功。otherwise，信號a從一開始就沒起來，則斷言也成功。

8. 語法4：多時鐘域聯合斷言：一句斷言能夠表示多個時鐘域的信號關係，例如：

@ （posedge clk1） a |-> ##1 @ (posedge clk2) b

當clk1上升沿時，事件a發生，緊接着若是過來第二個時鐘clk2的上升沿，則b發生。「##1」在跨時鐘時不表示一個時鐘週期，只表示等待最近的一個跨時鐘事件。因此此處不能寫成##2或其餘。可是能夠寫成：

@ （posedge clk1） a |=> @ (posedge clk2) b

9. 語法5：總線的斷言函數

總線就是好多根bit線，共同表示一個數。SVA提供了多bit狀態一塊兒判斷的函數，即總線斷言函數：

(1) $onehot(BUS) ————BUS中有且僅有1 bit是高，其餘是低。

(2) $onehot0(BUS) ————BUS中有不超過1 bit是高，也容許全0。

(3) $isunknown(BUS) ————BUS中存在高阻態或未知態。

(4) countones(BUS)==n ————BUS中有且僅有n bits是高，其餘是低。

10. 語法6：屏蔽不定態

當信號被斷言時，若是信號是未復位的不定態，無論怎麼斷言，都會報告：「斷言失敗」，爲了在不定態不報告問題，在斷言時能夠屏蔽。

如： @(posedge clk) (q == $past(d))，當未復位時報錯，屏蔽方法是將該句改寫爲：

@(posedge clk) disable iff (!rst_n) (q == $past(d)) //rst是低電平有效

10. 語法6：斷言覆蓋率檢測：

name: cover property (func_name)

11. 在modelsim中開啓斷言編譯和顯示功能：

（1）【編譯verilog代碼時按照system verilog進行編譯】 vlog -sv abc.v

（2）【仿真命令加一個-assertdebug】 vsim -assertdebug -novopt testbench

（3）【若是想看斷言成功與否的分析，使用打開斷言窗口的命令】 view assertions

12. 在VCS中加入斷言編譯和顯示功能：

在fsdb文件中加一句話：$fsdbDumpSVA

在VCS編譯參數：system "vcs $VCS_SIMULATION" 中加入一些options:

-assert enable_diag\

-assert vpiSeqBeginTime\

-assert vpiSeqFail\

-assert report=路徑\

-assert finish_maxfail=100

***********************************************************************************************

【經驗】如下是一些編寫斷言的經驗：

1. 斷言的目的：傳統的驗證方法是經過加激勵，觀察輸出。這種方法對案例的依賴嚴重，案例設計很差，問題不便於暴露。而斷言是伴隨RTL代碼的，不依賴測試案例，而是相對「靜態」。例如：咱們要測試一個串行數據讀寫單元，數據線只有一根，先傳四位地址，再傳數據。

（1）案例驗證法：寫一個地址，再寫一段數據，而後讀取該地址，看輸出的是否是剛纔寫的數據。

（2）斷言法：不須要專門設計地址和數據，當發起寫時，在地址傳輸的時間裏將地址存儲到一個變量裏，在數據傳輸的時間裏將數據存儲到一個變量裏，觀察RAM中該地址是否存在該數據就能夠了。

斷言設計至關於在電腦上把RTL實現的功能再實現一遍。

2. 斷言中能夠包含function和task。並且function常常用於斷言，由於有的處理很複雜，而斷言又是「一句式」的，沒法分紅好幾句進行表達，因此須要function替斷言分擔工做。

3. 斷言容許規定同時發生的事件，就是組合邏輯，你能夠寫成：a && b，也能夠寫成 a ##0 b，不能寫 ##0.5，不支持小數。

4. 斷言是用電腦模仿RTL的運行過程，當RTL功能複雜時，你必須用到變量。斷言中支持C語言的int和數組聲明，但在賦值時「不能」寫成：##4 var = Signal，其中var是斷言中的變量，和RTL無關，Signal是RTL中的一個信號。本句是想在第4週期將Signal的值賦給var，以便在後面使用該值。但本句只有變量賦值，沒有對RTL信號的任何斷言，就會報錯，解決方法是：##4 (「廢話」，var = Signal)，必定要有斷言的話咱們就寫「廢話」，例如:data == data 等。若是有多個變量要賦值也能夠，##4 （廢話，變量1賦值，變量2賦值...........）

5. 關於斷言的表達風格：語法介紹的「a |-> b」，其實是「if a, then b」的邏輯，當a不發生，b也不會被判斷，該斷言天然成功。但當咱們的邏輯是

if a1

{

if a2

then b

}

該如何用斷言表達？？？？或許能夠寫成：「a1 |-> a2 |-> b」，也能夠，但經常使用的表達是：

「a1 && a2 |-> b」或者「a1 ##3 a2 |-> b」

6. 關於斷言的時序：時序邏輯的斷言須要注意的一個問題：

例如：假設當clk上升沿到來時，b<=a。將上述邏輯寫成斷言時，若是寫成「@(posedge clk) b==a」，看起來和 b<=a同樣，但其實是錯的。由於當時鐘上升時，b尚未獲得a的值，a還須要一段保持時間。即，斷言中的信號值其實是時鐘沿到來以前的值，而不是時鐘沿到來後他們將要編程的值。因此，b<=a邏輯的斷言應該是：「@ (posedge clk) (a==a,tmp=a) |=> (b==tmp);」

針對上述幾點，舉一個複雜的例子：

斷言wr的功能是檢查串行地址輸入是否正確，串行地址輸入線是 DataIn 。$time返回值以0.1ns爲單位（由於我在testbench中的單位規定是`timescale 1ns/100ps，精度是100ps = 0.1ns），因此$time/10纔是ns。

/////////////////////////////////////////////////////////////////////////////

wr: assert property(wr_p)

$display("succeed：",$time/10);

else

$display("error: ",$time/10);

/////////////////////////////////////////////////////////////////////////////

//斷言能夠聲明一個int數組arr[4]，

//「@(posedge clk) !vld_pulse_r[0] && !DataIn」是真實的預備條件

//「##4 (read==read, arr[0] = DataIn)」只是爲了在特定時間內賦值，有用的語句是「arr[0] = DataIn」，//「read==read」是廢話，爲了編譯經過。

//arr賦值完畢後，進入function進行處理，判斷實際地址addr跟junc處理過的數據是否相同。