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

1 checker check1(a, b, c, d,
2 event clk = $inferred_clock, untyped rst = $inferred_disable);
3 default clocking @clk; endclocking
4 default disable iff rst;
5 property p1(x, y);
6 x[ * 2] |-> y;
7 endproperty :p1
8 property p2(x, y);
9 x |-> y[ * 2];
10 endproperty :p2
11 ...
12 checker check2();
13 property p1(x, y);
14 x[ * 2] |-> y[ * 2];
15 endproperty :p1
16 a1: assert property (p1(a, b));
17 a2: assert property (p2(c, d));
18 endchecker : check2
19 check2 check_cd;
20 endchecker : check1

Fig. 9.7 Nested checkers

declared in these scopes and in the higher-level scopes visible inside the checker.
Another reason is to hide the checker from other parts of the design.

Example 9.13. Figure 9.7 shows nested checkers: checker check2 is declared
inside checker check1 .
Even though checker check2 does not have arguments, the arguments and the
other objects of checker check1 are visible in its scope. For example, arguments
a , b , c , and d of check1 , and property p2 declared in check1 are used in
check2 . Property p1 used in assertion a1 (Line 16 ) is a local property of check2
(Lines 13 - 15 ), and not the property p1 declared in checker check1 (Lines 5 - 7 ).
Property p1 of check1 cannot be directly referenced in check2 because property p1
of check2 masks the visibility of property p1 of check1 . If we needed to instantiate
property p1 of check1 in check2 , we have to reference it by its hierarchical name
check1.p1 .
Checker check2 also inherits the default clocking and default reset definitions
from checker check1 (Lines 3 - 4 ), hence clocking event @clk and reset rst are
inferred in assertions a1 and a2 .

t

All objects referenced in a checker are resolved in the scope of the checker
definition, and not in the scope of its instantiation.