晶片設計：verilog斷言（SVA）文法

                                                                                                                                                                                          (2014-01-23 13:51:36)

                                                                                                                                                                                                    作者：白栎旸   

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

【注】在介紹文法之前，先強調寫斷言的一般格式：

    一般，斷言是基于時序邏輯的，單純進行組合邏輯的斷言很少見，因為太費記憶體（時序邏輯是每個時鐘周期判斷一次，而組合邏輯卻是每個時鐘周期内判斷多次，記憶體吃不消）。

    是以，寫斷言的一般規則是： time + event，要斷定發生什麼event，首先要指定發生event的時間，例如

每個時鐘上升沿 + 發生某事

                某信号下降時 + 發生某事

5. 文法1：信号（或事件）間的“組合邏輯”關系：

   (1) 常見的有：&&, ||, !, ^

   (2) a和b哪個成立都行，但如果都成立，就認為是a成立：firstmatch(a||b)，與“||”基本相同，不同點是當a和b都成立時，認為a成立。

   (3) a ? b:c ———— a事件成功後，觸發b，a不成功則觸發c

6. 文法2：在“時序邏輯”中判斷獨立的一根信号的行為：

    @ (posedge clk) A事件; ———— 當clk上升沿時，如果發生A事件，斷言将報警。

   邊沿觸發内置函數：(假設存在一個信号a)

     $rose( a );———— 信号上升

     $fell( a );———— 信号下降

     $stable( a );———— 信号值不變

