什么时候断言“禁用iff”值?

问题描述 投票:1回答:1

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

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将不再起作用。因为它最近评估了。

system-verilog system-verilog-assertions
1个回答
3
投票

disable iff (expr)中的表达式是异步的,并使用非抽样值。该物业被评估为观察区域的一部分,该区域位于NBA地区之后。

对于第一个断言,rst在第一次尝试在观察区域中的时间10处评估属性时已经很低。因此,disable iff不会阻止尝试评估始终失败的属性。

对于第二个属性,rst的采样值在第一次尝试评估该属性时仍然是1,因此它也必须失败。

跟进,

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

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

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

© www.soinside.com 2019 - 2024. All rights reserved.