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

Checker Procedures
Straightforward inlining cannot work for checker procedures: it is illegal to have
nested procedures in SystemVerilog. One should regard checker procedures as if
they were instantiated outside the procedural code. Therefore, always procedures in
checkers are sort of screens “protecting” their contents from the procedural code at
the place of the checker instantiation.
Example 14.27. Consider the following checker check instantiated in module m .
checker check(a, event clk);
always_ff @clk
a1: assert property (@clk a);
endchecker : check
module m( input logic clock, b, en);
// ...
always @( posedge clock) begin
if (en) begin
// ...
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
always_ff @( negedge clock)
a1: assert property (@( negedge clock) b);
endmodule :m
The always_ff procedure in the checker screens assertion a1 from the direct
effect of the always procedure in the module: assertion a1 is controlled by
negedge clock and does not depend on the value of en . This behavior is different
from the behavior of static assertion a1 in checker check1 from Example 14.26 . t
Example 14.28. Assertion a1 in the following checker is instantiated in the scope
of an initial procedure.
checker check(a, event clk = $inferred_clock);
initial
a1: assert property (@clk s_eventually a);
endchecker : check
module m( input logic clock, b, en);
// ...
always @( posedge clock) begin
if (en) begin
// ...