system-verilog - 何时评估断言 "disable iff"值？

Question

对于这段代码，我看到两个断言都失败了。似乎禁用 iff (value) 的计算晚于表达式本身。有人可以解释一下。

module tb();
reg clk = 1;
always #5 clk = !clk;
reg rst = 1;
always @ (posedge clk)
    rst <= 0;

initial #11ns $finish();

assert property (@ (posedge clk) disable iff (rst) 1 |-> 0);
assert property (@ (posedge clk) rst |-> 0);
endmodule

后续，如何测试这一点:

always_ff @ (posedge clk or posedge rst) begin
    if (rst) q <= 0;
    else q <= d;
end

其中 rst 基于延迟被取消断言:

always_ff @ (posedge clk)
    rst <= rst_a;

似乎禁用 iff 将不再起作用。因为它第一次评估很晚。

Answer 1

disable iff (expr)内的表达式是异步的并使用非采样值。该属性作为观察区域的一部分进行评估，该区域位于 NBA 区域之后。

对于第一个断言，rst在第一次尝试评估观察区域中的时间 10 的属性时，它已经很低了。所以disable iff不会阻止对属性求值的尝试，但总是失败。

对于第二个属性，采样值 rst还在1在第一次尝试评估属性时，它也必须失败。

跟进，

我想你可能会担心一个不切实际的案例。重置后前因成立的可能性有多大？如果它是真的，那么断言应该仍然有效。例如，假设您有一个带有断言的计数器来检查它在达到最大值时是否翻转

assert property (@ (posedge clk) disable iff (rst) (counter==maxval) |=> (counter ==0) );

如果计数器的重置值为最大值，则您不希望禁用断言。