SystemVerilog Assertion(SVA):是一種描述性的語言，可以很容易的描述時序相關的情況，所以主要用在協議檢查和協議覆蓋。SVA在systemverilog仿真器中的
調度區間在RTL之后，Testbench之前。所以同一時鍾斷言只能采樣到上一時刻的RTL值。由於是描述性語句，所以“;”用的比較多。
斷言失敗后會自動打印信息到log文件，用戶也可以自定義打印內容。
assertion name： assert xxxx
$display("xxxxx");
else
$display("xxxxx");
SVA分為並發斷言：基於時鍾的，調度區間按assertion的調度區間，可以在過程塊(always initial),模塊(module),接口(interface),程序(program)中定義。
即時斷言：基於事件的，本質不是時序關系，會立刻求值。進行檢查。只能在過程塊(always initial)中定義。
兩者另一個區別是：並發斷言會用property來聲明，即時斷言不需要。
always
begin
a_ia: assert (a && b); //即時斷言
end
因為並發斷言應用更多，所以一下均以並發斷言來說：
並發斷言可以自定義一個SVA塊來描述自己要求的時序，兩個關鍵字：sequence, property。
sequence s1; //sequence允許自己定義更小的時鍾描述
a ##2 b;
endsequence
property s2; //property 一個assert只能有一個
@(posedg clk) s1;
endproperty
s3 ：assert property(s2); //標准形式 name : assert property();
斷言中內嵌的表示信號的上升沿和下降沿的函數：$rose(expression or signal) $fell(expression or signal) $stable(expression or signal) $changed(expression)
sequence s2;
@(posedge clk) $rose(a); //時鍾的上升沿仍然用posedge, 信號的上升沿才用$rose();
endsequence
斷言中時序延時的描述： ##表示延時，但是注意觸發加.ended，否則SVA默認都是按起始時刻來對齊的，也就是說如果斷言3時刻觸發，5時刻succeed，但是斷言
也是會報道3時刻的對錯。
sequence s2;
@(posedge clk) a ##2 b; //a為高電平延時2個時鍾后如果b為高電平，則斷言成功。
endsequence
property p12;
@(posedge clk) (a && b) |-> ##[1:3] c; //相當於(a && b) |-> ##1 c; 或 (a && b) |-> ##2 c; (a && b) |-> ##3 c;
endproperty
斷言中時鍾的定義：一般情況下，在property中定義時鍾，而保證sequence獨立於時鍾比較好。當然從語法角度來說，時鍾可以定義在property,sequence,assert
中。但是當assert定義時鍾之后，property不能再重新定義時鍾。
sequence s5a;
a ##2 b;
endsequence
property p5a;
@(posedge clk) s5a; //在property中定義時鍾
endproperty
a5a: assert property(p5a); //assert不再定義時鍾
斷言通過蘊含操作符來作為斷言的觸發條件，交疊蘊含： “|->”來表示，表示在先行算子(蘊含前的表達式)有效的同一個時刻判斷后續算子(蘊含后的表達式)。
非交疊蘊含： “|=>”來表示，表示在先行算子有效的下一時刻再判斷后續算子。
property p8; property p9;
@(posedge clk) a |-> b; //同一時刻 @(posedge clk) a |=> b; //延時一個時鍾
endproperty endproperty
##m延時m個clock：
[*n]重復n次：
assert property (@posedge clk) rst[*2]; end property //最開始的clock連續重復兩個cycle rst
[=m]重復m次，不要求連續
[->m]重復m次，與[=m]的主要區別是，在后邊加延時##1時，[=m]不准確表示延時1個clock
[->m]表示准確延時1個clock
sig1 throughout seq：throughout之前表示一個expression，之后表示一個sequence，在sequence期間，expression一直有效。
seq1 within seq2：within前后都表示sequence，在后一sequence有效期間，sequence1必須一直有效。
seq1 and seq2：兩個sequence進行與運算，兩個sequence必須同時start，但是不要求同時結束。
seq1 or seq2：兩個sequence進行或運算，只要有一個sequence有效，該語句有效。
seq1 intersect seq2，兩個seq必須完全同時開始，同時結束，同時有效。
not seq1：表示對seq的結果取反
if(expression) seq1 else seq2：if---else語句控制，但是好像不能用在local var的場景中。
sva提供的system task：
1)$onehot(expression)，在expression中只有一個1或者沒有1時，表示結果正確
2)$isunknown(expression)，在expression中包含x、z時，表示結果正確
3)$countones(expression)，返回expression中1的個數， ones=$countones(busgnt)
4)$assertoff(level, list of module) $asserton $assertkill
sva中可以定義local var，
賦值與比較，前都必須有一個sequence，或者顯示指明1’b1
sequence rdc;
##[1:5] rdDone;
endsequence
sequence datacheck;
int local_data;
(rdc, local_data = rData) ##5 (wData == (local_data + 'hff));
endseqence
baseP：assert property (@(posedge clk) RdWr |-> dataCheck) else gotoFail;
sequence s1;
int x;
((1'b1, x = data) ##0 ((a ##1 b) or (d ##1 e) ) ##1 (data1 == x+1);
endsequence
延時中不可以使用參數，變量定義時，不能用參數，因為變量在elabration時，需要使用
property checkDelay;
int lv;
(readReq, lv=dataDelay) |=> ##[0:lv] readData; （錯誤）
endproperty
endsequence