SV -- Assertions 斷言
1.簡介
斷言assertion被放在verilog設計中，方便在仿真時查看異常情況。當異常出現時，斷言會報警。一般在數字電路設計中都要加入斷言，斷言占整個設計的比例應不少於30%。
斷言的作用：
- 檢查特定條件或事件序列的出現情況。
- 提供功能覆蓋
斷言的種類：
- 立即斷言 Immediate Assertions
- 並發斷言 Concurrent Assertions
1.1 立即斷言
立即斷言檢查當前仿真時間的條件，相當於 if else , 需要放在過程塊中。
語法
label: assert(expression) action_block;
其中：
- action block 操作塊在斷言表達式的求值之后立即執行
- 操作塊指定在斷言成功或失敗時采取什么操作
action_block:
pass_statement; else fail_statement;
由於斷言表達式中所斷言的條件必須為真，因此斷言的失敗將具有與之相關的“嚴重”程度。默認情況下，斷言失敗的嚴重程度是一個error。
還有其他可選的fail statement:
（嚴重等級依次遞減）
- $fatal ： a run-time fatal.
- $error ： a run-time error.
- $warning ： a run-time warning
- $info ：information.
例如：
//With Pass and Fail statement; Fail verbosity fatal;
assert(expression) $display(“expression evaluates to true”); else $fatal(“expression evaluates to false”);
立即斷言案例：
module asertion_ex;
bit clk,a,b;
//clock generation
always #5 clk = ~clk;
//generating 'a'
initial begin
a=1;
b=1;
#15 b=0;
#10 b=1;
a=0;
#20 a=1;
#10;
$finish;
end
//Immediate assertion
always @(posedge clk) assert (a && b);
endmodule
output :
ncsim: *E,ASRTST (./testbench.sv,23): (time 15 NS) Assertion asertion_ex.__assert_1 has failed
ncsim: *E,ASRTST (./testbench.sv,23): (time 25 NS) Assertion asertion_ex.__assert_1 has failed
ncsim: *E,ASRTST (./testbench.sv,23): (time 35 NS) Assertion asertion_ex.__assert_1 has failed
Simulation complete via $finish(1) at time 55 NS + 0
1.2 並發斷言
並發斷言檢查跨越多個時鍾周期的事件序列。
- 並發斷言僅在有時鍾周期的情況下出現
- 測試表達式是基於所涉及變量的采樣值在時鍾邊緣進行計算的
- 它可以放在過程塊、模塊、接口或程序定義中
- 區別並發斷言和立即斷言的關鍵字是property
c_assert: assert property(@(posedge clk) not(a && b));
2.SVA (system verilog assertion)
下圖顯示了創建SVA檢查器的步驟:
- Boolean expressions: 基本的邏輯信號組成的布爾表達式
- Sequence: 布爾表達式事件，在一段時間內計算涉及單個/多個時鍾周期的值。SVA提供一個名為“sequence”的關鍵字來表示這些事件。
- 語法：
sequence name_of_sequence;
endsequence
- Property : 一般用來定義一個有時間觀念的斷言，它會常常調用sequence，一些時序操作如“|->”只能用於property, 而不能用於立即斷言。
2.1 Sequence
Sequence 可以帶參數，例如sequence seq_lib (a, b)，可以在其他sequence中例化：seq_lib(req1,req2);
Example:
sequence seq_1;
@(posedge clk) a==1;
endsequence
在SVA中，時鍾周期延遲用“##”符號表示。例如，##2表示2個時鍾周期
sequence seq;
@(posedge clk) a ##2 b;
endsequence
上面代碼表示在上升沿，檢測a是否為1,如果否，則斷言失敗，否則，查看2個周期后的b是否為1，如果是，則斷言通過。
通常，在sequence中不定義時鍾語句，而在property中定義：
sequence seq;
a ##2 b;
endsequence
property p;
@(posedge clk) seq;
endproperty
a_1 : assert property(p);
2.2 Property
property也可以像sequence一樣定義參數，同時也可以在property內部定義變量，如： int a;
另外，如果這么寫 a_3: assert property(@(posedge clk) p) ，如果p中也有clk語句，則不允許。
not的寫法：
sequence seq;
@(posedge clk) a ##2 b;
endsequence
property p;
not seq;
endproperty
a_1: assert property(p);
not表示斷言的內容不發生，也就是要么a不為1，要么a為1但延時2以后b還不為1.
2.2.1 implication
implication只能在property中使用，它的作用如下：
sequence seq;
@(posedge clk) a ##2 b;
endsequence
在上面這段斷言中，表示如果在上升沿a為1，之后2個延時后b也為1，那么斷言成功，而如果a在上升沿就不是1，那么每個這樣的情況都會報error,這可能不是我們希望的。我們可能只想要在a為高之后才進行斷言。
於是就有了implication（蘊含，不知道是不是這么翻譯）。 它的邏輯類似於下面的代碼：
if a then b; else succeed;
因此，一旦 a 發生，b必須發生，斷言才成功。如果a沒發生，走else，同樣成功而不會報錯。
implication分為兩種：
- Overlapped implication （|->) 交疊蘊含
- Non-overlapped implication（|=>) 非交疊蘊含
Overlapped implication （|->):
表示左邊的條件發生時，立即檢查右邊的是否發生。
property p;
@(posedge clk) a |-> b;
endproperty
a: assert property(p);
上面的代碼表示當a為1時，在同一個上升沿檢查b是否為1.
Non-overlapped implication（|=>)：
與上面不同的是|=>表示左邊的條件發生時，在下一個周期檢查右邊的是否發生。
property p;
@(posedge clk) a |=> b;
endproperty
a: assert property(p);
上面的代碼表示當a為1時，在下一個上升沿檢查b是否為1.
timing windows:
property p;
@(posedge clk) a |-> ##[1:4] b;
endproperty
a: assert property(p);
表示在a為高的上升沿后，b需要在1-4個周期內置高。
其中，如果用$代替4：##[1:$]則表示最大時間，也就是直到仿真結束時間。
2.2.2 repetition 重復操作
property p;
@(posedge clk) a |-> ##1 b ##1 b ##1 b;
endproperty
a: assert property(p);
這個斷言表示 a為高的上升沿后，b需要保持三個周期的高
當然，也可以使用下面的寫法：
property p;
@(posedge clk) a |-> ##1 b[*3];
endproperty
a: assert property(p);
2.2.3 go to repetition 跟隨重復
property p;
@(posedge clk) a |-> ##1 b[->3] ##1 c;
endproperty
a: assert property(p);
其中##1 b[->3]表示在a為高的上升沿后，經過一個周期，b在接下來要有三個上升沿為高，而且不一定要連續。但有個要求，就是在##1 c發生之前的上升沿b是剛好完成最后一次匹配
2.2.4 Nonconsecutive repetition 非連續重復
跟上面類似，如果改為：b[=3]，就是非連續重復，區別是，不要求b的最后一次匹配發生在c發生之前。也就是b完成了三次匹配后，可以等若干周期c才發生
2.2.5 throughout
蘊含（implication）是目前討論到的允許定義前提條件的一項技術。例如，要對一個指定的序列進行檢驗，必須某個前提條件為真。也有這樣的情況，要求在檢驗序列的整個過程中，某個條件必須一直為真。蘊含只能在時鍾沿檢驗前提條件一次，然后就開始檢驗后續算子部分，因此它不檢測先行算子是否一直保持為真。為了保證某些條件在整個序列的驗證過程中一直為真，可以使用“throughout”運算符。運算符“throughout”的基本語法如下所示：
（expression）throughout （sequence definition）
示例：
property p31;
@(posedge clk) $fell(start) |->(!start) throughout (##1 ( !a && !b ) ##1 ( c[->3] ) ##1 ( a&&b ) );
endproperty
a31: assert property(p31);
p31檢查下列內容：
- 在信號“start”的下降沿開始檢查。
- 檢查表達式((!a&&!b)##1(c[->3])##1(a&&b))。
- 序列檢查在信號“a”和“b”的下降沿與信號“a”和“b”的上升沿之間，信號“c”應該連續或間斷地出現3次為高電平。
- 在整個檢驗過程中，信號“start”保持為低。
2.2.6 within
“within”構造允許在一個序列中定義另一個序列。
seq1 within seq2
這表示seq1在seq2的開始到結束的范圍內發生，且序列seq2的開始匹配點必須在seq1的開始匹配點之前發生，序列seq1的結束匹配點必須在seq2的結束匹配點之前結束。
2.3 SVA 方法
2.3.1 $rose
sequence seq_rose;
@(posedge clk) $rose(a);
endsequence
當a的最低位從0變為1時（在上升沿），斷言成功。否則失敗。
2.3.2 $fell
sequence seq_fell;
@(posedge clk) $fell(a);
endsequence
與rose相反，斷言a的最低位從1變0.
2.3.3 $stable
@(posedge clk) $stable(a);
斷言a在clk每個上升沿都保持不變。
2.3.4 $past
property p;
@(posedge clk) b |-> ($past(a,2) == 1);
endproperty
a: assert property(p);
提供信號在之前周期的值。例如上面例子斷言在上升沿，b為1時，兩個周期前的a也為1.
此外，$past還有一個gating變量：
@(posedge clk) b |-> ($past(a,2,c) ==1);
上例中c就是這個變量，該斷言判斷在給定的正時鍾邊緣上，如果b為高，那么在此之前的2個周期中，只有當選通信號“c”在時鍾的任意正邊緣上有效時，a才高。
2.3.5 內置系統方法
a_1: assert property( @(posedge clk) $onehot(state) );
a_2: assert property( @(posedge clk) $onehot0(state) );
a_3: assert property( @(posedge clk) $isunknown(bus) ) ;
a_4: assert property( @(posedge clk) $countones(bus)> 1 );
- $onehot(expression)
檢查是否只有一位為高 - $onehot0(expression)
檢查是否只有一位或0位為高 - $isunknown(expression)
檢查是否有任意比特為 X or Z. - $countones(expression)
計數表達式中為高的比特的個數
2.3.6 disable iff
在某些設計條件下，我們不想繼續檢查某些條件是否正確。這可以通過使用禁用iff來實現。
property p;
@(posedge clk)
disable iff (reset) a |-> ##1 b[->3] ##1 c;
endproperty
a: assert property(p);
disable iff后面的條件為停止檢查的判斷條件。上面在reset為低時會檢查a |-> ##1 b[->3] ##1 c，直到reset為高，停止檢查
2.3.7 ended
默認情況下，多重sequence的組合是以個sequence的起始時間作為同步標志的，SVA提供ended結構以sequence的結束時間作為序列同步點。ended的用法如下：
sequence s1;
@(posedge clk) a##1 b;
endsequence
sequence s2;
@(posedge clk) c ##1 d;
endsequence
property p1;
s1|=>s2; //s1的成功匹配點滯后一時鍾周期是s2匹配的起點
endproperty
property p2;
s1|=>##1 s2.ended; //s1成功匹配點滯后兩個時鍾周期是s2成功匹配點，即s1匹配成功則再過兩個時鍾周期s2必須匹配成功
endproperty
property p3;
s1.ended|=>s2; //s1的成功匹配點滯后一時鍾周期是s2匹配的起點
endproperty
property p4;
s1.ended|=> ##1 s2.ended;//s1成功匹配點滯后兩個時鍾周期是s2成功匹配點，即s1匹配成功則再過兩個時鍾周期s2必須匹配成功
endproperty
若使用ended，則sequence必須定義時鍾。關鍵字ended存儲一個反映在指定時鍾處序列是否匹配成功的布爾值。該布爾值盡在同一時鍾內有效。
2.4 Variable Delay
直接使用##v_delay會導致編譯錯誤，因為在斷言中使用變量是非法的。比如下面的例子：
module asertion_variable_delay;
bit clk,a,b;
int cfg_delay;
always #5 clk = ~clk; //clock generation
//generating 'a'
initial begin
cfg_delay = 4;
a=1; b = 0;
#15 a=0; b = 1;
#10 a=1;
#10 a=0; b = 1;
#10 a=1; b = 0;
#10;
$finish;
end
//calling assert property
a_1: assert property(@(posedge clk) a ##cfg_delay b);
endmodule
上面的代碼編譯時會出錯。解決方法是：##4 (“廢話”，var = Signal)，一定要有斷言的話我們就寫“廢話”，例如:data == data等。如果有多個變量要賦值也可以，##4（廢話，變量1賦值，變量2賦值...........）
例如：
sequence delay_seq(v_delay);
int delay;
(1,delay=v_delay);
endsequence