In reply to curious_verifier:
I would implement one of those options:
// Option 1
initial begin
ap_enb: assert property(@(posedge clk) $rose(enable)[->1] |=> always(!enable));
ap_enb_aevery10: assert property(@(posedge clk) $rose(enable)[->1] |->
strong (##1 $rose(a) ##1 !a[*9])[*2^31);
// Note: the s_always requires a range. If no range, use the s_eventually
// 1800 syntax:
// s_always [ constant_range] property_expr
// s_eventually property_expr
end
//option 2 $rose (a) |=> !a[*9] ##1 $rose(a);
initial
ap_enb: assert property(@(posedge clk) $rose(enable)[->1] |=> always(!enable) and $rose(a));
// Concurrent assertion
ap_aevery10: assert property(@(posedge clk) $rose(a) |=>
strong(!a[*9] ##1 $rose(a)));
A note on the always
1800’2017: 16.12.11 Always property
Implicit form:__
implicit_always: assert property(p);
Explicit form:
initial explicit_always: assert property(always p);
1800 also states “This is not shown as a practical example, but only for illustration of the meaning of always.”
The always needs a leading clocking event (LCE) prior to the always construct.
Thus,
module p;
bit clk, a ;
always #5 clk = !clk ;
ap_illegal: assert property (always (@(posedge clk) a )); // line 5
// ** Error (suppressible): testbench.sv(5): (vlog-1957)
// The sva directive is not sensitive to a clock. Unclocked directives are not supported.
ap_legal: assert property (@(posedge clk) always (@(posedge clk) a));
ap_legal2: assert property (@(posedge clk) always (a) );
initial begin
#200 ;
$finish();
end
endmodule