consider a scenario say we want to check that whenever there is a change in sig_a, sig_b must be 0 and the prop is written like this:
property check_sigs;
@(posedge clk_1) disable iff (disable_check)
($change(sig_a) |-> sig_b==0);
endproperty
assume following conditions:
sim starts at t=0ns;
at t=3ns: sig_a changes 0->1 and clk_1 is also turned off right after the posedge (half of clk_1 was visible to check i.e. the posedge :: check image attached)
at t=7ns: the clocks are turned back on and by that time the sig_b which was correctly 0 at the the time of change now comes back to 1, since assertion will be triggered at this point i.e. t=7ns the check is bound to fail in such scenario.
How can we modify the check so that it handles such sampling clks turning of scenarios gracefully?
