Passing reset to SystemVerilog statements

Question

How do the following two properties differ?

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

Completely different.

In p1, Resetnon-synchronous asynchronous. At any time during the evaluation p1, Resetit becomes true, the property is disabled. While Reset is false, each posedge clockhas an attempt to verify what bis true, and then one measure, and cis the truth for an attempt to transmit, otherwise it fails. If at any time the Reset becomes true, all active attempts will be destroyed.

p2, Reset . posedge clock , ~Reset &b , , c - true , . , Reset .

Answer 2

• p1 reset. Reset p1 .
• p2 Reset . , Reset==1 b==0.

.

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