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

In this example, the clocking event @clk is nondeterministic, and so also is the
value of a because the assignment is performed at nondeterministic time moments.
However, a is deterministic in the sense that it does not introduce any new
nondeterminism: its value is fully defined by the values of e and clk .
The nondeterminism associated with the clocking event is not of an essentially
different kind because the effect of the clocking event could be pushed into the
right-hand side of a checker variable assignment:

always_ff @clk a <= e;
has the same formal semantics as

always_ff @$global_clock a <= $changing_gclk(clk) ?e:a;
had the latter statement been legal in SystemVerilog.

t

A situation similar to assignment of a free variable to a checker variable arises
when a free variable of one checker is passed to a function or to another checker
as an input argument. Formal arguments of a checker can never be declared as free
variables.

Example 23.14. Checker check1 below defines a free variable v and passes it to

checker check2 .
checker check1;
rand bit v;
check2 c2(v, $global_clock);
endchecker : check1

checker check2(a, clk = $inferred_clock);
a1: assert property (@clk not always a iff s_eventually !a);
endchecker : check2
In checker, check2 formal argument a is untyped. We could define it to be of
type bit ,but not of type rand bit since formal checker arguments cannot be free
variables.

t

Though it is illegal to assign free variables by continuous or blocking assign-
ments, they may be referenced on the right-hand sides.

Example 23.15. In FV modeling, it may be useful to define an expression that
may assume only values from a specific set, for example, only values 2 and 5.
A straightforward way to do this is to define a three-bit free variable and add an
assumption constraining its value, such as:

rand bit [2:0] v;
m1: assume property (@$global_clock v == 3'd2 || v == 3'd5);
A better solution is to define a one-bit free variable and to use a continuous
assignment to a regular variable instead:

bit [2:0] v;
rand bit x;
assign v=x?3'd2:3'd5;