Search code examples
system-verilogsystem-verilog-assertions

Handing reset in SystemVerilog assertions

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);
Solution

  • 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.