芯片设计：verilog断言(SVA)语法

1、芯片设计：verilog断言（SVA）语法 (2014-01-23 13:51:36)转载标签： verilog sva assertion 断言 it作者：白栎旸        断言assertion被放在verilog设计中，方便在仿真时查看异常情况。当异常出现时，断言会报警。一般在数字电路设计中都要加入断言，断言占整个设计的比例应不少于30%。以下是断言的语法：1. SVA的插入位置：在一个.v文件中：     

2、;           module ABC ();                   rtl 代码                

3、60;  SVA断言                endmodule   注意：不要将SVA写在enmodule外面。2. 断言编写的一般格式是：   【例】 断言名称1：assert property(事件1)       /没有分号     &

4、#160;    $display(".",$time);             /有分号          else          $display(".",$time);  

5、60;          /有分号          断言名称2：assert property(事件2)          $display(".",$time);         

6、60;else          $display(".",$time);   断言的目的是：断定“事件1”和“事件2”会发生，如果发生了，就记录为pass，如果没发生，就记录为fail。注意：上例中没有if，只有else，断言本身就充当if的作用。   上例中，事件1和事件2可以用两种方式来写：   (1) 序列块： sequence name;  

7、60;                   。;                 endsequence   (2) 属性块： property name;    

8、60;                 。;                endsequence    从定义来讲，sequence块用于定义一个事件（砖），而property块用于将事件组织起来，形成更复杂的一个过程（楼）。s

9、equence块的内容不能为空，你写乱字符都行，但不能什么都没有。sequence也可以包含另一个sequence, 如：                    sequence s1;                  

10、;      s2(a,b);                    endsequence  /s1和s2都是sequence块    sequence块和property块都有name，使用assert调用时都是：“assert property(name);”  

11、  在SVA中，sequence块一般用来定义组合逻辑断言，而property一般用来定义一个有时间观念的断言，它会常常调用sequence，一些时序操作如“|->”只能用于property就是这个原因。        注：以下介绍的SVA语法，既可以写在sequence中，也可以写在property中，语法是通用的。3. 带参数的property、带参数的sequence   property也可以带参数，参数可以是事件或信号，调用时写成：assert pr

