上一篇博客主要寫了SVA的基本語法（詳細），這一篇主要寫SVA語法總結，以及如何查看SVA波形等。
斷言assertion被放在verilog設計中，方便在仿真時查看異常情況。當異常出現時，斷言會報警。一般在數字電路設計中都要加入斷言，斷言占整個設計的比例應不少於30%。以下是斷言的語法：
1. 斷言的位置
SVA的插入位置：在一個.v文件或者.sv的文件中：
module ABC ();
rtl 代碼
SVA斷言
endmodule
如：
module inline(
input logic clk ,
input logic a ,
input logic b ,
input logic [7:0] d1 ,
input logic [7:0] d2 ,
output logic [7:0] d
);
always @(posedge clk)
begin
if(a)
d <= d1;
if(b)
d <= d2;
end
property p_mutex;
@(posedge clk) not (a && b);
endproperty
a_mutex: assert property (p_mutex);
endmodule
注意：不要將SVA寫在endmodule外面。
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的作用。在VCS仿真的過程中，默認打印斷言失敗的情況，上述語句既可以打印斷言失敗的語句也可以打印斷言成功的語句。
上例中，事件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. SVA語法
3.1. 帶參數的property、帶參數的sequence
property也可以帶參數，參數可以是事件或信號，調用時寫成：assert property (p1(a,b))
被主sequence調用的從sequence也能帶參數，例如從sequence名字叫s2，主sequence名字叫s1:
sequence s1;
s2(a,b);
endsequence
3.2. property內部定義局部變量
內部可以定義局部變量，像正常的程序一樣
property p1;
int cnt;
.....................
endproperty
【注】在介紹語法之前，先強調寫斷言的一般格式：
一般，斷言是基於時序邏輯的，單純進行組合邏輯的斷言很少見，因為太費內存（時序邏輯是每個時鍾周期判斷一次，而組合邏輯卻是每個時鍾周期內判斷多次，內存吃不消）。
因此，寫斷言的一般規則是： time + event，要斷定發生什么event，首先要指定發生event的時間，例如
每個時鍾上升沿 + 發生某事
某信號下降時 + 發生某事
3.3. 語法1：信號（或事件）間的“組合邏輯”關系
(1) 常見的有：&&, ||, !, ^
(2) a和b哪個成立都行，但如果都成立，就認為是a成立：firstmatch(a||b)，與“||”基本相同，不同點是當a和b都成立時，認為a成立。
(3) a ? b:c —a事件成功后，觸發b，a不成功則觸發c
3.4. 語法2：在“時序邏輯”中判斷獨立的一根信號的行為
@ (posedge clk) A事件: —當clk上升沿時，如果發生A事件，斷言將報警。
邊沿觸發內置函數：(假設存在一個信號a)
$rose( a );—信號上升
$fell( a ); —信號下降
$stable( a );—信號值不變
3.5. 語法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] —斷定a在連續3個時鍾周期內都成立。
@ (posedge clk) a [*1:3] —斷定a在連續1~3個時鍾周期內都成立。
@ (posedge clk) a [->3] —斷定a在非連續的3個時鍾周期內都成立。
舉一個復雜點的例子：
property ABC;
int tmp;
@(posedge clk) ($rose(a),tmp = b) |-> ##4 (c == (tmp*tmp+1)) ##3 d[*3];
endproperty
a_ABC: assert property(事件2)
上例的一個property說明：當clk上升沿時，斷言開始。首先斷定信號a由低變高，將此時的信號b的值賦給變量tmp，4個時鍾周期后，斷定信號c的值是4個周期前b^2+1，再過3個周期，斷定信號d一定會起來，再過3個周期，信號d又起來一次,只有這些斷定都成功，該句斷言成功。否則，信號a從一開始就沒起來，則斷言也成功。
3.6 語法4：多時鍾域聯合斷言
一句斷言可以表示多個時鍾域的信號關系，例如：
@(posedge clk1) a |-> ##1 @ (posedge clk2) b
當clk1上升沿時，事件a發生，緊接着如果過來第二個時鍾clk2的上升沿，則b發生。“##1”在跨時鍾時不表示一個時鍾周期，只表示等待最近的一個跨時鍾事件。所以此處不能寫成##2或其他。但是可以寫成：
@ （posedge clk1） a |=> @ (posedge clk2) b
3.7. 語法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是高，其他是低。
3.8 語法6：屏蔽不定態
當信號被斷言時，如果信號是未復位的不定態，不管怎么斷言，都會報告：“斷言失敗”，為了在不定態不報告問題，在斷言時可以屏蔽。
如： @(posedge clk) (q == $past(d))，當未復位時報錯，屏蔽方法是將該句改寫為：
@(posedge clk) disable iff (!rst_n) (q == $past(d)) //rst是低電平有效
3.9. 語法7：斷言覆蓋率檢測
name: cover property (func_name)
功能覆蓋是按照設計規范衡量驗證狀態的一個標准，它可以分成兩類。
a． 協議覆蓋
b． 測試計划覆蓋
斷言可以用來獲得有關協議覆蓋的窮舉信息。SVA提供了關鍵詞“cover”來實現這一功能，cover語句的基本語法如下所示。
<cover_name> : cover property (property_name)
“cover_name”是用戶提供的名稱，用來標明覆蓋語句，“property_name”是用戶想獲得覆蓋信息的屬性名。如：
c_mutex : cover property (property_mutex);
cover語句的結果包含下面的信息：
（1）、屬性被嘗試檢驗的次數。
（2）、屬性成功的次數。
（3）、屬性失敗的次數。
（4）、屬性空成功的次數。
檢驗器“mutex_clk”在一次模擬中的覆蓋日志的實例如下所示。
就像斷言（assert）語句一樣，覆蓋（cover）語句可以有執行塊。在一個覆蓋成功匹配時，可以調用一個函數（function）或者任務（task），或者更新一個局部變量。
4. 在VCS中加入斷言編譯和顯示功能：
在fsdb文件中加一句話：$fsdbDumpSVA
在VCS編譯參數：vcs中加入一些options:
編譯選項：
-assert enable_diag\
-assert vpiSeqBeginTime\
-assert vpiSeqFail\
執行選項：
-assert report=路徑\
-assert finish_maxfail=100
5.總結
以下是一些編寫斷言的總結：
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]);”就是function調用。
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個斷言，沒更好的方法。
這篇文檔是參考別人的，具體是誰的，我也不記得了，只知道這篇文檔對我的幫助很大，入門的文檔，寫的很不錯。