SV-assertion

斷言(assert)是一種描述性語言，經過描述的指望結果來進行仿真驗證。

斷言有一個更加基礎的信息，咱們稱爲屬性(property)，屬性能夠做爲斷言結果，功能覆蓋點，形式檢查和約束隨機激勵生成。

斷言相比較與testcase的仿真驗證，對設計的可見度要求比較高，能夠幫助快速定位錯誤的根源，斷言能夠分佈在設計各個部位。

在項目中使用斷言，有兩種方式(eda tool中都支持)：

　　1) 使用預建的斷言庫，如OVL，

　　2) 使用SVA，PSL等斷言語言來本身描述。(PSL是徹底獨立的斷言語言，SVA被繼承在SV語言中)，

SVA的語言層次結構：

　　

assertion分爲：

　　1) immediate assert，基於simulation event semantics；

　　　　　　assert/assume/cover (expression)  action_block；

　　2) concurrent assert，基於clock semantics；

　　　　　　assert/assume/cover (expression)  action_block；

　　action_block的聲明：

　　　　　　statement | [statement] else statement；

　　immediate assert的action block緊跟着assert執行，就像在procedual block中，(好比active或者NBA region)

　　　　能夠放在任何procedual中，initial，always，task，function。

　　concurrent assert的action block，在當前assert的reactive region執行，因此action block中使用$sampled()採樣信號值，表示evaluate時的信號值。

 

assertion中的property，能夠用來描述design的某一個行爲，必須被例化在assert，assume，cover等編譯選項後，

　　　　　　　　包含在module，interface，package，program，clocking，$unit中。

　　　　　　sequence，用來描述high level property的abort condition或者common start point，一系列的boolean expression。

 

在sva中，一個property表明一個thread，表示一系列event的sequence，可能持續多個cycle。

　　在property沒有start的時候，thread不會起來，以後的check是不會被evaluation的。被認爲是true的。

　　當該property執行結束或者結果已經出錯，property在這個時間點結束。

SV引入了 |->表示overlapping的操做，resulting sequence (consequent) 與causing sequence (antecedent) 在同一個cycle完成。

　　　　  |=>表示non-overlapping的操做，resulting sequence在causing sequence的下一個cycle開始。

 

sequence：隨着時間增長的SV boolean expression。

　　能夠聲明有formal args，local var；

　　method方法有：ended，matched，triggered，這三個方法都表示sequence的結束；

　　儘可能使用named sequence，來增長代碼的可讀性。

　　sequence支持的操做符：

　　　　

 

注意：1) sequence中的formal args是untyped的；formal args能夠是一個signal，sequence，sequence method。

　　　2) sequence中的local var是不能用做setup delay或者repetition ranges的，

 

property：能夠包含formal args，能夠有local var；

　　　　

　　　　property支持的操做符：

　　　　　　

 

注意：1) 一個property_spec不是一個sequence，可是一個sequence能夠是一個property_spec。

　　　2) formal args能夠帶default value。

 

SVA中支持的assertion 語句以及function：

　　

　　

　　

SVA中各個運算符之間的操做，能夠是expression，sequence，property。

　　expression的優先級與logic operate部分相同。

　　sequence之間的優先級：

　　　　

　　property之間的優先級：

　　　　

 

verilog中的#表示延時，delay，##號表示延時若干個clock cycles。

若是implication operator中，antecedent fail，property被hold爲vacuous success。

property中的not operator不能夠和implication operator一同使用，通常只用在sequence組成的property，表示從不true的序列。

sequence中的first_match操做符，用來消除可能發生overlap的assert result：

　　1.若是property中只由一個sequence組成，則包含一個implicit first_match。

　　　　property p_seq;   (a##1 b ##[0:5] c); endproperty

　　2.consequent sequence中默認包含一個implicit first_match。

　　　　property p_seq;  a=>b##[1:2] c ## [0:4] d; endproperty

　　　　property p_seq;  a=>## [0:3] qABC.ended; endproperty

　　first_match主要用在antecedent的sequence中，一個sequence的ended是能夠多觸發的。

　　　　property p_seq; first_match(a##[2:3]b) |-> c;  endproperty

　　　　property p_seq; first_match(qABC.ended) |-> c; endproperty

重複操做符，能夠用於sequence和expression中。

　　consecutive repetitive,  seq[*n], exp[*n]

　　non-consecutive repetive,   seq[=n],  exp[=n]

　　goto repetitive，non-consecutive exact repetitive， seq[->n]，exp[->n]

throughtout, condition over sequence。用來保證boolean condition在sequence有效期間是正確的。

　　 property p_seq; @(posedge clk)  $rose(req) |-> ##[1:4] enable throughout (ack ##[1:$] done); endproperty

　　　　　　其中enable throughout (ack ##[1:$] done)表示一個sequence；

　　　　　　##[1:4] seq表示一個sequence；

intersect, length-match sequence 表示兩個sequence從同一個clock tick 開始而且在同一個clock tick結束。

within, 表示一個sequence在另外一個sequence有效中完成。

and, not-length-matching sequence，兩個sequence同時開始，可是不須要同時結束。

sequence  method：

　　ended，主要用在sequence在single clock assertion中的endpoint；

　　　　ended method方法，在observe region以外是沒有意義的，因此只能用在assert evaluation。

　　　　property p_seq;  @(psoedge clk) dmaWriteBlock(dma_done).ended |-> ##[1:5] cpu_interrupt; endproperty

　　matched，主要用在sequence在multi_clocks assertion中的endpoint；

　　　　將ended的結果進行latch and multi-clock sync，只在第一個clock的observe region有效。

　　　　sequence q_1(a, b);     @(posedge clk)   $rose(a) ##[2:3] b;     endsequence

　　　　sequence q_2;       @(posedge sysclk)   c##1 q_1(a,b).matched[->1]##1 d; endsequence

　　triggered，Level-sensitive control，主要用在disable iff，或者wait sequence.triggered中。

值採樣函數，$stable(exp)，表示該exp的值與上一個clock tick的值相同。

　　property p_seq;    $fell(req_n) |=> ack ##1 $stable(ack)[*0:100] ##1data_valid;   endproperty。

assertion-ctrl system task；

　　$asserton,  $assertoff,  $assertkill。

assert cover中，能夠收集assert更多的結果，主要分爲coverage for properties，coverage for sequences。

　　1.coverage for properties, Number of times attempted, succeeded, failed, vacuous success.

　　2.coverage for sequence, Number of times attempted, matched.

 

assert中的clock定義：

　　1. sequence中定義，

　　　　頂層的clock定義不影響該sequence中的clock定義；

　　　　assert property中仍須要定義clock，該sequence中定義的clock不會變爲property clock。

　　2. concurrent property中定義，

　　3. procedual block中inferred clock，

　　4. 自己property定義在clocking block中，

　　　　clocking block中的input output delay並不影響assert的執行，input，output delay只是對circuit delay的建模。

　　5. 定義default clocking，

　　6，聲明assert的時候顯式指定， assert property (@posedge clk) p_seq);

　　　　若是此時property中也定義了clock，兩個clock必須相同。