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

check mycheck(b, negedge clock);
end
end
endmodule :m
This checker instantiation is conceptually equivalent to the following code:

module m( input logic clock, b, en);
// ...
always @( posedge clock) begin
if (en) begin
// ...
end
end
initial
a1: assert property (@( negedge clock) s_eventually b);
endmodule :m
Even though the checker is instantiated in an always procedure of module m ,
assertion a1 is monitored only once. t

Monitoring of procedural checker assertions is done according to the place-
ment of the assertions in the checker, not according to the placement of the
checker instantiation in a module or in an interface.

Checker Instantiation in Procedural Loops

Procedural loops are just a particular case of procedural code, and thus all the rules
of checker instantiation in procedural code are applicable here too. Note, however,
that if a checker actual argument depends on a loop variable, the loop variable should
have automatic lifetime or const ' cast should be applied to the actual argument.
Example 14.29. Consider the following checker instantiation:

checker check(a, b, event clk = $inferred_clock);
a1: assert property (@clk a |=> b);
endchecker : check
module m( input logic clock, logic [7:0] req, ack);
// ...
always @( posedge clock) begin
for ( int i=0;i<8;i++)
if (i != 3) begin
// ...
check mycheck(req[i], ack[i]);
end

end
endmodule :m
According to the instantiation semantics in procedures, the checker instantiation is
conceptually equivalent to