verilog斷言（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
b;
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處理過的資料是否相同。
//“addr == junc(arr[0],arr[1],arr[2],arr[3]);”就是junction呼叫。
property wr_p;
int arr[4];
@(posedge clk) !vld_pulse_r[0] && !DataIn
##4 (read==read, arr[0] = DataIn)
##1 (read==read, arr[1] = DataIn)
##1 (read==read, arr[2] = DataIn)
##1 (read==read, arr[3] = DataIn) |=>
addr == junc(arr[0],arr[1],arr[2],arr[3]);
endproperty
//////////////////////////////////////////////////////////////////////////
function [3:0] junc;
input a,b,c,d;
reg [3:0] a1;
reg [3:0] b1;
reg [3:0] c1;
reg [3:0] d1;
a1 = {3'b0,a};
b1 = {3'b0,b};
c1 = {3'b0,c};
d1 = {3'b0,d};
junc = a1+(b1<<1)+(c1<<2)+(d1<<3);
$display(junc);
endfunction
////////////////////////////////////////////////////////////////////////
7. 如果想在SVA中使用類似for(){....}的功能，別忘了語法中介紹的[*3]，這是在斷言中實現for的唯一方式。
##4 (廢話, cnt = 0, arr[cnt] = DataIn, cnt++) //初始化一下，
##1 (read==read, arr[cnt] = DataIn, cnt++)[*3] //迴圈3次
8. 每句斷言都是一個小程式：如上例，在##4時間點上，(廢話, cnt = 0, arr[cnt] = DataIn, cnt++)就是一個小程式，訊號斷言必須是第一句，其他運算按照順序進行。
9. 斷言的變數除了可用C語言中的int，float外，還可以是reg [n:0]等數位電路型別。
10. 注意：
像這種寫法：
property ept_p;
@(posedge rd_clk) ((rd_num == 0) |-> rd_ept)
&& (rd_ept |-> (rd_num == 0));
endproperty
是錯誤的，寫了|->，就不能再用 && 等事件組合邏輯了。
解決方法是使用2個斷言，沒更好的方法。