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

Instance mycheck of checker check in module m1 is not exactly equivalent to
module m1( logic clock, req, ack);
...
a1: assert property (@( posedge clock) req |=> ack);
endmodule :m1
This is because the true name of the assertion upon the check instantiation in
m1 is mycheck.a1 , and not just a1 . The checker introduces its own scope. Since
assigning a hierarchical name, such as mycheck.a1 to an assertion directly in the
module is illegal, the checker instantiation “in place” is rather conceptual than real.
t

9.3.2.2 Context Inference and Name Resolution

As mentioned in Sects. 9.2.1 and 9.2.3 , name resolution and context inference are
done at the point of the checker declaration and not of its instantiation.

Example 9.17. Consider instantiation of checker check from Example 9.16 in

module m2 :
module m2( input logic clock, rst, req, ack);
default disable iff rst;
...
check mycheck(req, ack, posedge clock);
endmodule :m2
There is no inference possible, hence implicitly the disable condition is 0, and
not rst , because reset is resolved at the declaration point. Thus, assertion a1 is
equivalent to
a1: assert property (@( posedge clock) disable iff (0)
req |=> ack);
If the checker were defined in module m2 (see Sect. 9.2.3 ), then rst would be
inferred from the default disable iff statement in m2 , which is visible in the
declaration of check .
module m2( input logic clock, rst, req, ack);
default disable iff rst;

checker check(a, b, event clk);
a1: assert property (@clk a |=> b);
endchecker : check
//...
check mycheck(req, ack, posedge clock);
endmodule :m2
The assertion would be equivalent to
assert property (@( posedge clock) disable iff (rst)
req |=> ack);

t