SVA用關鍵詞sequence（序列）來表示設計中的邏輯事件。序列的基本語法是：
sequence name_of_sequence
<test expression>
endsequence
許多序列可以邏輯或者有序的組合起來生成更復雜的序列。SVA提供了一個關鍵詞property（屬性）來表示這些復雜的有序行為。屬性的基本語法是：
property name_of_property
<test expression>；or
<complex sequence expressions>
endproperty
屬性必須在模擬過程中被用於斷言(assert)、假設(assume)或覆蓋(cover)語句來發揮作用。
SVA提供了關鍵詞assert來檢查屬性。其基本語法是：
assertion_name: assert property (property_name);
SVA提供了關鍵詞assume來假設屬性。其基本語法是：
assertion_name: assume property (property_name);
SVA提供了關鍵詞cover來衡量協議覆蓋。其基本語法是：
cover_name: cover property (property_name);
上圖表明了SVA語言的基本構成。布爾表達式將設計中的信號組合起來，組成序列。然后序列邏輯或者有序的組合起來得到屬性。最后通過關鍵詞assert,cover和assume指示屬性的具體作用。
2 蘊含操作符
上一小節中序列s2的失敗由兩個原因：(1)a為低電平；(2) a為高電平，b在兩個cycle之后不為高電平。通常我們只關心第二種錯誤，第一種錯誤是一個無效的錯誤信息。因而我們希望通過定義某種約束技術，在檢查的起始點無效時忽略這次檢查。SVA提供了蘊含（Implication）實現這一目的。
蘊含的左邊叫做先行算子(antecedent)，右邊叫做后續算子 (consequent)。當先行算子成功時，后續算子才會被計算；如果先行算子不成功，那么整個屬性被默認為“空成功”。另外要注意的是，蘊含只可用於屬性定義中，不可用於序列中。
蘊含分為兩類：
(1) 交疊蘊含（Overlapped implication）
用符號”|->”表示。如果先行算子匹配，在同一個時鍾周期計算后續算子表達式。也可以加入固定延時”|-> ##2”，表示如果先行算子匹配，在兩個時鍾周期之后計算后續算子表達式。
(2) 非交疊蘊含（Non-overlapped implication）。
用符號”|=>”表示。如果先行算子匹配，在下一個時鍾周期計算后續算子表達式。
利用蘊含，序列s2可以改為更符合我們需要的時序檢查的屬性p3：
property p3
@(posedge clk) a |-> ##2 b; // ##表示時鍾周期延遲
end property
3 SVA檢驗器的時序窗口
上面討論的延遲的例子都是固定的正延遲。延遲也可以用時序窗口的方式定義，從而給延遲限定一個范圍。
例如：
(a&&b) |-> ##[1:3] c;
上述表達式實際上以下面三個線程展開：
(a&&b) |-> ##1 c或
(a&&b) |-> ##2 c或
(a&&b) |-> ##3 c
時序窗口可以用於屬性以及序列。不同的是，第一個成功的線程將使整個屬性成功，並結束這個屬性；而序列可以有多個匹配都能使得序列成功，即第一個成功並不結束這個序列的檢查，序列可以有多個成功的結束點。
時序窗口左邊的值最小為0。時序窗口右邊的值最大為$（它指示一個有限的但無邊界的最大值）。檢驗器不停的檢查表達式是否成功直到模擬結束。如果屬性檢查在模擬結束之前都沒有成功，那么檢查報告為“未完成的檢驗（incomplete check）”。如果序列在模擬結束之前檢查沒有結束，那么檢查報告也為未完成的檢驗。
例如：
sequence s4;
@(posedge clk) a ##[1:3] b;
endsequence
property p4;
@(posedge clk) s4;
endproperty
Ø 大的時間窗口應該使用變量予以限定
當##[M:N]和[*M:N]運算符中的時間間隔很長（如大於20個時鍾周期）時，編譯或運行這樣的運算符要占用很長的時間和很多的資源。
例如，帶長時間間隔的非重疊事務：
a1:assert property(@(clk)start |-> ##[150:256] stop);
可改寫位
logic [10:0] timer=0;
always @(posedge clk) begin:nooverlap
if(reset||stop) timer<=0;
else if(start) timer<=1;
else if(timer!=0 && timer<=255) timer<= timer + 1;
timing:assert property
disable iff(reset)
$rose(stop)||$rose(timer==256)
|-> ((timer>150) && (timer<=255))
)else …；
end:nooverlap
4序列操作符
1重復運算符
SVA語言提供三種不同的重復運算符：連續重復（consecutive repetition），跟隨重復（go to repetition），非連續重復（non-consecutive repetition）。
連續重復
表明信號和序列將在指定數量的時鍾周期內連續的匹配。信號的每次匹配之間都有一個時鍾周期的隱藏延遲。連續重復的重復次數可以是一個窗口。
基本語法如下：
signal or sequence [*n] （n為表達式匹配的次數）
或者signal or sequence [*n:m] （表達式匹配的次數為n~m次）
例如：
property p5;
@(posedge clk) $rose(start) |-> ##2 (a[*3]) ##2 stop ##1 !stop;
endproperty
其中a[*3]可以被展開成：
a ##1 a ##1 a
跟隨重復
表明信號將匹配指定次數，但不一定在連續的時鍾周期上發生。跟隨重復的主要要求是信號的最后一個重復匹配發生在整個序列匹配前的那個時鍾周期。
跟隨重復的基本語法如下：
signal [->n]
非連續重復
表明信號將匹配指定次數，但不一定在連續的時鍾周期上發生。非連續重復不要求信號的最后一個重復匹配發生在整個序列匹配前的那個時鍾周期。
非連續重復的基本語法如下：
signal [=n]
下面舉例說明跟隨重復和非連續重復的區別：
property p6;
@(posedge clk) $rose(start) |-> ##2 (a[->3]) ##1 stop ##1 !stop;
endproperty
property p7;
@(posedge clk) $rose(start) |-> ##2 (a[=3]) ##1 stop ##1 !stop;
endproperty
屬性p6和p7做的檢查為：在任何時鍾上升沿start拉高后開始檢查，兩個時鍾周期后，信號a連續或者間斷的出現3次為高，接着信號stop在下一個時鍾周期為高。p6與p7的唯一區別是，p6要求a第三次為高后的那個時鍾周期stop必須為高，而p7只要求在a的第三個匹配之后，期望一個有效的信號stop，但不必在下一個時鍾周期發生。
p6和p7都有一個未完成的檢查，標記3s標出了檢驗器一個有效的開始，但在模擬結束前，a只重復為高兩次，因而雖然信號stop出現了一次有效，但是模擬結束時這個檢查未能完成。
2選擇運算符
SVA允許在序列和屬性中使用選擇運算符。
例如
property p8;
@(posedge clk) c ? d==a : d==b ;
endproperty
在信號c為高時，檢驗d是否與a相等；在信號c為低時，檢驗d是否與b相等。
.3二元運算符
（1） and運算符
二進制運算符and可以用來邏輯地組合兩個序列。當兩個序列都成功時，檢驗才成功。兩個序列必須具有相同的起始點，但是可以有不同的結束點。檢驗的成功點是后一個成功的序列的匹配點。
例如：
sequence s9a;
@(posedge clk) a ##[1:3] b;
endsequence
sequence s9b;
@(posedge clk) c ##[2:3] d;
endsequence
sequence s9c;
@(posedge clk) s9a and s9b;
endsequence
property p9;
@(posedge clk) s9a and s9b;
endproperty
一個有效的檢驗開始於時鍾周期2。在時鍾周期3時，s9a第一次成功，但必須等待s9b也成功，整個序列的組合才成功。在時鍾周期4時，s9b第一次成功，因此s9c和p9都成功，並且p9結束，但s9c繼續檢查，在時鍾周期5檢驗到另一個成功。
（2）intersect運算符
二進制運算符intersect與and很相似，但它還要求兩個序列必須在相同時刻開始且結束於同一時刻。
（3）or運算符
二進制運算符or可以用來邏輯地組合兩個序列。兩個序列必須具有相同的起始點，但是可以有不同的結束點。只要其中一個序列成功，檢驗就成功。檢驗的成功點是前一個成功的序列的匹配點。
4 first_match 構造
使用了邏輯運算符（如and和or）的序列中如果指定了時間窗，就有可能出現同一個檢驗具有多個匹配的情況。first_match構造可以確保只用第一次序列匹配，而丟棄其他的匹配。這相當於在屬性中定義這個相同的序列。
例如：
sequence s10a;
@(posedge clk) a ##[1:3] b;
endsequence
sequence s10b;
@(posedge clk) c ##[2:3] d;
endsequence
sequence s10c;
@(posedge clk) first_match(s10a or s10b);
endsequence
property p10;
@(posedge clk) s10a or s10b;
endproperty
序列s10c與屬性p10做的是相同的檢查，只保留s10a和s10b的第一次匹配。
5 throughout構造
throughout構造可以保證某些條件在整個序列的驗證過程中一直為真，其基本語法如下：
(expression) throughout (sequence definition)
如果表達式沒有在整個驗證過程中保持為真，即使序列的其他檢驗都正確，也會導致整個檢驗失敗。
6 within構造
within構造允許在一個序列中定義另一個序列。
其基本語法為：
seq1 within seq2
這表示seq1在seq2的開始到結束的范圍內發生，且seq2的開始匹配點必須不晚於seq1的開始匹配點，seq2的結束匹配點必須不早於seq1的結束匹配點。
一個屬性定義了設計的一個行為。一個屬性可以作為一個假設、一個檢查器或者一個覆蓋率規范被用於驗證。為了將這種行為用於驗證，必須使用斷言(assert)、假設（assume）或者覆蓋(cover)語句。一個屬性聲明本身不會產生任何結果。
SVA中有七種類型的屬性：
(1) sequence：由序列構成；
(2) negation：not property_expr；
(3) disjunction：property_expr1 or property_expr2；
(4) conjunction：property_expr1 and property_expr2；
(5) if…else：
if(expression_or_dist)
property_expr1
else
property_expr2
(6) implication：蘊含；
(7) instantiation：屬性的實例可以被用作property_expr或者property_spec。
property_expr ::= sequence_expr | implication_expr
property_spec ::= [clocking_event] [disable iff( expression )] [ not ] property_expr
在序列、屬性中都可以定義時鍾。通常情況下， 在屬性的定義中指定時鍾，並保持序列獨立於時鍾是一種好的編碼風格，這樣可以提高序列的重用性。
SVA提供了關鍵詞disable iff來實現檢驗器的復位，即某些條件為真時，我們不想執行檢驗。其基本語法如下：
disable iff (expression) <property definition>
disable iff只可用在屬性中。
例如：
property p_dis;
@(posedge clk)
disable iff(reset) $rose(start) |=> a[=2] ##1 !start;
endproperty
SVA提供了下列系統函數來訪問一個表達式的采樣值。
(1) $rose(boolean expression or signal_name)：
當信號/表達式的最低位變成1時返回真。
(2) $fell(boolean expression or signal_name)：
當信號/表達式的最低位變成0時返回真。
(3) $stable(boolean expression or signal_name)：
當信號/表達式不發生變化時返回真。
(4) $past(signal_name, number of clock cycle,gating signal)：
得到信號在幾個時鍾周期之前的值。這個函數能夠有效的驗證設計到達當前時鍾周期的狀態所采用的通路是正確的。並且past可以由門控信號（gating signal）控制。
例如：property p_past;
@(posedge clk) (c&&d) |->($past((a&&b),2,e)==1’b1);
endproperty
當門控時鍾e在任意給定的時鍾上升沿有效時，檢驗如果表達式(c&&d) 為真，那么兩個周期前，(a&&b)為真。
SVA還提供幾個內建的函數來檢查一些最常用的設計條件。
(1) $onehot(expression)：在任意給定的時鍾沿，表達式只有一位為高。
(2) $onehot0(expression)：在任意給定的時鍾沿，表達式只有一位為高或者沒有任何位為高。
(3) $isunknown(expression)：在任意給定的時鍾沿，表達式的任何位是否是x或者z。
(4) $onehot(expression)：在任意給定的時鍾沿，計算向量中為高的位的數量。
2.8.1在序列和屬性中使用形參
通過在序列中定義形參，相同的序列可以被重用到設計中具有相似行為的信號上。例如，我們可以定義下面的序列：
sequence s_lib1(a,b)
a||b;
endsequence
我們可以通過下面這個序列調用上面的序列：
sequence s_lib1_inst1
s_lib1(req1, req2);
endsequence
同樣，與序列聲明一樣，一個屬性在聲明的時候可以帶有可選的形式參數。當一個屬性被實例化的時候，實參可以被傳遞到屬性。通過使用實參替代形參，實參使得屬性得到了擴展。例如，我們可以定義下面的屬性：
property arb(a,b,c);
@(posedge clk) $fell(a) |-> ##1 (c&&d)[*4] ##1 b;
endproperty
下面三個斷言都可以調用屬性arb：
a1_1:assert property(arb(a1,b1,c1,d1));
a1_2:assert property(arb(a2,b2,c2,d2));
a1_3:assert property(arb(a3,b3,c3,d3));
2.8.2使用參數的SVA檢驗器（module）
SVA檢驗器模塊中可以使用參數，這為創建可重用的檢驗器模塊提供了很大的靈活性。
SVA檢驗模塊如下：
Module generic_chk(input logic a,b,clk)
parameter delay=1;
property p1;
@(posedge clk) a |-> ##delay b;
endproperty
a1:assert property(p1);
endmodule
以下兩個generic_chk的實例：
generic_chk #(.delay(2)) i1(a,b,clk); //將延遲參數改寫為2個cycle
generic_chk i2 (c,d,clk); //使用默認的1個cycle
在序列或者屬性的內部可以局部定義變量。局部變量能夠在需要的時候在一個序列或者屬性實例中動態地產生並能在序列結束的時候移除。變量的賦值接着子序列放置，用逗號隔開。
例如：
sequence s0;
int lvar;
@(posedge clk)
$rose(start) |=> (enable, lvar = lvar+aa)[*4] ##1 (stop&&(aout= lvar));
endsequence
序列在start拉高后開始有效的檢查，序列中的局部變量lvar在每次enable匹配時，累加aa的值，並在序列結束匹配點處檢查lvar是否與aout相等。
在上例中，局部變量在序列的實例中是不可見的。如果要使得子序列的局部變量可以被上層序列訪問，必須聲明一個局部變量並通過一個自變量傳遞到被實例化的子序列。
sequence s1(lvar);
@(posedge clk)
$rose(start) |=> (enable, lvar = lvar+aa)[*4] ##1 (stop&&(aout= lvar));
endsequence
sequence s2;
int v1;
c ##1 s1(v1) ##1 (do1 == v1);
endsequence
任務、任務線程、void函數、void函數線程以及系統任務（tasks, task methods, void functions, void function methods, and system tasks）可以在一個序列成功匹配的結束處調用。子程序調用，出現在緊跟着序列的以逗號分割的列表中。
舉例說明：
sequence s1;
logic v, w;
(a, v = e) ##1
(b[->1], w = f, $display("b after a with v = %h, w = %h\n", v, w));
endsequence
在序列s1中定義了局部變量v和w，當a為高電平時，把向量e的值賦給v；然后b出現一次高電平時，把向量f的值賦給w，並調用系統任務進行打印。
任務、任務線程、void函數、void函數線程以及系統任務（tasks, task methods, void functions, void function methods, and system tasks）可以在一個序列成功匹配的結束處調用。子程序調用，出現在緊跟着序列的以逗號分割的列表中。
舉例說明：
sequence s1;
logic v, w;
(a, v = e) ##1
(b[->1], w = f, $display("b after a with v = %h, w = %h\n", v, w));
endsequence
在序列s1中定義了局部變量v和w，當a為高電平時，把向量e的值賦給v；然后b出現一次高電平時，把向量f的值賦給w，並調用系統任務進行打印。
SVA中提供了兩種方法將一個復雜序列分解成較為簡單的子序列。一種方法是以序列的起始點作為同步點，另一種方法是以序列的結束點作為同步點。后一種方法通過為序列名字追加上關鍵詞ended來表示。
舉例說明：
sequence s0;
@(posedge clk) a ##1 b;
endsequence
sequence s1;
@(posedge clk) c ##1 d;
endsequence
property p0;
s0 |=>s1;
endproperty
property p1;
s0.ended |-> ##2 s1.ended;
endproperty
屬性p0和p1做的是相同的檢查。p0是以序列的起始點作為同步點，序列s1從s0匹配后的一個時鍾周期開始檢驗；p1是以序列的結束點作為同步點，序列s1的結束匹配時間必須在s0的結束匹配時間之后的2個時鍾周期。
使用ture表達式，可以在時間上延長SVA檢驗器，能夠使得序列的結束點延長一個時鍾周期。這可以用來實現同時監視多個屬性且需要同時成功的復雜協議。
例如：
sequence s0;
@(posedge clk) a ##1 b;
endsequence
sequence s0_ext;
@(posedge clk) a ##1 b ##1 ‘true;
endsequence
sequence s1;
@(posedge clk) c ##1 d;
endsequence
property p0;
@(posedge clk) s0.ended |-> ##2 s1.ended;
endproperty
property p1;
@(posedge clk) s0_ext.ended |=> s1.ended;
endproperty
屬性p0和p1做的是相同的檢查。序列s0_ext的成功匹配點比s0往后移了一個時鍾周期。因此屬性p0檢查s0與s1成功匹配點是否相隔兩個時鍾周期，屬性p1檢查s0_ext與s1成功匹配點是否相隔一個時鍾周期。
SVA允許序列或者屬性使用多個時鍾定義來采樣獨立的信號或者子序列。
2.13.1多時鍾序列
多時鍾序列由單時鍾序列通過延遲連接符號##1連接而成。連接符號##1是非交疊的，並且能夠同步不同子序列的時鍾域。它表示從第一個單時鍾序列的結束點，到第二個單時鍾序列的起始點。當一個序列中使用了多個時鍾信號時，只允許使用##1延遲構造。
例如：
sequence s_mul_clk;
@(posedge clk1) a ##1 @(posedge clk2) b;
endsequence
序列s_mul_clk做的檢查是：當信號a在時鍾clk1的任意給定上升沿為高時，序列開始匹配，接着查找clk2的最近的上升沿，檢查b是否為高。clk1的時鍾周期3開始第一次有效的檢查，查找clk2的最近的上升沿為其時鍾周期2，檢測到b為高，檢查成功；clk1的時鍾周期7開始第二次有效的檢查，查找clk2的最近的上升沿為其時鍾周期3，檢測到b為低，檢查失敗。
多時鍾序列只能用延遲連接符號##1連接單時鍾序列。注意的是以下的序列都是非法的：
@(posedge clk1) s1 ##0 @(posedge clk2) s2
@(posedge clk1) s1 ##2 @(posedge clk2) s2
@(posedge clk1) s1 intersect @(posedge clk2) s2
2.13.2多時鍾屬性
多時鍾屬性的檢查規則和多時鍾序列相同。多時鍾屬性除了使用延遲連接符號##1，還可以對單時鍾序列使用非交疊蘊含運算符。要注意的是，並不是不允許在多時鍾序列中使用交疊蘊含運算符，只是不允許將其連接兩個時鍾定義不同的單時鍾序列。例如，下面的語句就是合法的：
@(posedge clk0) s0 |-> @(posedge clk0) s1 ##1 @(posedge clk1) s2
多時鍾屬性也可以使用邏輯運算符（and,or,not）連接兩個單時鍾序列。
2.13.3 matched構造
如果一個序列中定義了多個時鍾，構造matched可以用來監測子序列的結束點。
例如：
sequence e1;
@(posedge clk1) (a ##1 b ##1 c) ;
endsequence
sequence e2;
@(posedge clk2) start ##1 e1.matched ##1 stop;
endsequence
信號start在clk2的時鍾周期2為高，然后我們檢測到序列e1在clk2的時鍾周期3出現一次匹配，並且在clk2的時鍾周期4信號stop為高，因此在clk2的時鍾周期4出現序列e2的第一次成功；clk2的時鍾周期5開始第二次有效的檢驗，但是在clk2的時鍾周期6我們沒有檢測到序列e1的成功匹配點，因此在clk2的時鍾周期6出現序列e2的失敗。
理解matched構造的使用方法的關鍵在於，被采樣到的匹配的值一直被保存到另一個序列最近的下一個時鍾邊沿。
SVA提供了關鍵詞assert來檢查屬性，assert語句的基本語法是：
assertion_name: assert property(property_name);
執行塊可以在屬性成功或者失敗后執行某些語句。
執行塊的基本語法如下：
assertion_name:
assert property (property_name)
<success message>;
else
<fail message>;
執行塊可以用來顯示成功和失敗。
有兩種方法可以將SVA檢驗器連接到設計中：
（1） 在模塊定義中內建或者內聯檢驗器。
（2） 將檢驗器模塊與模塊、模塊的實例或者一個模塊的多個實例綁定。
檢驗器模塊用來檢驗一組通用的信號，檢驗器可以與設計中任何的模塊或者實例綁定。定義獨立的檢驗器模塊，增強了檢驗器的可重用性。
綁定的語法如下：
bind <module_name or instance_name>
<checker name> <checker instance name>
<design signals>;
舉例說明綁定的使用：
下面為檢驗器模塊的代碼：
module mutex_chk(a,b,clk)
logic a,b,clk;
property p1;
@(posedge clk) not(a&&b);
endproperty
endmodule
有如下所示的頂層模塊：
module top(..);
inline u1(clk,a,b,in1,in2,ou1);
inline u2(clk,c,d,in3,in4,ou2);
endmodule
綁定的語句如下：
bind top.u1 mutex_chk i1(a,b,clk);
bind top.u2 mutex_chk i1(c,d,clk);
功能覆蓋分為兩類：對屬性的覆蓋和對序列的覆蓋。
對屬性覆蓋的cover語句的結果包含下面的信息：
(1) 屬性被嘗試檢驗的次數
(2) 屬性成功的次數
(3) 屬性失敗的次數
(4) 屬性空成功的次數（由於使用蘊含）
例如得到如下的屬性覆蓋報告：
c0, 596 attempts, 202 match, 51 vacuous match（真正成功的次數為match的次數減去vacuous match的次數）
對序列覆蓋的cover語句的結果包含下面的信息：
(1) 序列被嘗試檢驗的次數（attemps）
(2) 所有成功的次數（total match）
(3) 初次成功的次數（first match）
(4) 序列空成功的次數（vacuous match）（總是為0，因為序列中不允許使用蘊含）
例如得到如下的序列覆蓋報告：
c1, 596 attempts, 361 total match, 151 fisrt match, 0 vacuous match
序列中如果指定了時間窗，就有可能出現同一個檢驗具有多個匹配的情況。total match就包括了所有的成功，而first match只包括檢驗的第一次匹配。
SVA提供了關鍵詞cover來衡量協議覆蓋。其基本語法是：
cover_name: cover property (property_name or sequence_name);
通過運用cover語句我們可以得到屬性或者序列的執行情況。我們可以把我們希望發生的情景表達成屬性或者序列，並通過檢測所有屬性或者序列的檢驗至少真正成功一次，來實現功能覆蓋。利用與assert語句中一樣的執行塊，我們可以控制模擬環境和收集功能覆蓋數據。
下面以一個請求情景（Request Scenario）為例。
在任何給定的時間，有三個主控設備可以請求訪問總線。這就意味着主控設備的req信號有七種可能的組合（0表示主控設備正在請求總線）。
測試平台應該生成上表中所有的輸入組合。
七個屬性定義了上表中的所有可能的請求組合。每個屬性都與cover語句相連。我們期望每個請求組合都出現三次，因此我們只要檢測七個屬性是否都被成功檢測到三次。並且，我們可以利用flag標志位來控制模擬環境，例如所有組合都檢測到三次后就終止模擬。
要注意的是，每次屬性或者序列的匹配都會執行action block在中的語句，如果在某一時鍾周期同時產生了多個匹配，那么這個語句就會相應的被執行多次。
在形式驗證和動態仿真中，assume語句將屬性指定為環境中的假設。當一個屬性被假設，工具會約束環境使得屬性的檢驗得到滿足。
在形式驗證中，被假設的屬性不會被強制滿足檢驗。被假設的屬性可以認為是被斷言的屬性的前提假設（hypothesis）。
在動態仿真中，環境必須被約束使得被假設的屬性滿足檢驗。和被斷言的屬性一樣，被假設的屬性也要被檢查，並且在失敗時報錯。
舉例說明assume語句的使用：
檢查信號req的屬性如下：
property pr1;
@(posedge clk) !reset_n |-> !req; //when reset_n is asserted (0),keep req 0
endproperty
property pr2;
@(posedge clk) ack |=> !req; // one cycle after ack, req must be deasserted
endproperty
property pr3;
@(posedge clk) req |-> req[*1:$] ##0 ack;
// hold req asserted until and including ack asserted
endproperty
檢查信號ack的屬性如下：
property pa1;
@(posedge clk) !reset_n || !req |-> !ack;
endproperty
property pa2;
@(posedge clk) ack |=> !ack;
endproperty
在假設斷言a1, assume_req1,assume_req2, and assume_req3一直滿足的前提下，檢查斷言assert_ack1和assert_ack2是否滿足檢驗。
a1:assume property @(posedge clk) req dist {0:=40, 1:=60} ;
assume_req1:assume property (pr1);
assume_req2:assume property (pr2);
assume_req3:assume property (pr3);
assert_ack1:assert property (pa1)
else $display("\n ack asserted while req is still deasserted");
assert_ack2:assert property (pa2)
else $display("\n ack is extended over more than one cycle");
要注意的是assume語句不能使用執行塊，因為執行語句對於假設來說沒有意義。
SVA支持expect構造，它等待屬性的成功檢驗，並將except構造后面的代碼作為一個阻塞的語句來執行。expect語句允許在一個屬性成功或者失敗后使用一個執行塊。
舉例說明：
program tst;
initial begin
# 200ms;
expect( @(posedge clk) a ##1 b ##1 c ) else $error( "expect failed" );
ABC ...
end
endprogram
上例中，在expect語句失敗后打印失敗信息，並且語句ABC要等待expect語句檢驗成功或者失敗后才執行。