何时评估断言“禁用 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) );

如果计数器的复位值是最大值，则您不希望禁用断言。