$past在系统Verilog断言中的应用

Question

我想检查变量的当前值是否为'1‘，那么变量的前一个值应该是'0’。我在System断言中使用$past。这里我检查的是cal_frame_mode=1，那么它是cal_frame_mode=0的前一个值。我的密码在下面。然而，我看到断言失败了。当我检查波形时，它的行为是正确的。断言标志2时钟后，第一次检查。如何在只检查一个时钟周期后停止此断言？

property p_NOP_2_RX_CAL;
  @(posedge clk)
  (cal_frame_mode==3'b001) |-> ##2 $past(cal_frame_mode)==3'b000;  
endproperty

assert_nop2cal : assert property(p_NOP_2_RX_CAL);

Answer 1

##2的意思是等两个钟。$past的默认值是从当前时钟返回的表达式一个时钟的值(默认情况下，这是在属性中定义的时钟)。因此：

(cal_frame_mode==3'b001) |-> ##2 $past(cal_frame_mode)==3'b000;

相当于：

(cal_frame_mode==3'b001) |-> ##1 cal_frame_mode==3'b000;

您想要的是：(cal_frame_mode==3'b001) |-> $past(cal_frame_mode)==3'b000;，但是我猜您使用##2的原因是为了过滤掉cal_frame_mode，等于两个时钟的一个。如果是这样，那么更好的解决方案是将$change或!$stable添加到前面，这是只在cal_frame_mode更改且当前值为1时才执行的检查。

$changed(cal_frame_mode) && (cal_frame_mode==3'b001) |-> $past(cal_frame_mode)==3'b000;

断言记录在IEEE Std 1800-2012第16节断言中。

§16.9.3采样值函数详细描述了$sample、$rose、$fell、$stable、$changed和$past

§16.12.6含义描述|->和|=>