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

14.8 Procedural Checker Instances

Checkers are generalizations of concurrent assertions that also serve as containers
for verification code that supports the assertions. As such, it is desirable to be able to
instantiate checkers wherever concurrent assertions can be written, including within
procedures. Supporting this capability comes with some challenges to define how
various checker constructs interact with the surrounding procedural context. The
instantiation rules formulated for static checker instances hold also for procedural
checker instances, but there are additional rules applicable to procedural instances,
as well as considerations for their effective use. These are the subjects of this section.

Static Assertions

Static assertions in a checker declaration (i.e., those checker assertions that are not
in the scope of any checker procedure) become procedural assertions as the result
of a procedural instantiation of the checker.

Example 14.26. Assertion a1 is static in checker check1 :
checker check1(a, event clk = $inferred_clock);
a1: assert property (@clk a);
endchecker : check1
The instantiation c1 of checker check1 in module m
module m( input logic clock, b, en, ...);
// ...
always @( posedge clock) begin
if (en) begin
// ...
check1 c1(b);
end
end
endmodule :m
is conceptually 3 equivalent to
module m( input logic clock, b, ...);
// ...
always @( posedge clock) begin
if (en) begin
// ...
a1: assert property (@( posedge clock) b);
end
end
endmodule :m
That is, the static assertion a1 in checker check1 behaves as a procedural assertion
in checker instantiation c1 in module m .

t

3 We use the term “conceptually” because of the hierarchical assertion naming in the checker, as
explained in Sect. 9.3.2 .