In reply to Adarsh Santhosh:
Glad that you brought this up. I relied on memory.
In addition, I also made a mistake, particularly since I
am not an active user of SV and SVA.
As in any language, no use → it fades :)
OK, let’s get this assertion correctly.
// 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
Thanks,
BEn