Handing reset in SystemVerilog assertions
system-verilog, system-verilog-assertions
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.
Problem
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); ```