Checkers - SVA: The Power of Assertions in SystemVerilog - page 190

For example, let, sequence and property declarations may be freely used in
checkers. As a rule, it is recommended to avoid sequence and property declarations
in modules. If sequences and properties used in modules are general enough,
they should be defined in some global place, for example, in a package, to be
also accessible to different modules. If a module uses several specific sequences
and properties, it is better to encapsulate them in a checker to keep the module
code clean. Unlike modules, checkers are natural containers for sequence and
property encapsulation. Another construct natural in checkers are covergroups (see
Sect. 18.3 ). For checker modeling, see Sect. 9.4 .
As modules, checkers may access elements from their enclosing scope through
their hierarchical names, except the following:

￿ Automatic and dynamic variables.
￿ Elements of fork ... join blocks (including join_any and join_none ).
Also, hierarchical references into checkers are forbidden.

Example 9.8. As mentioned above, checkers may reference signals defined in
modules by their hierarchical names. Thus, we can rewrite the checker from
Example 9.1 to address the signal names directly.

module m(...);
logic req, gnt;
...
endmodule :m

module top;
logic clock, reset;
...
m m1(...);
request_granted c1(clock, reset);
endmodule : top

checker request_granted(clk, rst);
a1: assert property (@clk disable iff (rst) m1.req |=> m1.gnt);
endchecker : request_granted
In this example the checker references signals req and gnt declared in module m1
by their hierarchical names, and not through checker ports. This style limits checker
generality and is better to be avoided whenever possible. Its usage is acceptable for
complex checkers dedicated to the verification of large design blocks. t

9.2.2.1 Generate Constructs

Generate constructs in SystemVerilog are used to perform elaboration time actions
to enable flexible tuning of the design at the elaboration time, as described in
Sect. 2.1 . In checkers, the same generate constructs may be used, and the same rules
as everywhere else apply.