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

This chapter is mainly intended for people interested in FV. However, it is also
useful for people interested in creating testbenches that can be processed by FV
tools.

23.1 Free Variables

Free variables in checkers have the same syntax as regular checker variables, but
they are prefixed with the keyword rand . If a free variable is unrestricted, it may
assume any value at any time. Essentially free variables are similar to primary inputs
to the model.
Free variables may only be declared in a checker body. They cannot be used as
checker formal arguments (ports).

23.1.1 Free Variables in Assertions

We will study first the behavior of free variables in an assertion context, introducing
the main ideas with examples. The following statement characterizes the semantics
of free variables in the absence of assumptions:

The behavior of a free variable in an assertion context corresponds to universal
quantification over its domain in each clock tick.

Example 23.1. Consider the following checker:

checker failure;
default clocking @$global_clock; endclocking
rand bit v;
a1: assert property (v);
endchecker : failure
Since v may assume any value in any clock tick, it may assume value 0 (i.e., false)
in clock tick 0, and therefore assertion a1 fails.
Here is a more formal explanation. The formal semantics of the assertion
always a , where a is a regular variable, is 8 i w i

ˆ a, which means that a holds
in each clock tick on the trace w . If we want to stress that the value of a depends
on the clock tick i, we can rewrite this formula as 8 i w i ˆ a i . In this formula,

we assume that a is well defined, i.e., the values of a are given in each clock tick.
In our case, when v is a free variable, it may assume any value in any clock tick,
and therefore the formal semantics of the assertion a1 is 8 i 8 v i w i ˆ v i , which is