[SVA]SystemVerilog Assertion(SVA)應用指南_systemverilog中assert用法

              SystemVerilog Assertion(SVA)語法總結

       前言：断言assertion被放在verilog设计中，方便在仿真时查看异常情况。当异常出现时，断言会报警。一般在数字电路设计中都要加入断言，断言占整个设计的比例应不少于30%。本文將系統介紹SystemVerilog Assertion的語法。本文可作為新人學習教程，也可供工程技術人員查詢。

1、SVA的插入位置

1.1、在module中完成Assertion開發

module ABC ();
 
  rtl 代码
 
  SVA断言
 
endmodule

• 注意：不要将SVA写在enmodule外面

1.2、Bind SVA to DUT

•  Bind SVA Module To top

bind      top     mutex_chk         u_mutex_chk(<port_connection>);
//關鍵字  top層    SVA module name   SVA module例化名

•  Bind SVA Module To Hierarchy

bind     top.mdsys.mdperisys.u_dma         mutex_chk       u_mutex_chk(<port_connection>);
//關鍵字  bind DUT Hierarchy instance name  SVA module name  SVA instance name

2、 断言编写的一般格式是：

2.1、例一：檢查事件1

assert property(事件1)       //没有分号
 
  $display("........",$time);             //有分号
 
else
 
  $display("........",$time);             //有分号        

 注意：如果else分支没有调用$error()或者$fatal()，那么VCS不会报Error出来，也就是说Offending不会导致Simulation Error。

• 推荐的写法 

assert property(事件1)       //没有分号
  $display("........",$time);             //有分号
else
  $error("........",$time);               //有分号        

2.2、例二：檢查事件2

assert property(事件2)
  $display("........",$time);
else
  $fatal("........",$time);

• 断言的目的是：断定“事件1”和“事件2”会发生，如果发生了，就记录为pass，如果没发生，就记录为fail。注意：上例中没有if，只有else，断言本身就充当if的作用。

2.3、上例中，事件1和事件2可以用两种方式来写

 2.3.1、序列块(sequence)

sequence name;
  ................. ; 
endsequence

2.3.2、属性块(property)

• 在property块中，在蕴含操作符（|->）之后可以使用if() else语句

但是请注意：

1. 蕴含操作符之后直接写if语句，clcok延迟时间写在if语句中
2. 如果在蕴含操作符后面先写延时块，再写if语句，将会导致语法错误
3. 注意if语句和else语句之间没有分号

property name;
  @(posedge clk) disable iff(!rst_n)
  .............. |-> if(<condition>) ##[] statement 
                     esle ##[] statement;
endproperty

