system-verilog - SystemVerilog 断言中的处理重置

Question

以下两个属性有何不同？

property p1;
    @(posedge clk) disable iff (Reset) b ##1 c;
endproperty

property p2;
    @(posedge clk) (~Reset & b) ##1 c;
endproperty

assert property (p1);
assert property (p2);

Answer 1

非常不一样。

在 p1 , Reset是异步未采样。评价期间随时p1 , Reset变为真，该属性被禁用。当 Reset 为 false 时，每个 posedge clock 都会尝试一次检查 b一个时钟周期后为真，c尝试通过时为真，否则失败。如果在任何时候重置为真，则所有事件的尝试都会被终止。

在 p2 , Reset是同步采样的。每个posedge clock都有一次尝试检查 ~Reset &b一个时钟周期后为真，c尝试通过时为真，否则失败。如果 Reset 尝试将失败变成真的。