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

Free variable support in simulation does not provide correctness confidence
even for a given simulation trace, but just shows one arbitrary realization
of the free variables in time. In the presence of temporal assumptions, an
assumption failure in simulation does not necessarily signify incorrectness of
the implementation.

23.3.4 Limitations Imposed on Free Variables

Why are continuous and blocking assignments to free variables illegal? One reason
was explained in Sect. 23.2.2.4 . There is another, more compelling reason related
to the simulation semantics of free variables. Had continuous assignments to free
variables been permitted it would be reasonable to expect the following statements
to behave similarly for a free variable v and an expression e :
assign v=e;
assume property (@global_clock v === e);
From the assumption we know that the sampled values of v and e coincide (at the
ticks of the global clock). This requires a right-hand side of a continuous assignment
in checkers to be also sampled. However, such a definition would not work for a
continuous assignment to regular checker variables. The same problem exists also
for blocking assignments.
An attempt to define the simulation semantics of free variable assignment in a
different manner, and require their right-hand side to be sampled, would not work,
either: Since continuous and blocking assignments in checkers are executed in the
Reactive region, assertions would miss new values of free variables, as shown in the
following example.

Example 23.27. Consider the following code fragment assuming that continuous
assignments to free variables are legal and their right-hand side is sampled:

1 rand bit v;
2 bit a;
3 ...
4 assign v=a;
5 a1: assert property (@$global_clock v == a);

The assignment in Line 4 would execute in the Reactive region, and the value of
a would be sampled. Let regular variable a change from 0 to 1. Then the value of
v would only change in the Reactive region, whereas assertion a1 executes in the
Observed region, and it would see the stale value of v , and therefore, would fail,
which is counterintuitive (cf. Exercise 23.8 ).

t

Unfortunately, there is one more source of inconsistency related to the simulation
semantics of free variables: SystemVerilog allows using free variables in deferred