In reply to Adarsh Santhosh:
I made the following correction above, my apologies
// Assertion states that in the cycle following done, and thereafter the done, a==0 until end of sim
// **** CORRECTION ****
initial BAD_ap: assert property(@(posedge clk)
done[->1] |=> strong(!a[*1:$])); // THIS IS INCORRECT because
// after the 1st !a the consequent completes.
// **** OK **** What you need
initial ap_preferred: assert property(@(posedge clk)
done[->1] |=> always (!a) );
// ON your other question
done[->1] |=> strong( !a[->1] ##1 !a[*0:$]));
// DO THIS instead
// At initialization, when done then starting from the next cycle
// wait for an occurrence of "a".
// In the cycle following the "a", that variable is always ZERO.
// SYntax:
property_expr ::=
... // several options, see 1800
| sequence_expr #-# property_expr // the followed-by operator.
| sequence_expr #=# property_expr
// property that follows a sequence by zero ( the #-#) or one cycle (the #=#) delay,
// starting from the end point of the sequence
| always property_expr
| always [ cycle_delay_const_range_expression ] property_expr
| s_always [ constant_range] property_expr
// Thus, the s_always require a range
module m;
bit clk, done, a;
initial
ap_1: assert property(@(posedge clk)
done[->1] |=> !a[->1] #=# always !a);
endmodule