7. 文法3：在“時序邏輯”中判斷多個事件/信号的行為關系：

   (1) intersect(a,b)———— 斷定a和b兩個事件同時産生，且同時結束。

   (2) a within b    ———— 斷定b事件發生的時間段裡包含a事件發生的時間段。

   (3) a ##2 b       ———— 斷定a事件發生後2個機關時間内b事件一定會發生。

       a ##[1:3] b   ———— 斷定a事件發生後1~3個機關時間内b事件一定會發生。

       a ##[3:$] b   ———— 斷定a事件發生後3個周期時間後b事件一定會發生。

   (4) c throughout (a ##2 b)    ———— 斷定在a事件成立到b事件成立的過程中，c事件“一直”成立。

   (5) @ (posedge clk) a |-> b   ———— 斷定clk上升沿後，a事件“開始發生”，同時，b事件發生。

   (6) @ (posedge clk) a.end |-> b ———— 斷定clk上升沿後，a事件執行了一段時間“結束”後，同時，b事件發生。

   注："a |-> b" 在邏輯上是一個判斷句式，即：

                    if a

                       b;

                    else

                       succeed;

   是以，一旦 a 發生，b 必須發生，斷言才成功。如果a沒發生，走else，同樣成功。    

   (7) @ (posedge clk) a |=> b   ———— 斷定clk上升沿後，a事件開始發生，下一個時鐘沿後，b事件開始發生。      

   (8) @ (posedge clk) a |=>##2b ———— 斷定clk上升沿後，a事件開始發生，下三個時鐘沿後，b事件開始發生。

   (9) @ (posedge clk) $past(a,2) == 1'b1 ———— 斷定a信号在2個時鐘周期“以前”，其電平值是1。

   (10) @ (posedge clk) a [*3] ———— 斷定“@ (posedge clk) a”在連續3個時鐘周期内都成立。

        @ (posedge clk) a [*1:3] ———— 斷定“@ (posedge clk) a”在連續1~3個時鐘周期内都成立。

        @ (posedge clk) a [->3] ———— 斷定“@ (posedge clk) a”在非連續的3個時鐘周期内都成立。

   舉一個複雜點的例子：

           property ABC;

              int tmp;

              @(posedge clk) ($rose(a),tmp = b) |-> ##4 (c == (tmp*tmp+1)) ##3 d[*3];

           endproperty 

   上例的一個property說明：當clk上升沿時，斷言開始。首先斷定信号a由低變高，将此時的信号b的值賦給變量tmp，4個時鐘周期後，斷定信号c的值是4個周期前b^2+1，再過3個周期，斷定信号d一定會起來，再過3個周期，信号d又起來一次。。。。。。。隻有這些斷定都成功，該句斷言成功。otherwise，信号a從一開始就沒起來，則斷言也成功。

8. 文法4：多時鐘域聯合斷言：一句斷言可以表示多個時鐘域的信号關系，例如：

                @ （posedge clk1） a |-> ##1 @ (posedge clk2) b

   當clk1上升沿時，事件a發生，緊接着如果過來第二個時鐘clk2的上升沿，則b發生。“##1”在跨時鐘時不表示一個時鐘周期，隻表示等待最近的一個跨時鐘事件。是以此處不能寫成##2或其他。但是可以寫成：

                @ （posedge clk1） a |=> @ (posedge clk2) b

9. 文法5：總線的斷言函數

   總線就是好多根bit線，共同表示一個數。SVA提供了多bit狀态一起判斷的函數，即總線斷言函數：

   (1) $onehot(BUS)      ————BUS中有且僅有1 bit是高，其他是低。

   (2) $onehot0(BUS)     ————BUS中有不超過1 bit是高，也允許全0。

   (3) $isunknown(BUS)   ————BUS中存在高阻态或未知态。

   (4) countones(BUS)==n ————BUS中有且僅有n bits是高，其他是低。

10. 文法6：屏蔽不定态

    當信号被斷言時，如果信号是未複位的不定态，不管怎麼斷言，都會報告：“斷言失敗”，為了在不定态不報告問題，在斷言時可以屏蔽。

    如： @(posedge clk) (q == $past(d))，當未複位時報錯，屏蔽方法是将該句改寫為：

         @(posedge clk) disable iff (!rst_n) (q == $past(d))  //rst是低電平有效

10. 文法6：斷言覆寫率檢測：

name: cover property (func_name)

11. 在modelsim中開啟斷言編譯和顯示功能：

    （1）【編譯verilog代碼時按照system verilog進行編譯】  vlog -sv abc.v

    （2）【仿真指令加一個-assertdebug】   vsim -assertdebug -novopt testbench

    （3）【如果想看斷言成功與否的分析，使用打開斷言視窗的指令】 view assertions

12. 在VCS中加入斷言編譯和顯示功能：

    在fsdb檔案中加一句話：$fsdbDumpSVA

    在VCS編譯參數：system "vcs $VCS_SIMULATION" 中加入一些options:

           -assert enable_diag\

           -assert vpiSeqBeginTime\

           -assert vpiSeqFail\

           -assert report=路徑\

           -assert finish_maxfail=100

***********************************************************************************************

【經驗】以下是一些編寫斷言的經驗：

1. 斷言的目的：傳統的驗證方法是通過加激勵，觀察輸出。這種方法對案例的依賴嚴重，案例設計不好，問題不便于暴露。而斷言是伴随RTL代碼的，不依賴測試案例，而是相對“靜态”。例如：我們要測試一個串行資料讀寫單元，資料線隻有一根，先傳四位位址，再傳資料。

（1）案例驗證法：寫一個位址，再寫一段資料，然後讀取該位址，看輸出的是不是剛才寫的資料。

（2）斷言法：不需要專門設計位址和資料，當發起寫時，在位址傳輸的時間裡将位址存儲到一個變量裡，在資料傳輸的時間裡将資料存儲到一個變量裡，觀察RAM中該位址是否存在該資料就可以了。

    斷言設計相當于在電腦上把RTL實作的功能再實作一遍。

2. 斷言中可以包含function和task。而且function經常用于斷言，因為有的處理很複雜，而斷言又是“一句式”的，無法分成好幾句進行表達，是以需要function替斷言分擔工作。

3. 斷言允許規定同時發生的事件，就是組合邏輯，你可以寫成：a && b，也可以寫成 a ##0 b，不能寫 ##0.5，不支援小數。

4. 斷言是用電腦模仿RTL的運作過程，當RTL功能複雜時，你必須用到變量。斷言中支援C語言的int和數組聲明，但在指派時“不能”寫成：##4 var = Signal，其中var是斷言中的變量，和RTL無關，Signal是RTL中的一個信号。本句是想在第4周期将Signal的值賦給var，以便在後面使用該值。但本句隻有變量指派，沒有對RTL信号的任何斷言，就會報錯，解決方法是：##4 (“廢話”，var = Signal)，一定要有斷言的話我們就寫“廢話”，例如:data == data 等。如果有多個變量要指派也可以，##4 （廢話，變量1指派，變量2指派...........）

5. 關于斷言的表達風格：文法介紹的 “a |-> b”，實際上是 “if a, then b”的邏輯，當a不發生，b也不會被判斷，該斷言自然成功。但當我們的邏輯是

        if a1

        {

           if a2 

              then b

        }

該如何用斷言表達？？？？ 或許可以寫成：“a1 |-> a2 |-> b”，也可以，但常用的表達是：

       “a1 && a2 |-> b” 或者 “a1 ##3 a2 |-> b”

6. 關于斷言的時序：時序邏輯的斷言需要注意的一個問題：

   例如：假設當clk上升沿到來時，b<=a。将上述邏輯寫成斷言時，如果寫成“@(posedge clk) b==a”，看起來和 b<=a一樣，但實際上是錯的。因為當時鐘上升時，b還沒有得到a的值，a還需要一段保持時間。即，斷言中的信号值實際上是時鐘沿到來之前的值，而不是時鐘沿到來後他們将要程式設計的值。是以，b<=a邏輯的斷言應該是：“@ (posedge clk) (a==a,tmp=a) |=> (b==tmp);”

針對上述幾點，舉一個複雜的例子：

斷言wr的功能是檢查串行位址輸入是否正确，串行位址輸入線是 DataIn 。$time傳回值以0.1ns為機關（因為我在testbench中的機關規定是`timescale 1ns/100ps，精度是100ps = 0.1ns），是以$time/10才是ns。

 /

    wr: assert property(wr_p)

    $display("succeed：",$time/10);

    else

        $display("error: ",$time/10);

/

//斷言可以聲明一個int數組arr[4]，

//“@(posedge clk) !vld_pulse_r[0] && !DataIn”是真實的預備條件

//“##4 (read==read, arr[0] = DataIn)”隻是為了在特定時間内指派，有用的語句是“arr[0] = DataIn”，//“read==read”是廢話，為了編譯通過。

//arr指派完畢後，進入function進行處理，判斷實際位址addr跟junc處理過的資料是否相同。

//“addr == junc(arr[0],arr[1],arr[2],arr[3]);”就是junction調用。

    property wr_p;

        int arr[4];

        @(posedge clk) !vld_pulse_r[0] && !DataIn   

            ##4 (read==read, arr[0] = DataIn) 

            ##1 (read==read, arr[1] = DataIn) 

            ##1 (read==read, arr[2] = DataIn) 

            ##1 (read==read, arr[3] = DataIn) |=>

            addr == junc(arr[0],arr[1],arr[2],arr[3]);

    endproperty

//

    function [3:0] junc;

        input a,b,c,d;

        reg [3:0] a1;

        reg [3:0] b1;

        reg [3:0] c1;

        reg [3:0] d1;

        a1 = {3'b0,a};

        b1 = {3'b0,b};

        c1 = {3'b0,c};

        d1 = {3'b0,d};

        junc = a1+(b1<<1)+(c1<<2)+(d1<<3);

        $display(junc);

    endfunction

7. 如果想在SVA中使用類似for(){....}的功能，别忘了文法中介紹的[*3]，這是在斷言中實作for的唯一方式。

                ##4 (廢話, cnt = 0, arr[cnt] = DataIn, cnt++)   //初始化一下，

                ##1 (read==read, arr[cnt] = DataIn, cnt++)[*3]  //循環3次

8. 每句斷言都是一個小程式：如上例，在##4時間點上，(廢話, cnt = 0, arr[cnt] = DataIn, cnt++)就是一個小程式，信号斷言必須是第一句，其他運算按照順序進行。

9. 斷言的變量除了可用C語言中的int，float外，還可以是reg [n:0]等數字電路類型。

10. 注意：

像這種寫法：

    property ept_p;

        @(posedge rd_clk)   ((rd_num == 0) |-> rd_ept)

                         && (rd_ept |-> (rd_num == 0));

    endproperty

是錯誤的，寫了|->，就不能再用 && 等事件組合邏輯了。

解決方法是使用2個斷言，沒更好的方法。