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

// ...
end

end
always_ff @( posedge clock) begin
a1: assert property (@( posedge clock) ok); // Legal
a2: assert property (@( posedge clock) req[i] |=>
ack[i]); // Illegal

end
endmodule :m
There is only one instance of each procedural checker assertion a1 , a2 regardless of
the checker instantiation in the loop. Even though the instantiation of assertion a1
is meaningful, the instantiation of a2 is not because variable i is not visible in the
context where the procedural checker assertion is rewritten. t

The code in checker always procedures should not depend on procedural loop
control variables.

Procedural Checkers with Checker Variables

The behavior of procedural checkers containing checker variables complies with
the rules described thus far: the always procedure in a checker remains a separate
process after instantiation.

Example 14.31. Consider the following instantiation of checker
stable_for_two_ticks defined in Example 9.19 :
module m( input logic clock, reset, logic [7:0] en, ...);
default disable iff reset;

logic cond;
logic [7:0] driver;
// ...
always @( posedge clock) begin
for ( int i = 0; i < 7; i++) begin
if (en[i] && cond) begin
driver[i] <= ...;
stable_for_two_ticks check_driver(driver[i]);
end
end
end
endmodule :m
This is roughly equivalent to the following code:

module m( input logic clock, reset, logic [7:0] en, ...);
default disable iff reset;
logic cond;
logic [7:0] driver;
bit toggle = 1'b0;