斷言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