property p_if_else; 
  @(posedge clk) 
  ($fell(start) ##1 (a||b)) |-> if(a) (c[->2] ##1 e) 
                                else  (d[->2] ##1 f); 
endproperty 
 
a_if_else： assert property(p_if_else); 

• 从定义来讲，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就是这个原因。     

2.3.3、使用實參和generate自動創建多條Assertion

• 以下為原創內容

property p1(a, b, c, d);
  @(posedge clk) 
  a && b&& c && d;	
endproperty
 
a1: assert property(p1(a1, b1, c1, d1)); 
a2: assert property(p1(a2, b2, c2, d2));
 
generate
  genvar i;
  for(i = 0; i < 20; i = i + 1) begin : assert
    a_gener : assert property(p1(a2, b2, c2, d2)) else $error();
   end
endgenerate

---

注：以下介绍的SVA语法，既可以写在sequence中，也可以写在property中，语法是通用的。

 2.3.4、嵌套的蕴含

• SVA允许使用嵌套的蕴含。当我们有多个门限条件指向一个最终的后续算子
  时，这种构造十分有用。

`define free   (a && b && c && d) 
 
property p_nest; 
  @(posedge clk) 
  $fell(a) |-> ##1 (!b && !c && !d) |-> ##[6：10] `free; 
endproperty 
 
a_nest： assert property(p_nest);

• 同一个属性可以被重写成不使用嵌套蕴含的方式，如下所示 

property p_nest1; 
  @(posedge clk) 
  $fell(a) ##1 (!b && !c && !d)|-> ##[6:10] `free; 
endproperty 
 
a_nest1： assert property(p_nest1); 

3、带参数的property、带参数的sequence

  3.1、property也可以带参数，参数可以是事件或信号

• 调用时写成

assert property (p1(a,b))

  3.3、被主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) 邏輯運算：&&, ||, !, ^

   (2)位運算: &, |, ~

   (3) a和b哪个成立都行，但如果都成立，就认为是a成立：firstmatch(a||b)，与“||”基本相同，不同点是当a和b都成立时，认为a成立。

   (4) a ? b : c ———— a事件成功后，触发b，a不成功则触发c

6、在“时序逻辑”中判断独立的一根信号的行为

 6.1、Clock觸發的事件 

@ (posedge clk) A事件;   //当clk上升沿时，如果发生A事件，断言将报警。

 6.2、边沿触发内置函数(假设存在一个信号a)

$rose( a );        //———— 信号上升
 
$fell( a );        //———— 信号下降
 
$stable( a );      //———— 信号值不变
 
$changed( a )      //---- return 1 if signal changed, === ~$stable(a)

7、Assertion Cycle Delay Range(##[]) 

 7.1、Assertion中循環過程的實現方法 ---> 原創內容

• 所謂連續或不連續，是針對clock而言的，指的是在連續的2T或者nT之內會發生某事
• 非連續指在nT之內（仿真過程中）發生某事即可，不要求是在連續的Clock之內發生
• 所謂連續重複，如下面的例子：事件b發生3次，在b第三次發生時，再過1T，c事件發生，斷言成功；在b第三次發生時，過了2T才看到b發生，則斷言失敗

property goto_repetition_p;
  @(posedge clk) $rose(a) |-> b[->3] ##1 c;
endproperty
 
//成功的例子：
// !a a !b !b b !b !b b !b !b c
//失敗的例子：
// !a a !b !b b !b !b b !b !b b !b c

• 所謂非連續重複，如下面的例子：只要在仿真過程中，b事件發生過3次（不要求在連續的3T），在此之後的nT內c事件發生，則斷言成功

property goto_repetition_p;
  @(posedge clk) $rose(a) |-> b[=3] ##1 c;
endproperty
 
//成功的例子：
// !a a !b !b !b b !b !b b !b !b b c
// !a a !b !b !b b !b !b b !b !b b !b c

8、在“时序逻辑”中判断多个事件/信号的行为关系

• 注："a |-> b" 在逻辑上是一个判断句式，即：

if a
   b;
else
   succeed;

• 因此，一旦 a 发生，b 必须发生，断言才成功。如果a没发生，走else，同样成功。 举一个复杂点的例子：

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从一开始就没起来，则断言也成功。

   再舉一個intersect應用的例子：

property p1;
  @(posdege clk) disable iff(!rst)
   1[*2:5] intersect (a ##[1:$] b ##[1:$] c);
endproperty

9、多时钟域联合断言

• 一句断言可以表示多个时钟域的信号关系，例如：

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

• 当clk1上升沿时，事件a发生，紧接着如果过来第二个时钟clk2的上升沿，则b发生。
• “##1”在跨时钟时不表示一个时钟周期，只表示等待最近的一个跨时钟事件。所以此处不能写成##2或其他。但是可以写成：

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

10、总线的断言函数

• 总线就是好多根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是高，其他是低。
 
(5) $past(signal, cycle_num, 1)   //----return # of cycle past value of signal

11、屏蔽不定态

       当信号被断言时，如果信号是未复位的不定态，不管怎么断言，都会报告：“断言失败”，为了在不定态不报告问题，在断言时可以屏蔽。如：

@(posedge clk) (q == $past(d));                       //当未复位时报错，屏蔽方法是将该句改写为：
 
@(posedge clk) disable iff (!rst_n)  (q === $past(d))  //rst是低电平有效

12、断言覆盖率检测

• 以下內容為原創

name: cover property (func_name);
 
module mutex_chk(a, b, clk, rst_n)
  input clk;
  input rst_n;
  input logic a, b;
  
  property p_mutex;
    @(posedge clk) disable iff (~rst_n)
     not(a && b);
  endproperty
 
  A_mutex : assert property(p_mutex);
  C_mutex : cover property(p_mutex);
 
endmodule
 

13、在modelsim中开启断言编译和显示功能

    （1）【编译verilog代码时按照system verilog进行编译】  vlog -sv abc.v

    （2）【仿真命令加一个-assertdebug】   vsim -assertdebug -novopt testbench

    （3）【如果想看断言成功与否的分析，使用打开断言窗口的命令】 view assertions

14、在VCS中加入断言编译和显示功能

 14.1、在top的initial塊中調用如下函數

initial begin
  $fsdbDumpSVA();
end

 14.2、添加VCS编译参数

vcs  –sverilog +define+ASSERT_ON+COVER_ON<design files and other options> 
     –y $VCS_HOME/packages/sva_cg +libext+.sv  
     +incdir+ $VCS_HOME/packages/sva_cg
     -ntb_opts dtm –assert finish_maxfail=300 -cm assert
 
 
verdi –sverilog –f rtl.f
 
//urgq –dir simv.vdb

 14.3、查看Coverage數據：

firefox `pwd`/urgReport/dashboard.html

15、致謝

 15.1、本文摘自：Link

 15.2、特別鳴謝：白栎旸