暑期實習兩個月的其中一個任務是：如何在設計中加入斷言？以及斷言的基本語法、三種應用場景下的斷言（如FIFO、FSM、AXI4-lite總線）。參考書籍：《System Verilog Assertion 應用指南》
一、SVA介紹
1.1斷言的定義
An assertion is a statement that a given property is required to be true, and a directive to verification tools to verify that the property does hold。
1.2斷言的好處
- 獲取設計者的目的；
- 允許協議被定義和驗證；
- 減少投入到市場的時間；
- 很大程度上簡化可重用IP核的驗證；
- 促進功能覆蓋率的度量。
1.3 建立SVA檢驗器的步驟
Step1：建立布爾表達式
在任何設計模型中，功能總是由多個邏輯事件的組合來表示的。這些事件可以是簡單的同一個時鍾邊緣被求值的布爾表達式，或者經歷幾個時鍾周期的求值的事件。
Step2：建立序列表達式
SVA用關鍵詞“sequence”來表示這些事件。序列（sequence）的基本語法是：
sequence name_of_sequence;
<test expression>;
endsequence
Step3 : 建立屬性
許多序列可以邏輯或者有序地組合起來生成更加復雜的序列。SVA提供了一個關鍵詞“property”來表示這些復雜的有序行為。屬性（property）的基本語法是：
property name_of_ property;
<test expression>; or
<complex sequence expressions>;
endproperty: name_of_ property
Step4：斷言屬性
屬性是在模擬過程中被驗證的單元。它必須在模擬過程中被斷言來發揮作用。SVA提供了關鍵詞“assert”來檢查屬性。斷言（assert）的基本語法是：
assertion_name: assert property(name_of_ property)
For example：下面這個檢驗器驗證信號request在當前周期為高電平是，下面1~4個周期內，信號acknowledge應該變為高電平。
property pReqAck;
@(posedge clk) request |-> ##[1:4] acknowledge;
endproperty: pReqAck
apReqAck : assert property (pReqAck);
1.4 SVA術語
SystemVerilog語言中定義了兩種斷言：並發斷言和即時斷言。
①並發斷言（Concurrent Assertion）
- 基於時鍾周期。
- 在時鍾邊緣根調用的變量的采樣值計算測試表達式。
- 變量的采樣在預備階段完后，而表達式的計算在調度器的觀察階段完成。
- 可以被放到過程塊（procedural block）、模塊（module）、接口（interface），或者一個程序（program）的定義中。
- 可以在靜態（形式的）驗證和動態驗證（模擬）工具中使用。
一個並發斷言的例子如下：
a_cc: assert property (@(posedge clk) not (a && b));
Tips：所有的成功顯示成向上的箭頭，所有的失敗顯示鄉下的箭頭。
這個例子的核心內容是屬性在每一個時鍾的上升沿都被檢驗，不論信號a 和信號 b 是否有值得變化。
②即時斷言（ImmediateAssertion）
- 基於模擬事件的語言。
- 測試表達式的求值就像在過程塊中的其他Verilog的表達式一樣。它們的本質不是時序相關的，而且立即被求值。
- 必須放在過程塊的定義中。
一個即時斷言的例子如下：
always_comb
begin
a_ia: assert (a && b);
end
當信號 a 或者信號 b 發生變化時，always塊被執行。
Tips：區別即時斷言和並發斷言的關鍵詞是“property”。
1.5 一個簡單的序列
序列s1檢查信號“a”在每個時鍾上升沿都為高電平。如果信號“a”在任何一個時鍾上升沿不為高電平，斷言將失敗。
sequence s1;
@(posedge clk) a;
endsequence
1.6邊沿定義的序列
序列s1使用的是信號的邏輯值。SVA也內嵌了邊緣表達式，以便用戶監視信號值從一個時鍾周期到另一個時鍾周期的跳變。這使得用戶能檢查邊沿敏感的信號。三種這樣有用的內嵌函數如下：
$rose(boolean expression or signal_name) 當信號、表達式的最低位變成1時返回真。
$fell(boolean expression or signal_name) 當信號、表達式的最低位變成0時返回真。
$stable(boolean expression or signal_name) 當表達式不發生變化時返回真。
序列s2檢查信號“a”在每一個時鍾上升沿都跳變成1。如果跳變沒有發生，斷言失敗。
sequence s2;
@(posedge clk) $rose (a);
endsequence
1.7 邏輯關系的序列
序列s3檢查每一個時鍾上升沿，信號“a”或者信號“b”是高電平，則斷言成功。如果兩個信號都是低電平，斷言失敗。
sequence s3;
@(posedge clk) a || b;
endsequence
1.8 序列表達式
通過在序列定義中定義形參，相同的序列能被重用到設計中具有相似行為的信號上。
sequence s3_lib (a, b);
a || b;
endsequence
通用的序列s3_lib能重用在任何兩個信號上。如，在兩個信號“req1”和“req2”，它們中至少一個信號應該在時鍾周期的上升沿為1，可以使用一下的序列。
sequence s3_lib_inst1;
s3_lib(req1, req2);
endsequence
1.9 時序關系的序列
簡單的布爾表達式在每個時鍾邊緣都會被檢查。它們只是簡單的組合邏輯檢查。很多時候我們關心的是檢查需要幾個時鍾周期才能完成的事件。也就是所謂的“時序檢查”。在SVA中，時鍾周期延遲用“##”來表示。
例如，##3表示3個時鍾周期。
在序列s4檢查信號“a”在一個給定的時鍾上升沿為高電平，如果信號“a”不是高電平，序列失敗。如果信號“a”在任何一個給定的時鍾上升沿為高電平，信號“b”應該在兩個時鍾周期后為高電平。如果信號“b” 在兩個時鍾周期后不為1，斷言失敗。注意，序列以信號“a”在時鍾上升沿為高電平開始。
sequence s4;
@(posedge clk) a ##2 b;
endsequence
需要注意的是，在圖中，成功的序列總是標注在序列開始的位置。時鍾數5成功（開始於5，結束於7）；時鍾數14成功（開始於14，結束於16）。（例子后續會添加）
1.10 SVA中的時鍾定義
一個序列或者屬性在模擬過程中本身並不能起什么作用。它們必須像下面的例子那樣被斷言才能發揮作用。
sequence s5;
@(posedge clk) a ##2 b;
endsequence
property p5;
s5；
endproperty
a5: assert property (p5);
注意，序列s5中制定了時鍾。這是一種把檢查和時鍾關聯起來的方法，但是還有其他的方法。在序列、屬性，甚至一個斷言的語句中都可以定義時鍾。下面的代碼顯示了在屬性p5a的定義中指定時鍾。
sequence s5a;
a ##2 b;
endsequence
property p5a;
@(posedge clk) s5a；
endproperty
a5a: assert property (p5a);
通常情況下，在屬性（property）的定義中指定時鍾，並保持序列（sequence）獨立於時鍾是一種好的編碼風格。這可以提高基本序列定義的可重用性。
斷言的一個序列並不一定需要定義在一個獨立的屬性。因為斷言語句調用屬性，在斷言的語句中可以直接調用被檢查的表達式，如下面的斷言a5b所示。
sequence s5b;
a ##2 b;
endsequence
a5b: assert property (@(posedge clk) s5b)
1.11禁止屬性
在之前的所有例子中，屬性檢查的都是正確的條件。屬性也可以被禁止發生。換句話說，我們期望屬性永遠為假。當屬性為真時，斷言失敗。
序列s6檢查當信號“a”在給定的時鍾上升沿為高電平，那么兩個時鍾周期以后，信號“b”不允許是高電平，關鍵詞“not”用來表示屬性應該永遠不為真。
sequence s6;
@(posedge clk) a ##2 b;
endsequence
property p6;
not s6;
endproperty
a6: assert property (p6);
1.12一個簡單的執行塊
SystemVerilog語言被定義成每當一個斷言檢查失敗，模擬器在默認情況下都會打印出一條錯誤信息。模擬器不需要對成功的斷言打印任何東西。也可以使用斷言陳述中的“執行塊”（action block）來打印自定義的成功或失敗信息。執行塊的基本語法如下所示。
assertion_name:
assert property(property_name)
<success message>;
else
<fail message>;
下面顯示的檢驗器a7在執行塊中使用了簡單的顯示語句來打印成功和失敗信息。
寫法一：
sequence s7;
@(posedge clk) a ##2 b;
endsequence
property p7;
s7；
endproperty
a7: assert property (p7)
$display(“Sequence s7 successed\n”);
else
$display(“Sequence s7 failed\n”);
寫法二：
property p7;
@(posedge clk) a ##2 b;
endproperty
a7: assert property (p7)
$display(“Property p7 successed\n”);
else
$display(“Property p7 failed\n”);
執行塊不僅僅局限於顯示成功和失敗。它可以有其他的應用，例如：控制模擬環境和收集功能覆蓋數據。
1.13蘊含（Implication）操作符
蘊含等效於一個if-then結構。蘊含的左邊叫做“先行算子”（antecedent），右邊叫做“后續算子”（consequence）。先行算子是約束條件。當先行算子成功時，后續算子才會被計算。如果先行算子不成功，那么整個屬性就默認地被認為成功。這叫做“空成功”（vacuous success）。
蘊含結構只能被用在屬性定義中，不能在序列中使用。
蘊含可以分為兩類：交疊蘊含（Overlapped implication）和非交疊蘊含（Non-Overlapped implication）
1.13.1 交疊蘊含
交疊蘊含用符號“|->”表示。如果先行算子匹配，在同一個時鍾周期計算后續算子表達式。
下面用一個簡單的例子解釋。屬性p8檢查信號“a”在給定的時鍾上升沿是否為高電平，如果a為高，信號“b”在相同的時鍾邊沿也必須為高。
property p8;
@(posedge clk) a |-> b;
endproperty
a8: assert property (p8);
當信號“a”檢測為有效的高電平，而且信號“b”在同一個時鍾沿也檢測為高，這是一個真正的成功。若信號“a”不為高，斷言默認地自動成功，則稱之為空成功。相應的，失敗指的是信號“a”檢測為高且在同一時鍾沿信號“b”未能檢測為有效的高電平。
1.13.2 非交疊蘊含
交疊蘊含用符號“|=>”表示。如果先行算子匹配，在下一個時鍾周期計算后續算子表達式。后續算子表達式的計算總是有一個時鍾周期的延遲。
下面用一個簡單的例子解釋。屬性p9檢查信號“a”在給定的時鍾上升沿是否為高電平，如果a為高，信號“b”在下一個時鍾邊沿為高。
property p9;
@(posedge clk) a |=> b;
endproperty
a9: assert property (p9);
需要注意的是，斷言在當前時鍾周期開始，在下一個時鍾周期成功的情況下才是真正的成功。相應的，如果屬性有一個有效的開始（信號“a”為高），且信號“b”在下一個時鍾周期不為高，屬性失敗。
1.13.3 后續算子帶固定延遲的蘊含
屬性p10檢查如果信號“a”在給定時鍾上升沿為高，在兩個時鍾周期后信號“b”應該為高。
property p10;
@(posedge clk) a |-> ##2 b;
endproperty
a10: assert property (p10);
1.13.4 使用序列作為先行算子的蘊含
屬性p10在先行算子的位置使用的是信號。先行算子同樣可以使用序列的定義。在這種情況下，僅當先行算子中的序列成功時，才計算后續算子中的序列或者布爾表達式。在任何給定的時鍾周期，序列s11a檢查如果信號“a”和信號“b”都為高，一個時鍾周期之后信號“c”應該為高。序列s11b檢查當前時鍾上升沿的兩個時鍾周期后，信號“d”應該為低。最終的屬性檢查如果序列s11a成功，那么序列s11b被檢查。如果沒有檢測到有效的序列s11a，那么序列s11b將不被檢查，屬性檢查得到一次空成功。
sequence s11a;
@(posedge clk) (a && b) ##1 c;
endsequence
sequence s11b;
@(posedge clk) ##2 !d;
endsequence
property p11;
s11a |-> s11b；
endproperty
a11: assert property (p11);
1.14 SVA檢驗器的時序窗口
到目前為止，帶延遲的例子使用的都是固定的正延遲。下面，將討論集中不同的描述延遲的方法。
屬性p12檢查布爾表達式“a&&b”在任何給定的時鍾上升沿為真。如果表達式為真，那么在接下來的1~3個中周期內，信號“c”應該至少在一個時鍾周期內為高。
SVA允許使用時序窗口來匹配后續算子。時序窗口表達式左手邊的值必須小於右手邊的值。左邊的值可以為0。如果它是0，表示后續算子必須在先行算子成功的那個時鍾沿開始計算。
property p12;
@(posedge clk) (a&&b) |-> ##[1:3] c;
endproperty
a12: assert property (p12);
p12實際上以上面三個線程展開。
(a&&b) |-> ##1 c 或
(a&&b) |-> ##2 c 或
(a&&b) |-> ##3 c
屬性有三個機會成功。所有三個線程具有相同的起始點，但是一旦第一個成功的線程將使整個屬性成功。注意：在任何時鍾上升沿只能有一個有效的開始，但是可以有多個有效的結束。這是因為每個有效的開始可以有三個機會成功。
1.14.1 重疊的時序窗口
屬性p13與屬性p12相似。兩者最大的區別是p13的后續算子在先行算子成功的同一個時鍾沿開始計算。
property p13;
@(posedge clk) (a&&b) |-> ##[0:3] c;
endproperty
a13: assert property (p13);
1.14.2無限的時序窗口
在時序窗口上限可以用“$”定義，這表明時序沒有上限。這叫做“可能性”（eventuality）。檢驗器不停地檢查表達式是否成功直到模擬結束。因為會對模擬器的性能產生巨大的負面影響，所有這不是編寫SVA的一個高效的方式。最好總是使用有限的時序窗口上限。
property p14;
@(posedge clk) a |-> ##[1:$] b ##[0:$] c;
endproperty
a14: assert property (p14);
1.15 “ended”結構(需要鞏固)
到目前為止，定義的序列都只是用了簡單的連接（concatenation）的機制。換句話講，就是將多個序列以序列的起始點作為同步點，來組合成時間上連續的檢查。
SVA還提供了另外一種使用序列結束點作為同步點的連接機制。這種機制通過給序列名字追加關鍵詞“ended”來表示。例如，s.ended表示序列的結束點。關鍵詞“ended”保存了一個布爾值，值的真假取決於序列是否在特定的時鍾邊沿匹配檢驗。這個s.ended的布爾值只有在相同時鍾周期有效。
序列s15a和s15b是兩個需要多個時鍾周期來完成的簡單序列，屬性p15a檢查序列s15a和序列s15b滿足連着間隔一個時鍾周期的延遲分別匹配檢驗。屬性p15b檢查相同的協議，但使用了關鍵詞“ended”。在這種情況下，兩個序列在結束點同步。由於使用了結束點，兩個序列間加上兩個時鍾周期的延遲，來保證斷言檢驗的協議與p15a相同。
sequence s15a;
@(posedge clk) a ##1 b;
endsequence
sequence s15b;
@(posedge clk) c ##1 d;
endsequence
property p15a;
s15a |=> s15b；
endproperty
property p15b;
s15a.ended |-> ##2 s15b.ended；
endproperty
a15a: assert property (p15a);
a15b: assert property (p15b);
上述例子中，我們用了兩種不同的方法來實現一個檢驗。第一種基於序列的起始點來同步序列。第二種方法基於序列的結束點來同步序列。
1.16 使用參數的SVA檢驗器
SVA允許像Verilog那樣在檢驗器使用參數（parameter）。兩個信號間的延遲信息可以在檢驗器中用參數表示，那么這種檢驗器就可以在設計只有時序關系不同的情況重用。例子1.2顯示了一個帶延遲默認值參數的檢驗器。如果這個檢驗器在設計中被調用，它是以一個時鍾周期作為延遲默認值。如果在實例化中重設檢驗器中延遲參數值，那么同一個檢驗器可以被重用。
module generic_chk(
input logic clk
);
parameter delay = 1;
reg a = 1'b0;
reg b = 1'b0;
always @(posedge clk)
begin
a <= $urandom_range(0,1);
b <= $urandom_range(0,1);
end
property p16;
@(posedge clk) a |-> ##delay b;
endproperty
a16: assert property(p16);
endmodule
//call checker from the top.sv level module
generic_chk #(.delay(2)) i1(
.clk(clk)
);
generic_chk i2(
.clk(clk)
);
1.17 使用選擇運算符的SVA檢驗器
SVA允許在序列和屬性中使用邏輯運算符。屬性p17檢查如果信號“c”為高，那么信號“d”的值與信號“a”的相等。如果信號“c”不為高，那么信號“d”的值與信號“b”的相等。這是一個組合的檢驗，在每個時鍾上升沿被執行。
property p17;
@(posedge clk) c ? d == a : d == b;
endproperty
a17: assert property(p17);
1.18 使用true表達式的SVA檢驗器
使用true表達式，可以在時間上延長SVA檢驗器。這代表一種忽略的狀態，它使得序列延長了一個時鍾周期。這可以用來實現同時監視多個屬性且需要同時成功的復雜協議。
序列s18a檢查一個簡單的條件。序列s18a_ext檢查相同的條件，但是序列的成功被往后移了一個時鍾周期。當這個序列被用在一個屬性的先行算子時，它會造成一些差異。兩個序列的結束點不同，因此開始檢查后續算子的時鍾周期也不一樣。
`define true 1
sequence s18a;
@(posedge clk) a ##1 b;
endsequence
sequence s18a_ext;
@(posedge clk) a ##1 b ##1 `true;
endsequence
sequence s18b;
@(posedge clk) c ##1 d;
endsequence
property p18;
@(posedge clk) s18a.ended |-> ##2 s18b.ended;
endproperty
property p18_ext;
@(posedge clk) s18a_ext.ended |-> ##2 s18b.ended;
endproperty
a18: assert property (p18);
a18_ext: assert property (p18_ext);
1.19 “$past”構造
SVA提供了一個內嵌的系統函數“$past”，它可以得到信號在幾個時鍾周期之前的值。在默認情況下，它提供信號在前一個時鍾周期的值。結構的基本語法如下：
$past(signal_name, number of clock cycles)
這個任務能夠有效地驗證到達當前時鍾周期的狀態所采用的通路是正確的。
屬性p19檢驗的是在給定的時鍾上升沿，如果表達式（c&&d）為真，那么兩個周期前，表達式（a&&b）為真。
property p19;
@(posedge clk) (c && d) |-> ($past((a&&b), 2) == 1’b1);
endproperty
a19: assert property (p19);
帶時鍾門控的$past構造
“$past”構造可以由一個門控信號（gating singal）控制。比如，在一個給定的時鍾沿，只有當門控信號的值為真時才檢查后續算子的情況。使用門控信號的$past構造的基本語法如下：
$past(signal_name, number of clock cycles，gating signal)
屬性p20與屬性p19相似。但是只有當門控信號“e”在任意給定的時鍾上升沿有效時檢驗才被激活。
property p20;
@(posedge clk) (c && d) |-> ($past ( ( a&&b ), 2, e) == 1’b1);
endproperty
a20: assert property (p20);
1.21 重復運算符
SVA語言提供三種不同的重復運算符：連續重復（consecutive repetition），跟隨重復（go to repetition），非連續重復（non-consecutive repetition）。
連續重復---允許用戶表明信號或者序列將在指定數量的時鍾周期內都連續地匹配。信號的每次匹配之間都有一個時鍾周期的隱藏延遲。
連續重復運算符的基本語法如下：
signal or sequence [*n]
“n”是表達式應該匹配的次數。
比如，a[*3]可以被展開成：a ## 1 a ##1 a
而序列（a##1b）[*3]可以展開為：（a##1b）## 1（a##1b）## 1（a##1b）
跟隨重復---允許用戶表明一個表達式將匹配達到指定的次數，而且不一定在連續的時鍾周期上發生。這些匹配可以是間歇的。跟隨重復的只要要求是被檢驗重復的表達式的最好一個匹配應該發生在整個序列匹配結束之前。
跟隨重復運算符的基本語法如下：
signal [->n]
參考下面的序列：
start ##1 a[->3] ##1 step
這個序列需要信號“a”的匹配（即信號“a”的第三次，也就是最好以重復的匹配）正好發生在“stop”成功之前。換句話說，信號“stop”在序列的最后一個時鍾周期匹配，而且在前一個時鍾周期，信號“a”有一次匹配。
非連續重復---與跟隨重復相似，除了它並不要求信號的最后一次重復匹配發生在整個序列匹配前的那個時鍾周期。
非連續重復運算符的基本語法如下：
signal [=n]
在跟隨重復和非連續重復中只允許使用表達式，不能使用序列。
1.21.1連續重復運算符[*]
屬性p21檢查在檢驗有效地開始兩個時鍾周期后，信號“a”在連續的三個時鍾周期為高，再過兩個時鍾周期，信號“stop”為高。下一個時鍾周期，信號“stop”為低。
property p21;
@(posedge clk) $rose(start) |-> ##2 (a[*3]) ##2 stop ##1 !stop ;
endproperty
a21: assert property (p21);
1.21.2 用於序列的連續重復運算符[*]
屬性p22檢查有效開始的兩個時鍾周期以后，序列(a ##2 b)重復三次，接着再過兩個時鍾周期，信號“stop”為高。
property p22;
@(posedge clk) $rose(start) |-> ##2 ((a ##2 b) [*3]) ##2 stop ;
endproperty
a22: assert property (p22);
1.21.3 用於帶延遲窗口的序列的連續重復運算符[*]
屬性p23檢查有效開始的兩個時鍾周期以后，序列(a ##[1:4] b)重復三次，接着再過兩個時鍾周期，信號“stop”為高。實際上，這個序列有一個時序窗口，使得情況變得有些復雜。
property p23;
@(posedge clk) $rose(start) |-> ##2 ((a ##[1:4] b) [*3]) ##2 stop ;
endproperty
a23: assert property (p23);
主序列(a ##[1:4] b)[*3]可以被擴展成：
((a ##1 b) or (a ##2 b) or (a ##3 b) or (a ##4 b)) ##1
((a ##1 b) or (a ##2 b) or (a ##3 b) or (a ##4 b)) ##1
((a ##1 b) or (a ##2 b) or (a ##3 b) or (a ##4 b))
1.21.4連續運算符[*]和可能運算符
屬性p23指定了一個重復序列的時序窗口。同樣的，重復的次數也可以是一個窗口。比如,a[*1:5]表示信號“a”從某個時鍾周期開始重復1~5次。這個定義可以展開成下面的表達式。
a or
(a ##1 a) or
(a ##1 a ##1 a) or
(a ##1 a ##1 a ##1 a) or
(a ##1 a ##1 a ##1 a ##1 a)
重復窗口的邊界規則與延遲窗口的相同。左邊的值必須小於右邊的值。右邊的值可以是“$”，這表示沒有重復次數的限制。
屬性p24顯示了一個帶沒有重復次數限制的有限的檢查。它檢驗有效開始兩個時鍾周期后，信號“a”將保持為高，直到信號“stop”跳變為高。
property p24;
@(posedge clk) $rose(start) |-> ##2 (a [*1 : $]) ##1 stop ;
endproperty
a24: assert property (p24);
1.21.5 跟隨重復運算符[->]
屬性p25檢查如果在任何時鍾上升沿有效開始，兩個時鍾周期以后，信號“a”連續或者間斷地出現3次為高，接着信號“stop”在下一個時鍾周期為高。
property p25;
@(posedge clk) $rose(start) |-> ##2 (a [->3]) ##1 stop ;
endproperty
a25: assert property (p25);
1.21.6非連續重復運算符[=]
屬性p26檢查如果在任何時鍾上升沿有有效的開始信號，兩個時鍾周期后，在一個有效的“stop”信號前，信號“a”連續或者間斷地出現3次為高，然后一個時鍾周期后“stop”應該為低。p26和p25做的是相同的檢查，唯一不同的是p26使用的是非連續（non-consecutive）重復運算符而不是跟隨（go to）重復運算符。這表示在屬性p26中，在信號“stop”有效匹配的前一個時鍾周期，信號“a”不一定需要有有效的匹配。
property p26;
@(posedge clk) $rose(start) |-> ##2 (a [=3]) ##1 stop ##1 !stop;
endproperty
a26: assert property (p26);
1.22 “and”構造
二進制運算符“and”可以用來邏輯地組合兩個序列。當兩個序列都成功時整個屬性才成功。兩個序列必須具有相同的起始點，但是可以有不同的結束點。檢驗的起始點是第一個序列的成功時候的起始點，而檢驗的結束點是使得屬性最終成功的另一個序列成功時的點。
序列s27a和s27b時兩個獨立的序列。屬性p27將兩者用運算符“and”組合起來。當兩個序列都成功時，屬性成功。
sequence s27a;
@(posedge clk) a ##[1:2] b;
endsequence
sequence s27b;
@(posedge clk) c ##[2:3] d;
endsequence
property p27;
@(posedge clk) s27a and s27b ;
endproperty
a27: assert property(p27);
1.23 “intersect”構造
“intersect”運算符和“and”運算符相似，它有一個額外要求。兩個序列必須在相同時刻開始且結束於同一時刻。換句話說，兩個序列的長度必須相等。
屬性p28檢驗與屬性p27相同的情況。唯一的區別是它使用的是“intersect”構造而不是“and”構造。
sequence s28a;
@(posedge clk) a ##[1:2] b;
endsequence
sequence s28b;
@(posedge clk) c ##[2:3] d;
endsequence
property p28;
@(posedge clk) s28a intersect s28b ;
endproperty
a28: assert property(p28);
1.24 “or”構造
二進制運算符“or”可以用來邏輯地組合兩個序列。只要其中一個序列成功，整個屬性就成功。
序列s29a和s29b時兩個獨立的序列。屬性p29將兩者用運算符“or”組合起來。當其中一個序列成功，整個屬性就成功。
sequence s29a;
@(posedge clk) a ##[1:2] b;
endsequence
sequence s29b;
@(posedge clk) c ##[2:3] d;
endsequence
property p29;
@(posedge clk) s29a or s29b ;
endproperty
a29: assert property(p29);
1.25 “first_match”構造
任何時候使用了邏輯運算符（如“and”和“or”）的序列中指定了時間窗，就有可能出現同一檢驗具有多個匹配的情況。“first_match”構造可以確保只用第一次序列匹配，而丟棄其他的匹配。當多個序列被組合在一起，其中只需時間窗的第一次匹配來檢驗屬性剩余的部分時，“first_match”構造非常有用。
在下面的例子中，屬性用運算符“or”將兩個序列組合在一起。這個屬性的幾個可能的匹配如下所示。
a ##1 b;
a ##2 b;
c ##2 d;
a ##3 b;
c ##3 d;
當檢驗屬性p30時，第一次匹配保留下來，其他匹配都被丟棄了。
sequence s30a;
@(posedge clk) a ##[1:3] b;
endsequence
sequence s30b;
@(posedge clk) c ##[2:3] d;
endsequence
property p30;
@(posedge clk) first_match (s30a or s30b) ;
endproperty
a30: assert property(p30);
1.26 “throughout”構造
蘊含（implication）是目前討論到的允許定義前提條件的一項技術。例如，要對一個指定的序列進行檢驗，必須某個前提條件為真。也有這樣的情況，要求在檢驗序列的整個過程中，某個條件必須一直為真。蘊含只能在時鍾沿檢驗前提條件一次，然后就開始檢驗后續算子部分，因此它不檢測先行算子是否一直保持為真。為了保證某些條件在整個序列的驗證過程中一直為真，可以使用“throughout”運算符。運算符“throughout”的基本語法如下所示：
（expression）throughout （sequence definition）
屬性p31檢查下列內容：
- 在信號“start”的下降沿開始檢查。
- 檢查表達式((!a&&!b)##1(c[->3])##1(a&&b))。
- 序列檢查在信號“a”和“b”的下降沿與信號“a”和“b”的上升沿之間，信號“c”應該連續或間斷地出現3次為高電平。
- 在整個檢驗過程中，信號“start”保持為低。
property p31;
@(posedge clk) $fell(start) |->(!start) throughout (##1 ( !a && !b ) ##1 ( c[->3] ) ##1 ( a&&b ) );
endproperty
a31: assert property(p31);
1.27 “within”構造
“within”構造允許在一個序列中定義另一個序列。
seq1 within seq2
這表示seq1在seq2的開始到結束的范圍內發生，且序列seq2的開始匹配點必須在seq1的開始匹配點之前發生，序列seq1的結束匹配點必須在seq2的結束匹配點之前結束。 屬性p32檢查序列s32a在信號“start”的上升沿和下降沿之間發生。信號“start”的上升和下降由序列s32b定義。
sequence s32a;
@(posedge clk) (( !a && !b ) ##1 ( c[->3] ) ##1 ( a&&b ) );
endsequence
sequence s32b;
@(posedge clk) $fell(start) ## [5:10] $rose(start);
endsequence
sequence s32;
@(posedge clk) s32a within s32b;
endsequence
property p32;
@(posedge clk) $fell(start) |-> s32;
endproperty
a32: assert property(p32);
1.28 內建的系統函數
SVA提供了幾個內建的函數來檢查一些最常用的設計條件。
$onehot(expression)—檢驗表達式滿足“one-hot”，換句話說，就是在任意給定的時鍾沿，表達式只有一位為高。
$onehot0(expression)—檢驗表達式滿足“zero one-hot”，換句話說，就是在任意給定的時鍾沿，表達式只有一位為高或者沒有任何一位為高。
$isunknown(expression)—檢驗表達式的任何位是否是X或者Z。
$countones(expression)—計算向量中為高的位的數量。
斷言語句a33a檢驗向量“state”是“one-hot”, 斷言語句a33b檢驗向量“state”是“zero one-hot”, 斷言語句a33c檢驗向量“bus”是否有任何位為X或Z。斷言語句a33b檢驗向量” bus”中等於1的位的個數大於1。
a33a: assert property( @ (posedge clk) $onehot(state) );
a33b: assert property( @ (posedge clk) $onehot0(state) );
a33c: assert property( @ (posedge clk) $isunknown(bus) );
a33d: assert property( @ (posedge clk) $countones (bus) );
1.29 “disable iff”構造
在某些設計情況下，如果一些條件為真，則我們不想執行檢驗。換句話說，這就像是一個異步的復位，使得檢驗在當前時刻不工作。SVA提供了關鍵詞“disable iff”來實現這種檢驗器的異步復位。“disable iff”的基本語法如下：
disable iff (expression) < property definition>
屬性p34檢查在有效開始后，信號“a”重復兩次，且1個周期之后，信號“b”重復兩次，再過一個時鍾周期，信號“start”為低。在整個序列過程中，如果“reset”被檢測為高，檢驗器會停止並默認地發出一個空成功的信號。
property p34;
@(posedge clk)
disable iff (reset)
$rose (start) |-> a[=2] ##1 b[=2] ##1 !start ;
endproperty
a34: assert property(p34);
1.30 使用“intersect”控制序列的長度
運算符intersect提供了一個定義可能性運算符可以使用的最小和最大時鍾周期數的機制。
屬性p35定義了一個序列來檢驗在給定時鍾邊沿，如果信號“a”為高，那么從下一個時鍾周期開始信號“b”最終將為高，接着在下一個時鍾周期開始信號“c”最終也會為高。這個序列每當信號“a”為高時就開始，並且可能一直到整個模擬結束時才成功。
整個可以使用帶1[*2:5]的intersect運算符來加以約束。這個intersect的定義檢查從序列的有效開始點（信號“a”為高），到序列成功的結束點（信號“c”為高），一共經過2~5個時鍾周期。
property p35;
(@(posedge clk) 1[*2:5] intersect (a ##[1:$] b ##[1:$] c));
endproperty
a35: assert property(p35);
1.31 在屬性中使用形參
可以用定義形參（formal arguments）的方式來重用一些常用的屬性。屬性“arb”使用了4個形參，並且根據這些形參進行檢驗。其中還定義了特定的時鍾。SVA允許使用屬性的形參來定義時鍾。這樣，屬性可以應用在使用不同時鍾的相似設計模塊中。同樣的，時序延遲也可以參數化，這使得屬性的定義更具有普遍性。
屬性首先檢查有效開始。在規定的時鍾上升沿，如果在信號“a”的下降沿后的2~5個時鍾周期內出現信號“b”的下降沿，那么這就是一個有效開始。如果先行算子匹配，那么屬性接着檢查信號“c”和信號“d”的下降沿在下一個時鍾周期出現，並且確保它們在4個連續的周期都保持為低。接着一個周期后，必須檢測到信號“c”和信號“d”都為高，且再過一個時鍾周期應該檢測到信號“b”為高。
假定這是處理三個具有相似信號的不同主控設備的仲裁器的協議，可以很容易地重用前面定義的屬性來檢驗所有3個主控設備的接口。
斷言a36_1，a36_2和a36_3定義了每個主控接口用的檢驗器，分別使用了各個接口對應的信號作為屬性arb的參數。
property arb (a,b,c,d);
@(posedge clk) ($fell (a) ##[2:5] $fell(b) ) |-> ##1 ($fell (c) && $fell(d) ) ## 0 (!c && !d) [*4] ##1 (c&&d) ##1 b;
endproperty
a36_1: assert property(arb(a1,b1,c1,d1));
a36_2: assert property(arb(a2,b2,c2,d2));
a36_3: assert property(arb(a3,b3,c3,d3));
1.32 嵌套的蘊含
SVA允許使用嵌套的蘊含。當我們有多個門限條件指向一個最終的后續算子時，這種構造十分有用。
屬性p_nest檢驗如果信號“a”有一個下降沿，則是一個有效開始，接着在一個周期后，信號“b”，“c”和“d”應該為低電平有效信號以保持這個有效開始。如果第二個條件匹配，那么在6到10個周期內期望“free”為真。注意，當且僅當信號“b”,“c”和”d”都匹配時，在后續狀況（consequent condition）“free”才會被檢驗是否為真。
`define free (a && b && c && d)
property p_nest;
@(posedge clk) $fell (a) |-> ##1 (!b && !c && !d ) |-> ## [6:10] `free;
endproperty
a_nest: assert property(p_nest);
同一個屬性可以被重寫成不使用嵌套蘊含的方式，如下所示。
property p_nest1;
@(posedge clk) $fell (a) ##1 (!b && !c && !d ) |-> ## [6:10] `free;
endproperty
a_nest1: assert property(p_nest1);
注意：
使用嵌套蘊含的屬性p_nest中沒有“else”情況，因此屬性很容易就能重寫成如p_nest1的形式。
1.33 在蘊含中使用if/else
SVA允許在使用蘊含的屬性的后續算子中使用“if/else”語句。
屬性p_if_else檢查如果信號“start”的下降沿被檢測到，就是一個有效開始，接着一個時鍾周期后，信號“a”或者信號“b”為高。在現行算子成功匹配時，后續算子有兩個可能的路徑。
- 如果信號“a”為高，那么信號“c”必須間歇地重復兩次為高，且在下一個時鍾周期，信號“e”必須為高。
- 如果信號“a”不為高，那么信號“d”必須間歇地重復兩次為高，且在下一個時鍾周期，信號“f”必須為高。
注意，在檢驗信號“a”的后續算子中有優先級。
property p_if_else;
@(posedge clk) ($fell (start) ##1 (a || b)) |->
if (a)
(c[->2] ##1 e)
else
(d[->2] ##1 f);
endproperty
a_if_else: assert property(p_if_else);
1.34 SVA中的多時鍾定義
SVA允許序列或者屬性使用多個使用定義來采樣獨立的信號或者子序列。SVA會自動地同步不同信號或者子序列使用的時鍾域。下面的代碼顯示了一個序列使用多個時鍾的簡單例子。
sequence s_multiple_clocks;
@(posedge clk1) a ##1 @(posedge clk2) b;
endsequence
序列s_multiple_clocks檢驗在時鍾“clk1”的任何上升沿，信號“a”為高，接着在時鍾“clk2”的上升沿，信號“b”為高。當信號“a”在時鍾“clk1”的任意給定上升沿為高時，序列開始匹配。接着“##1”延遲構造將檢驗時間移到時鍾“clk2”的最近的上升沿，檢驗信號“b”是否為高。當在一個序列中使用了多個時鍾信號時，只允許使用“##1”延遲構造。序列s_multiple_clocks不能被重寫成下面這種形式。
sequence s_multiple_clocks;
@(posedge clk1) a ##0 @(posedge clk2) b;
endsequence
sequence s_multiple_clocks;
@(posedge clk1) a ##2 @(posedge clk2) b;
endsequence
使用“##0”會產生混淆，即在信號“a”匹配后究竟哪個時鍾信號才是最近的時鍾。這將引起競爭，因此不允許使用。使用##2也不允許，因為不可能同步到時鍾“clk2”的最近的上升沿。
相似的技術可以用來建立有多個時鍾的屬性。如下面的例子所示：
property p_multiple_clocks;
@(posedge clk1) s1 ##1 @(posedge clk1) s2;
endproperty
a_multiple_clocks: assert property(p_multiple_clocks);
它假定序列s1沒有被時鍾驅動，或者它的時鍾定義和“clk1”一樣。它又假定序列s2沒有被時鍾驅動，或者它的時鍾定義和“clk2”一樣。同樣的，屬性可以在序列定義之間使用非交疊蘊含運算符。下面是一個簡單的例子：
property p_multiple_clocks;
@(posedge clk1) s1 |=> @(posedge clk1) s2;
endproperty
禁止在兩個不同時鍾驅動的序列之間使用交疊蘊含運算符。因為現行算子的結束和后續算子的開始重疊，可能引起競爭的情況，這是非法的。下面的代碼顯示了這種非法的編碼方式：
property p_multiple_clocks_implied_illegal;
@(posedge clk1) s1 |-> @(posedge clk1) s2;
endproperty
1.35 “matched”構造
任何時候如果一個序列定義了多個時鍾，構造“matched”可以用來檢測第一個子序列的結束點。
序列s_a查找信號“a”的上升沿。信號“a”是根據時鍾“clk1”來采樣的。序列s_b查找信號“b”的上升沿。信號“b”是根據時鍾“clk2”來采樣的。
屬性p_match驗證在給定的時鍾“clk2”的上升沿，如果序列s_a匹配，那么在一個周期后，序列s_b。
sequence s_a;
@(posedge clk1) $rose(a);
endsequence
sequence s_b;
@(posedge clk2) $rose(b);
endsequence
property p_match;
@(posedge clk2) s_a.matched |=> s_b;
endproperty
a_match: assert property (p_match);
理解“matched”構造的使用方法的關鍵在於，被采樣到的匹配的值一會被保存到另一個序列最近的下一個時鍾邊沿。
1.36 “expect”構造
SVA支持一種叫“expect”的構造，它與Verilog中的等待和構造相似，關鍵的區別在於expect語句等待的是屬性的成功檢驗。expect構造后面的代碼是作為一個阻塞的語句來執行。expect構造的語法於assert構造很相似。expect語句允許一個屬性成功或者是被后使用一個執行塊（action block）。
使用expect構造的實例如下所示。
initial
begin
@(posedge clk);
#2ns cpu_ready = 1’b1;
expect (@(posedge clk) ##[1:16] memory_ready == 1’b1)
$display(“Hand shake successful\n”);
else
begin
$display(“Hand shake failed: exiting\n”);
$finish();
for(i=0; i<64; i++)
begin
send_packet();
$display(“Packet %0d sent\n”,i);
end
end
注意，在信號“cpu_ready”被斷言后，expect語句等待信號“memory_ready”在1~16個周期內的任意周期被斷言。如果信號“memory_ready”如預期的被斷言，那么顯示一個成功信息，並且開始執行“for”循環代碼。如果信號“memory_ready”沒能如預期的被斷言，那么顯示錯誤信息，且模擬結束。
1.37 使用局部變量的SVA
在序列或者屬性的內部可以局部定義變量，而且可以對這種變量進行賦值。變量接着子序列放置，用逗號隔開。如果子序列匹配，那么變量賦值語句執行。每次序列被嘗試匹配時，會產生變量的一個新的備份。
property p_local_var1;
int lvar1;
@(posedge clk) ($rose(enable1), lvar1 = a ) |=> ##4 (aa == (lvar1* lvar1* lvar1));
endproperty
a_local_var1 : assert property (p_local_var1);
屬性p_local_var1 查找“enable1”的上升沿。如果找到，局部變量“lvar1”保存設計中向量“a”的值。在4個周期后，檢查設計的輸出向量“aa”是否與局部變量的值得立方相等。屬性的后續算子等待設計滿足延遲（4個時鍾周期），然后將設計的實際輸出和屬性局部計算值比較。
可以在SVA中保持和操作局部變量，
property p_local_accum;
int lvar1;
@(posedge clk) $rose(start) |=>(enable1 ## enable2, lvar1 = lvar1 + aa ) [*4]##1 (stop && (aout == lvar1) );
endproperty
a_local_accum : assert property (p_local_accum);
屬性p_local_accum檢查下列內容：
（1）在任意給定的時鍾上升沿，如果檢測到信號“start”的上升沿，標志一個有效開始。
（2）在一個周期后尋找一個特定的模型或者子序列。信號“enable1”必須被檢測為高，且兩個周期后，“enable2”應該被檢測為高。這個子序列必須連續重復4次。
（3）在子序列的每次重復中，向量“aa”的值在序列內部被累加。在重復結束時，局部保存着向量“aa”累加4次的值。
（4）在重復結束的下一個時鍾周期，期望信號“stop”為高，且局部變量保存的值與向量“aout”的值相等。
1.38 在序列匹配時調用子程序
SVA可以在序列每次成功匹配時調用子程序。同一系列中定義的局部變量可以作為參數傳給這些子程序。對於系列的每次匹配。子程序調用的執行與它們在序列中的順序相同。
sequence s_display1;
@(posedge clk) ($rose(a), $display(“Signal a arrive at %t\n”,$time);
endsequence
sequence s_display2;
@(posedge clk) ($rose(b), $display(“Signal b arrive at %t\n”,$time);
endsequence
property p_display_window;
@(posedge clk) s_display1 |-> ##[2:5] s_display2;
endproperty
a_display_window: assert property (p_display_window);
1.39將SVA與設計連接
有兩種方法可以將SVA檢驗器連接到設計中。
（1）、在模塊（module）定義中內建或者內聯檢驗器。
（2）、將檢驗器與模塊、模塊的或者一個模塊的多個實例綁定。
有的工程師不喜歡在設計中加任何驗證代碼。在這種情況下，在外部綁定SVA檢驗器是很好的選擇。SVA代碼可以內建在模塊定義的任何地方。
下面的例子顯示了內聯在模塊中的SVA。
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檢驗器與設計代碼分離，那么就需要建立一個獨立的檢驗器模塊。定義獨立的檢驗器模塊，增強了檢驗器的可重用性。下面所示的是一個檢驗器模塊的代碼實例。
module mutex_chk(
input logic clk ,
input logic a ,
input logic b
);
property p_mutex;
@(posedge clk) not (a && b);
endproperty
a_mutex: assert property (p_mutex);
endmodule
注意，定義檢驗器模塊時，它是一個獨立的實體。檢驗器用來檢驗一組通用的信號，檢驗器可以與設計中任意的模塊（module）或者實例（instance）綁定，綁定的語法如下所示：
bind <module_name or instance_name > <checker name > <checker instance name > <design siganls>
在上面的檢驗器例子中，綁定可以用下面的方式實現，
bind inline mutex_chk i2 (a,b,clk);
在實現綁定時，使用的是設計中的實際信號。
比如，我們有一個如下所示的頂層模塊。
module top(...)
inline u1(
.clk(clk ),
.a (a ),
.b (b ),
.d1 (in1 ),
.d2 (in2 ),
.d (out1 )
);
inline u2(
.clk (clk ),
.a (c ),
.b (d ),
.d1 (in3 ),
.d2 (in4 ),
.d (out2 )
);
endmodule
檢驗器mutex_chk可以用下面的方式與頂層中內聯（inline）的兩個模塊實例綁定。
bind top.u1 mutex_chk i1 (a,b,clk);
bind top.u2 mutex_chk i2 (c,d,clk);
與檢驗器綁定的設計信號可以包含綁定實例中的任何信號的跨模塊引用（cross module reference）
1.40 SVA與功能覆蓋
功能覆蓋是按照設計規范衡量驗證狀態的一個標准，它可以分成兩類。
a． 協議覆蓋
b． 測試計划覆蓋
斷言可以用來獲得有關協議覆蓋的窮舉信息。SVA提供了關鍵詞“cover”來實現這一功能，cover語句的基本語法如下所示。
<cover_name> : cover property (property_name)
“cover_name”是用戶提供的名稱，用來標明覆蓋語句，“property_name”是用戶想獲得覆蓋信息的屬性名。例如，在1.39節定義的檢驗器“mutex_chk”，可以如下所示來檢查它的覆蓋率情況。
c_mutex : cover property (property_mutex);
cover語句的結果包含下面的信息：
（1）、屬性被嘗試檢驗的次數。
（2）、屬性成功的次數。
（3）、屬性失敗的次數。
（4）、屬性空成功的次數。
檢驗器“mutex_clk”在一次模擬中的覆蓋日志的實例如下所示。
就像斷言（assert）語句一樣，覆蓋（cover）語句可以有執行塊。在一個覆蓋成功匹配時，可以調用一個函數（function）或者任務（task），或者更新一個局部變量。
至此，SVA的基本語法總結（詳細）到此為止，后面還會繼續出SVA的教程。如有不清楚的地方，歡迎交流：QQ 447574829