systemverilog assertion 介绍

发表于 | 分类于 ，

在RTL设计或者是使用Formal Verification的工具时， 常用assertion来描述设计意图。本篇就主要介绍一下systemverilog的assertion。

  1. Immediate Assertions

常常用于仿真， 当某个条件满足的时候打印一些debug信息， 相当于if语句, 比如：

1
2
assert (A == B) $display ("OK. A equals B");
  else $error("It's gone wrong");
  1. Concurrent Assertions

这种assertion相当于增加某种约束，下面举两个例子：

1
assert property (!(Read && Write));

代表的是读写不能同时assert

1
assert property (@(posedge Clock) Req |-> ##[1:2] Ack);

上面的assertion经常出现在某种总线协议的握手过程， 表示的是req置位后1-2个clock cycle ack 信号assert。这个表达中的-> 符号解释如下：

  • s1 |-> s2: 如果s1 是match的， 那么s2也必然要match； 如果s1不匹配， 那么这个squence的结果就是true
  • s1 |=> s2: 代表的是s1在下一个clock在进行判断，这种写法等价于下面的描述：
1
2
‘define true 1
s1 ##1 ‘true |-> s2;
  1. 独立申明property和sequence

上面的示例中， property和##[1:2] Ack这种sequence都可以独立申明：

1
2
3
property not_read_and_write;
  not (Read && Write);
endproperty assert property (not_read_and_write);

也可以组合成为更复杂的assertion描述

1
2
3
4
5
6
7
8
9
10
11
12
13
sequence request
   Req;
 endsequence

 sequence acknowledge
   ##[1:2] Ack;
 endsequence

 property handshake;
   @(posedge Clock) request |-> acknowledge;
 endproperty

 assert property (handshake);
  1. assertion clock
1
2
3
4
property p;
  @(posedge clk) a ##1 b;
endproperty
assert property (p);

也可以直接写成：

1
assert property (@(posedge clk) a ##1 b);
  1. 异步复位
1
2
3
4
5
property p1;
  @(posedge clk) disable iff (Reset) not b ##1 c;
endproperty

assert property (p1);
  1. sequence

下面是一些sequence的例子： 其中##符号代表的是延迟指定个数的时钟周期：

1
2
3
4
5
6
a ##1 b               // a must be true on the current clock tick
                      // and b on the next clock tick
a ##N b               // Check b on the Nth clock tick after a
a ##[1:4] b           // a must be true on the current clock tick and b
                      // on some clock tick between the first and fourth
                      // after the current clock tick

*符号代表的是左边sequence描述的重复：(注意带括号的)

1
2
3
4
5
a ##1 b [*3] ##1 c    // Equiv. to a ##1 b ##1 b ##1 b ##1 c
(a ##2 b) [*2]        // Equiv. to (a ##2 b ##1 a ##2 b)
(a ##2 b)[*1:3]       // Equiv. to (a ##2 b)
                      // or (a ##2 b ##1 a ##2 b)
                      // or (a ##2 b ##1 a ##2 b ##1 a ##2 b)

$可以拓展时间窗口， 但是可以没有范围：

1
a ##1 b [*1:$] ##1 c  // E.g. a b b b b c
  1. coverage 描述

可以用cover property来确认某些sequence或者约束在电路中有没有被验证过：

1
2
3
4
5
6
7
8
module Amod2(input bit clk);
  bit X, Y;
  sequence s1;
    @(posedge clk) X ##1 Y;
  endsequence
  CovLavel: cover property (s1);
  ...
endmodule
  1. assertion中的系统函数

$rose , $fell, $stable表示的是某些信号的值是否在两个clock中间变化：

1
2
assert property
  (@(posedge clk) $rose(in) |=> detect);

上述表示的是： 如果in在clock的上升沿由0变成1， 那么下个周期， dedect信号变成1

1
2
assert property
  (@(posedge clk) enable == 0 |=> $stable(data));

上述assert表示的是如果enable=0， 那么data不应该变化

1
2
3
assert property
  (@(posedge clk) disable iff (reset)
                  enable |=> q == $past(q+1));

函数$past表示的是括号中表达式前一个周期的值。此外, 如果expr中只有一个bit是high，$onhot(expr)返回true。

  1. binding

在用assert， assume等property做形式验证是， 我们常常希望property文件和design分开， 那么就可以用binding 把assertion和要验证的设计绑定。

比如说design如下：

1
2
3
module M_v (...);
   // The design is modelled here
 endmodule

针对这个文件写的assert等如下所示：

1
2
3
4
module  M_sva(....)
 	assert property ...
    assume property ...
endmodule

然后就可以用binding 进行绑定

1
2
bind M 
M_sva  M_v (....)