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.