systemverilog中的assertion用法整理

时序电路讲究建立时间、保持时间需要留有裕量。这也说明了，在电路中信号的顺序以及之间的时序关系十分重要

如果激励的输入输出不满足设计的要求，那么测试的结果也是不可靠的。同样，如果设计内部不满足要求，输入输出的关系也不正确。为了检验这之间的关系，便引入了assertion.

由参考资料可知几点，非时序逻辑时，assertion的形式如下：

ASSERTION_TEST:
 assert (condition)
 else
  $error("check failed");

而对于时序逻辑的assertion，形式如下:

ASSERTION_TEST:
 assert
  property(
  @(posedge clk) disable iff (rst)
   condition
  )
  else
   $error("check failed");

或

property ASSERTION_TEST:
  @(posedge clk) disable iff (rst)
   condition
  )
endproperty

ASSERTION_ACTION: assert property (ASSERTION_TEST)

其它的一些系统函数，操作符作用如下，可以进参考资料查看：

那么，接下来我们就做个小测试，使用req ack的握手过程作为检测过程。

信号的时序图要求如上图，握手过程为：

1. req信号拉高，此时ack信号还是低电平
2. 在req信号拉高后，ack信号拉高
3. req端检测到ack拉高，拉低req信号
4. ack端的处理结束，检测到req信号拉低，ack信号拉低

那么，我们简单写一个ack应答的模块，内容如下：

module req2ack(
  input  clk ,
  input  rst ,

  input  en  ,
  input  req ,
  output reg ack 
);

reg [7:0] req_arr;

always @ (posedge clk or posedge rst)
begin
 if (rst)
  req_arr <= 'd0;
 else if (en)
  req_arr <= {req_arr[5:0], {2{req}}};
end

always @ (posedge clk or posedge rst)
begin
 if (rst) 
  ack <= 1'b1;
 else if (en)
  ack <= req_arr[7] ; 
end

endmodule

req经过8个时钟周期和使能信号的延迟后，ack做出应答。

tb简单写为：

module tb;

reg clk ;
reg rst ;
reg en  ;
reg req ;
wire ack;

initial begin
 clk = 0;
 rst = 1;
 en  = 0;
 req = 0;
 #100
 rst = 0;
 en  = 1;
 #100
 req = 1;
 wait(ack);
 req = 0;
 #50
 req = 1;
 #20
 req = 0;
 #50
 $finish;
end

initial begin
 $fsdbDumpfile("tb.fsdb");
 $fsdbDumpvars;
 $fsdbDumpSVA;
end

always #10 clk = ~clk;

req2ack req_inst(
  .clk(clk) ,
  .rst(rst) ,
  .en (en ) ,
  .req(req) ,
  .ack(ack) 
);

`ifdef ASSERTION_ENABLE
 `include "tb_assertion.v"
`endif

endmodule

提供20ns的周期时钟，使能信号；以及两次req信号拉高的模拟激励。

assertion定义在tb_assertion.v文件中，在仿真时定义ASSERTION_ENABLE的宏，可以调用assertion检查。

tb_assertion.v定义为：

check_req_ack_rise:
    assert property(
 @(posedge clk) disable iff (rst)
  $rose(req) |- > ##1 (req & ~ack)[*0:$] ##1 (req & ack)
 )
 else
   $error("req to ack rising edge is fail");

check_req_ack_fall:
    assert property(
 @(posedge clk) disable iff (rst)
  $rose(ack) |- > (req & ack)[*0:$] ##1 (~req & ack)[*0:$] ##1 (~req & ~ack)
 )
 else
  $error("req to ack falling edge is fail");

第一块内容，检查req-ack握手过程的1，2两步；第二块内容，检查req-ack握手过程的3，4步。

$rose(req)的意思是由上文或参考资料可知，等到req信号的上升沿有效；

|->操作符表示，LHS(左侧表达式)条件满足，则在同一时刻去检查RHS的表达式；

##1 代表延时1个时钟周期；

(req & ~ ack)[*0:$] 代表此时req信号为高，ack信号为低的情况满足0或多个时钟周期；周期不确定

第一块内容的意思是，等到req信号上升沿，过一个时钟周期检查req拉高，ack为低的情况是否满足，这个过程可能持续多个周期，不确定；然后就是ack信号拉高。检查结束

第二块内容的意思是，等到ack信号上升沿，检查req和ack的信号是否都拉高，这个过程可能持续多个周期，不确定；然后req信号拉低，ack保持，也会持续多个周期，最后ack信号也拉低。

最后，在运行vcs时，需要加入“+fsdb+sva_success -assert”

测试结果：

那么，我们对激励稍作修改下：

initial begin
 clk = 0;
 rst = 1;
 en  = 0;
 req = 0;
 #100
 rst = 0;
 en  = 1;
 #100
 req = 1;
 wait(ack);
 #20
 req = 0;
 wait(~ack);
 #50
 $finish;
end

Assertion的结果：

这只是作为一个小例子，而且写的过于匆忙，我相信应该是有更好的assertion写法，所以权当是一次记录的草稿内容。