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

Question

我想检查变量的当前值是否为“1”，则变量的先前值应该为“0”。我在系统 Verilog 断言中使用 $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两个时钟等于一的值。如果是这样，那么更好的解决方案是将$changeor添加到先行词，这仅当更改且当前值为 1!$stable时才执行检查。cal_frame_mode

$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和 § 16.12.6蕴涵描述和$past
|->|=>