1什么是斷言：
斷言就是在模擬過程中依據我們事先安排好的邏輯是不是發生了,假設發生斷言成功。否則斷言失敗。
2斷言的運行分為：預備（preponed）觀察(observed)響應(reactive).
3斷言的分類：並發斷言（基於時鍾）和即時斷言（基於語義）。
4SVA（system Verilogassertions）：塊的建立：
序列：
Sequencename_of_sequence;
<test expression>
Endsequence
Property name _of_ property
<test expression>
Or
<sequence>
Endproperty
Assertions _name: assert property (property_name) ortest_expression;
運行塊：
Assertion_name:
Assertproperty(property_name)
<success message>
Else
<fail message>
注：保持序列獨立於時鍾，屬性中定義時鍾是好的編碼風格。
5 SVA檢測器的步驟：
建立布爾表達式->建立序列表達式->建立屬性->斷言屬性；
6經常使用語句及函數：
$rose()：檢測信號上升沿
$fell(): 檢測信號下降沿
$stable(); 檢測信號是否穩定。
##n：表示延遲N個時鍾周期。
##[n1:n2]:延時在n1到n2個時鍾周期之內。
##[n1:$]:延時在n1到無窮個時鍾周期之內。
not：檢測屬性不為真的情況（禁止屬性）
|->:假設先行算子匹配在同一個時鍾周期檢測興許算子
|=>:假設先行算子匹配在下一個時鍾周期檢測興許算子
ended: 以序列的結尾作為多個序列的連接點
xx？xx:xx：問號表達式與c同樣。
`define true 1:利用true表達式可實現序列延時n個周期。
$past(signal_name, number of clock cycles，[gating signal]):用來檢測n個時鍾周期之前邏輯表達式的值。
Signalor sequence [*n] 連續反復
Signal[->n]：尾隨反復(在其后必須有一個信號使得最后一次反復有效發生在其后邏輯發生之前的時鍾周期)。
Signal[=n]：非連續反復，反復次數為n
and: 兩個序列必須有同樣的起始點。
intersect:兩個序列必須在同樣時刻開始而且結束於同一時刻。
or:當中一個序列成功就可以。
first_match:and or的序列中指定了時間窗，就可能同一檢驗具有多個匹配的情況。
first_match確保僅僅是用第一次序列匹配。
throughout:(expression) throughout (sequence definition)保證某些條件在檢測過程中一直為真。
within:seq1 within seq2。seq1序列的檢測必須包括在seq2的起始點和結束點。
內建系統函數：
$onehot(expression):在隨意給定的時鍾沿，表達式僅僅有一位為高。
$onehot0(expression):有一位或者沒有位為高。
$isunknown(expression):檢查表達式的不論什么位是否為x或者z。
$countones(expression):計算向量中為高的位的數量。
disable iff (expression) <property definition>: 當某些條件為真時則不進行檢測。
matched: 能夠用來檢測第一個子序列的結束點。
expect:屬性成功的檢驗
<cover_name>: cover property (property_name):cover會檢測序列的：被嘗試檢測次數。屬性成功次數；屬性失敗次數；屬性空成功次數。
7一個樣例：
sequences32a;
@(posedgeclk)
((!a&&!b) ##1 (c[->3]) ##1 (a&&b)); //信號a和信號b均為低電平。經過一個時鍾的延時后檢測信號c是否連續出現三次高電平。且c最后一次為高電平時，經過一個時鍾延時信號a和信號b均為高電平。
endsequence
sequences32b;
@(posedgeclk)
$fell(start) ##[5:10] $rose(start); //從start的下降沿開始。經過5-10個時鍾周期start出現上升沿。即start保持低電平5-10個時鍾周期。
endsequence
sequence s32;
@(posedgeclk)
s32a within s32b; //序列s32a 包括在 s32b中。即序列s32b的起始點和結束點包括s32a的起始點和結束點
endsequence
property p32;
@(posedgeclk)
$fell(start) |-> s32;//在start的下降沿馬上檢測s32.
endproperty
a32: assert property(p32);