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

9.3.1.4 Wildcard Named Association

When the names of several actual and formal arguments coincide, as in module
m4 below, it is convenient to use a wildcard association making all actual and
formal arguments to be connected implicitly by name. Note that in our case it is
incorrect to use only the wildcard association because the clocking event passed
to the checker request_granted check would be clk , and not posedge clk
as intended. We need to explicitly leave the formal argument clk unconnected to
allow using the default value $inferred_clock . We could also explicitly specify
.clk( posedge clk) instead.
module m4( input logic clk, rst, req, gnt, ...);
default clocking @( posedge clk); endclocking
...
request_granted check(. * , .clk());
endmodule :m4

9.3.2 Instantiation Semantics

Roughly speaking, checkers are “inlined” at their instantiation point—the checker
contents are inserted in the place of the checker instance. This is similar to sequence
and property instantiation, but different from a module instantiation and from a
task call.
Actually, checker instantiation is more complicated than straightforward inlining,
hence we need to describe all its subtleties. In this section, we concentrate on
static checker instances, while the peculiarities of procedural checker instances are
discussed in Sect. 14.8 .
A static checker is instantiated by substitution “in place” with reservations
concerning checker object naming, clock and reset inference, name resolution,
argument sampling, and checker variable semantics.

9.3.2.1 Object Naming

Example 9.16. Consider the following code:
checker check(a, b, event clk);
a1: assert property (@clk a |=> b);
endchecker : check
module m1( input logic clock, req, ack);
...
check mycheck(req, ack, posedge clock);
endmodule :m1