system-verilog - Handing reset in SystemVerilog assertions

Question

How are the following two properties different?

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

Very different.

In p1, Reset is asynchronous not sampled. At any time during the evaluation of p1, Reset becomes true, the property is disabled. While Reset is false, there is an attempt at every posedge clock to check that b is be true followed one clock cycle later, c is true for the attempt to pass, otherwise it fails. If at any time Reset becomes true, all active attempts are killed off.

In p2, Reset is synchronously sampled. There is an attempt at every posedge clock to check that ~Reset &b is be true followed one clock cycle later, c is true for the attempt to pass, otherwise it fails. The attempt will fail if Reset becomes true.

Answer 2

• p1 has an asynchronous reset. At any port Reset is high any active p1 threads are aborted.
• p2 only check Reset at the first clock. The assertion fails if Reset==1 or b==0.

Here are are two examples of ways to visual it.

clk   ‾‾‾\__/‾‾‾\__/‾‾‾
Reset _________/‾‾‾‾‾‾‾
b     ‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾
c     ‾‾‾‾‾‾‾‾‾\_______ c is asynchronously reset by Reset in this example
p1          .___        Assertion aborts on posedge Reset
p2          .______↓    Assertion fails

clk   ‾‾‾\__/‾‾‾\__/‾‾‾
Reset ____/‾‾‾‾‾‾‾‾‾‾‾‾
b     ‾‾‾‾‾‾‾\_________
c     ‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾
p1                      Assertion never starts
p2          ↓      ↓    Assertion fails