Checkers in Formal Verification - SVA: The Power of Assertions in SystemVerilog - page 523

randomized, but not at its initialization. If a free variable is both initialized and
assigned, it is not randomized. 11

Example 23.20. Consider the following code:
checker check(..., clk = $inferred_clock);
rand bit v;
rand bit w = 1'b0;

always_ff @clk
v <= ...;
...
endchecker : check
In checker check , free variable v is randomized at its initialization only, whereas
free variable w may be randomized at every simulation step except for step 0, where
the value of w is 0. t

23.3.3 Checkers with Assumptions

The set of all assumptions contained in a checker instance and in its child checkers
is called the assume set of the checker instance. 12 If the assume set of a checker
instance is nonempty, then the unassigned free variables are randomized in each tick
of any clock event used in any assumption of the assume set. The random values of
the free variables should be chosen in a way to satisfy all the assumptions in the
assume set, if possible—this means that no assumption from the set should fail at
the simulation step when the new randomization values have been assigned if such
values exist. However, lookahead analysis is not required in constraint solving. In
time steps that are not ticks of any clock in the assume set, the unassigned free
variables may be randomized arbitrarily.

Example 23.21. The assume set of checker check1 consists of single assump-
tion m1 . This assumption is clocked by two clocks, clk1 and clk2 .
checker check1( sequence s, ..., event clk1, clk2);
rand bit [3:0] v, w, r;
...
m1: assume property (@clk1 s |-> @clk2 v+w<7);
endchecker : check1

11 If a free variable is of an aggregate data type—array or structure, some of its elements may be
assigned, while others remain unassigned. The LRM defines that all elements of the singular data
types (i.e., of all data types except unpacked ones) should be randomized monolithically, whereas
different elements of the unpacked data types may be randomized independently: some elements
may be randomized, while other may not.
12 There are several subtleties concerning assumption set definition for procedural checker instan-
tiations and for instances involving const cast of checker arguments. These are not covered here.
Refer to the LRM [ 8 ] for the exact definitions.