SVA(system verilog assertions)基礎

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：檢測屬性不為真的情況（制止屬性）

  |->:如果先行算子匹配在同1個時鐘周期檢測后續算子

 |=>:如果先行算子匹配在下1個時鐘周期檢測后續算子

 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]：跟隨重復(在其后必須有1個信號使得最后1次重復有效產生在其后邏輯產生之前的時鐘周期)。

  Signal[=n]：非連續重復，重復次數為n

  and: 兩個序列必須有相同的起始點。

  intersect:兩個序列必須在相同時刻開始并且結束于同1時刻。

  or:其中1個序列成功便可。

  first_match:and or的序列中指定了時間窗，便可能同1檢驗具有多個匹配的情況。first_match確保只是用第1次序列匹配。

  throughout:(expression) throughout (sequence definition)保證某些條件在檢測進程中1直為真。

  within:seq1 within seq2。seq1序列的檢測必須包括在seq2的起始點和結束點。

 內建系統函數：

   $onehot(expression):在任意給定的時鐘沿，表達式只有1位為高。

   $onehot0(expression):有1位或沒有位為高。

   $isunknown(expression):檢查表達式的任何位是不是為x或z。

   $countones(expression):計算向量中為高的位的數量。

disable iff (expression)  <property definition>: 當某些條件為真時則不進行檢測。

matched: 可以用來檢測第1個子序列的結束點。

expect:屬性成功的檢驗

<cover_name>: cover property (property_name):cover會檢測序列的：被嘗試檢測次數；屬性成功次數；屬性失敗次數；屬性空成功次數。

71個例子：

 sequences32a;

   @(posedgeclk)

     ((!a&&!b) ##1 (c[->3]) ##1 (a&&b)); //信號a和信號b均為低電平，經過1個時鐘的延時后檢測信號c是不是連續出現3次高電平，且c最后1次為高電平時，經過1個時鐘延時信號a和信號b均為高電平。

endsequence

 sequences32b;

   @(posedgeclk)

     $fell(start) ##[5:10] $rose(start); //從start的降落沿開始，經過5⑴0個時鐘周期start出現上升沿。即start保持低電平5⑴0個時鐘周期。

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);

生活不易，碼農辛苦
如果您覺得本網站對您的學習有所幫助,可以手機掃描二維碼進行捐贈