Procedural Concurrent Assertions - SVA: The Power of Assertions in SystemVerilog - page 325

// ...
always @( posedge clock) begin
for ( int i = 0; i < 7; i++) begin
if (en[i] && cond) begin
driver[i] <= ...;
a1: assert property (!toggle |-> $stable(driver[i]));
end
end
end
always @( posedge clock)
toggle <= reset ? 1'b0 : !toggle;
endmodule :m
As usual, the real names toggle and a1 have a different hierarchy than in
the inlined version of the checker. Also, the non-blocking assignment to checker
variable toggle is performed in the Reactive region, and not in the Active region as
in modules.
The resulting assertion a1 remains in the scope of the for -loop. In fact, this
assertion is checked for all indices i for which en[i] && cond is true. The
assignment of the checker variable toggle is performed in a separate process, and
does not depend on the values of i and the condition en[i] && cond .
Checker stable_for_two_ticks may be safely instantiated in a procedural
loop because the checker variable does not depend on the loop control variables.
Otherwise, the checker instantiation in the loop would be illegal.

t

If a checker is instantiated in procedural loop, its variables should not depend
on the loop control variables.

Clock Inference in Checker Procedures

Consider the following checker:

checker mycheck(a, event clk);
always_ff @clk begin
a1: assert property (a);
end
endchecker : mycheck
Will a clock be inferred for a1 from the checker procedural context of the
always_ff ? It depends on the actual argument passed to the formal argument clk .
The Rule of Clock Inferencing cannot be applied to @clk . It must instead be applied
after the substitution of the actual argument for clk from the instance of mycheck .
If, for example, the actual argument of clk is posedge clock , then always @clk
becomes always @( posedge clock) . From the Rule of Clock Inferencing it
follows that in this case the assertion infers its clocking event from the always
procedure. Suppose now that the actual argument of clk is just clock , where
clock is not an event variable or clocking block event, hence not an inferable event