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

including property and sequence . 1 In this example, we have the argument
clk of type event , and also untyped arguments. As in properties, it is legal to
use $inferred_clock and $inferred_disable system functions for checker
argument initialization (Lines 3 and 4 ; see Sect. 8.3 ): these functions return the
inferred values of the clock and reset from the checker instantiation context. By
default clk contains the inferred clock from the checker instantiation context, and
rst contains the inferred reset.
The default statements on Lines 5 and 6 define clk and rst as default clock
and reset for checker assertions. As a result, the values of the clock and reset
inferred at the checker instantiation become known inside the checker. Without these
statements, no clock and reset inference can be achieved inside the checker. This
checker behavior is identical to modules.
The clock clk is passed to the checker as an event 2 (Line 3 ), and not as a signal.
As in the case of properties or sequences we can specify the default value of the
clock to be inferred from the checker instantiation context using system function
$inferred_clock (see Sect. 8.2 ).
The type of reset rst is also inferred from the type of the corresponding actual
argument, but since the previous port is typed, we need to use explicit untyped
declaration on Line 4 . The default value of reset is inferred from the checker
instantiation context using system function $inferred_disable . This is, again,
similar to the reset passing to properties as described in Sect. 8.2 .
As we can see, we do not need to specify parameters for checkers, and this is why
the checkers do not have parameters. We do not need to invent tricks to distinguish
between single and double edge clocking model.
Consider now the assertion modeling code (Lines 14 - 16 ). Notice that we use
always_ff (see Sect. 2.2.1.3 ) instead of always in the module. This is because
the plain always is forbidden in checkers. 3 The formal port clk designates already
the correct event, and we can use it in the event control directly. We do not need
explicitly sample signals on Lines 15 - 16 , because the checker does all the required
sampling correctly.
Let us proceed now to the checker instantiations, shown in Fig. 9.5 .
The checker instantiation syntax (Lines 6 - 8 ) is similar to module instantiation.
c_seqprotocol is the name of the checker, inst1 , inst2 and inst3 are the names
of the checker instances. Checker instantiation semantics is similar to property
instantiation in an assertion. All argument types that can be used with a property,
can also be used with a checker. For example, it is possible to pass sequences to a
checker (see Sect. 9.2.1.4 ).
The checker instantiation inst1 (Line 6 ) is equivalent to the following:
c_seqprotocol inst1(go, done, din, dout, posedge clock, reset);
1 Except arguments with local qualifier, see Sect. 16.2 .
2 Not to be confused with passing events to modules. In case of modules it is possible to pass a
variable of the type event . Here we pass the entire event expression, such as posedge clk by
substitution.