12、operty (p1(a,b)   被主sequence调用的从sequence也能带参数，例如从sequence名字叫s2，主sequence名字叫s1:          sequence s1;             s2(a,b);        &

13、#160; endsequence4. property内部可以定义局部变量，像正常的程序一样。           property p1;              int cnt;             

14、; .           endproperty【注】在介绍语法之前，先强调写断言的一般格式：    一般，断言是基于时序逻辑的，单纯进行组合逻辑的断言很少见，因为太费内存（时序逻辑是每个时钟周期判断一次，而组合逻辑却是每个时钟周期内判断多次，内存吃不消）。    因此，写断言的一般规则是： time + event，要断定发生什么event，首先要指定发生event的时间，例如每个时钟上升沿

15、+ 发生某事                某信号下降时 + 发生某事5. 语法1：信号（或事件）间的“组合逻辑”关系：   (1) 常见的有：&&, |, !,    (2) a和b哪个成立都行，但如果都成立，就认为是a成立：firstmatch(a|b)，与“|”基本相同，不同点是当a和b都成立时，认为a成立。   (3) a

16、? b:c a事件成功后，触发b，a不成功则触发c6. 语法2：在“时序逻辑”中判断独立的一根信号的行为：     (posedge clk) A事件; 当clk上升沿时，如果发生A事件，断言将报警。   边沿触发内置函数：(假设存在一个信号a)     $rose( a ); 信号上升     $fell( a ); 信号下降     $stable( a ); 信号值不变7

17、. 语法3：在“时序逻辑”中判断多个事件/信号的行为关系：   (1) intersect(a,b) 断定a和b两个事件同时产生，且同时结束。   (2) a within b     断定b事件发生的时间段里包含a事件发生的时间段。   (3) a #2 b        断定a事件发生后2个单位时间内b事件一定会发生。       a #1:3

18、 b    断定a事件发生后13个单位时间内b事件一定会发生。       a #3:$ b    断定a事件发生后3个周期时间后b事件一定会发生。   (4) c throughout (a #2 b)     断定在a事件成立到b事件成立的过程中，c事件“一直”成立。   (5) (posedge clk) a |-> b    断定clk上升沿后，a事件“开始发生”

19、，同时，b事件发生。   (6)  (posedge clk) a.end |-> b  断定clk上升沿后，a事件执行了一段时间“结束”后，同时，b事件发生。   注："a |-> b" 在逻辑上是一个判断句式，即：                    if a  

20、;                     b;                    else        

21、;               succeed;   因此，一旦 a 发生，b 必须发生，断言才成功。如果a没发生，走else，同样成功。       (7)  (posedge clk) a |=> b    断定clk上升沿后，a事件开始发生，下一个时钟沿后，b事件开始发生。   

22、0;     (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个时钟周期内都成立。    

23、;     (posedge clk) a *1:3 断定“ (posedge clk) a”在连续13个时钟周期内都成立。         (posedge clk) a ->3 断定“ (posedge clk) a”在非连续的3个时钟周期内都成立。       举一个复杂点的例子：         

24、0; property ABC;              int tmp;              (posedge clk) ($rose(a),tmp = b) |-> #4 (c = (tmp*tmp+1) #3 d*3;      

25、     endproperty    上例的一个property说明：当clk上升沿时，断言开始。首先断定信号a由低变高，将此时的信号b的值赋给变量tmp，4个时钟周期后，断定信号c的值是4个周期前b2+1，再过3个周期，断定信号d一定会起来，再过3个周期，信号d又起来一次。只有这些断定都成功，该句断言成功。otherwise，信号a从一开始就没起来，则断言也成功。8. 语法4：多时钟域联合断言：一句断言可以表示多个时钟域的信号关系，例如：     &#

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

27、0;    （posedge clk1） a |=> (posedge clk2) b9. 语法5：总线的断言函数   总线就是好多根bit线，共同表示一个数。SVA提供了多bit状态一起判断的函数，即总线断言函数：   (1) $onehot(BUS)      BUS中有且仅有1 bit是高，其他是低。   (2) $onehot0(BUS)     BUS中有不超过1 bit

28、是高，也允许全0。   (3) $isunknown(BUS)   BUS中存在高阻态或未知态。   (4) countones(BUS)=n BUS中有且仅有n bits是高，其他是低。10. 语法6：屏蔽不定态    当信号被断言时，如果信号是未复位的不定态，不管怎么断言，都会报告：“断言失败”，为了在不定态不报告问题，在断言时可以屏蔽。    如： (posedge clk) (q = $past(d)，当未复位时报错，屏蔽方法是

29、将该句改写为：         (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   

30、 （2）【仿真命令加一个-assertdebug】   vsim -assertdebug -novopt testbench    （3）【如果想看断言成功与否的分析，使用打开断言窗口的命令】 view assertions12. 在VCS中加入断言编译和显示功能：    在fsdb文件中加一句话：$fsdbDumpSVA    在VCS编译参数：system "vcs $VCS_SIMULATION" 中加入一些optio

31、ns:           -assert enable_diag           -assert vpiSeqBeginTime           -assert vpiSeqFail      

32、60;    -assert report=路径           -assert finish_maxfail=100*【经验】以下是一些编写断言的经验：1. 断言的目的：传统的验证方法是通过加激励，观察输出。这种方法对案例的依赖严重，案例设计不好，问题不便于暴露。而断言是伴随RTL代码的，不依赖测试案例，而是相对“静态”。例如：我们要测试一个串行数据读写单元，数据线只有一根，先传四位地址，再传数据。（1）案例验证法：写一个地址，再写一段数据

33、，然后读取该地址，看输出的是不是刚才写的数据。（2）断言法：不需要专门设计地址和数据，当发起写时，在地址传输的时间里将地址存储到一个变量里，在数据传输的时间里将数据存储到一个变量里，观察RAM中该地址是否存在该数据就可以了。    断言设计相当于在电脑上把RTL实现的功能再实现一遍。2. 断言中可以包含function和task。而且function经常用于断言，因为有的处理很复杂，而断言又是“一句式”的，无法分成好几句进行表达，所以需要function替断言分担工作。3. 断言允许规定同时发生的事件，就是组合逻辑，你可以写成：a &&

34、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 （废话，变量

35、1赋值，变量2赋值.）5. 关于断言的表达风格：语法介绍的 “a |-> b”，实际上是 “if a, then b”的逻辑，当a不发生，b也不会被判断，该断言自然成功。但当我们的逻辑是        if a1                   if a2     &#

36、160;         then b        该如何用断言表达？ 或许可以写成：“a1 |-> a2 |-> b”，也可以，但常用的表达是：       “a1 && a2 |-> b” 或者 “a1 #3 a2 |-> b”6. 关于断言的时序：时序逻辑的断言需要注意的一个问题：  

37、60;例如：假设当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为单位（因为我在

38、testbench中的单位规定是timescale 1ns/100ps，精度是100ps = 0.1ns），所以$time/10才是ns。 /    wr: assert property(wr_p)    $display("succeed：",$time/10);    else        $display("error: ",$time/

39、10);/断言可以声明一个int数组arr4，/“(posedge clk) !vld_pulse_r0 && !DataIn”是真实的预备条件/“#4 (read=read, arr0 = DataIn)”只是为了在特定时间内赋值，有用的语句是“arr0 = DataIn”，/“read=read”是废话，为了编译通过。/arr赋值完毕后，进入function进行处理，判断实际地址addr跟junc处理过的数据是否相同。/“addr = junc(arr0,arr1,arr2,arr3);”就是junction调用。    proper

40、ty wr_p;        int arr4;        (posedge clk) !vld_pulse_r0 && !DataIn               #4 (read=read, arr0 = DataIn)    

41、60;        #1 (read=read, arr1 = DataIn)             #1 (read=read, arr2 = DataIn)             #1 (read=read, arr3 = DataIn) |=>

42、;            addr = junc(arr0,arr1,arr2,arr3);    endproperty/    function 3:0 junc;        input a,b,c,d;        reg 3:0 a1;        reg 3:0 b1;        reg 3:0 c1;     &#