对于这段代码,我看到两个断言都失败了。似乎禁用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将不再起作用。因为它最近评估了。
disable iff (expr)
中的表达式是异步的,并使用非抽样值。该物业被评估为观察区域的一部分,该区域位于NBA地区之后。
对于第一个断言,rst
在第一次尝试在观察区域中的时间10处评估属性时已经很低。因此,disable iff
不会阻止尝试评估始终失败的属性。
对于第二个属性,rst
的采样值在第一次尝试评估该属性时仍然是1
,因此它也必须失败。
跟进,
我想你可能会担心一个不切实际的案子。重置后前提的可能性有多大?如果确实如此,那么断言应该仍然有效。例如,假设您有一个带有断言的计数器,以检查它在达到最大值时是否翻转
assert property (@ (posedge clk) disable iff (rst) (counter==maxval) |=> (counter ==0) );
如果计数器的复位值是最大值,则不希望断言被禁用。