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

9.4 Checker Modeling

9.4.1 Checker Variables

Assertion modeling code in checkers is similar to that of hardware modeling in
modules and interfaces: one can declare variables in checkers, assign values to
them using continuous, blocking and nonblocking assignments, etc. However, some
limitations apply. On the other hand, checkers have a mechanism of nondeter-
ministic modeling which is missing in modules and interfaces. This mechanism is
described in Chap. 23 .
The variables declared in the checker are called checker variables . Declaring nets
in the checker is illegal. Checker variables may be initialized at their declaration, but
assigning them a value in initial procedures is illegal (see Sect. 9.2.2.2 ). Checker
variables may be assigned using continuous assignments or in always procedures.
As mentioned in Sect. 9.2.2.2 the following kinds of always procedures may be used
in checkers (these procedures are discussed in Sects. 2.2.1.1 - 2.2.1.3 ):

￿ always_comb
￿ always_latch
￿ always_ff
Checker always procedures may contain the following statements:

￿ assignments (blocking and nonblocking)
￿ if and case statement
￿ loops
￿ function and task calls
￿ let declarations

Blocking assignments are allowed only in always_comb and always_latch
procedures. Of course, always_ff should contain an event control.
As in programs, all checker variable assignments are executed in the Reactive
region set: continuous and blocking assignments are executed in the Reactive region,
and nonblocking assignments are executed in the Re-NBA region.
Checker variables provide means for carrying auxiliary computations in support
of assertions, called assertion modeling code . Having modeling capability in
checkers is important; it allows separating instrumentation code for assertions from
the RTL code, thus keeping RTL clean and maintainable. This separation is also con-
venient for synthesis tools as it provides an easily identifiable distinction between
RTL and the instrumentation code without the need of conditional compilation.

Example 9.19. Checker stable_for_two_ticks verifies that sig may change
only in clock ticks 2, 4, ...after the reset rst becomes low, as shown in Fig. 9.8 .