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

assertions. Their simulation semantics looks innocent, and Example 23.26 shows a
reasonable usage. Consider now a different example:

rand bit v;
bit a;
...
m1: assume final (v == a);
a1: assert property (@$global_clock v == a);
Suppose that a transitions from 0 to 1. According to Sect 23.3.3 , v receives the value
1 before the Observed region. Concurrent assertion a1 is executed in the Observed
region. The sampled value of v is 1 (its current value), and the sampled value of a is
0 (its preponed value), so that the assertion fails. Therefore, using free variables in
deferred (or final) assertion statements is a bad idea.

Never use free variables in deferred (or final) assertion statements.

23.4 Rigid Variables

23.4.1 Rigid Variables in Formal Verification

Free variables defined in Sect. 23.1 can assume any value at any simulation
step (unless constrained by assumptions). Rigid variables may assume any value
initially, but their value does not change in time. In other words, rigid variables are
constant free variables, which fact is reflected in their syntax. For example,

rand const bit [3:0] r;
is a declaration of rigid variable r . This variable may assume any 4-bit value, but
this value remains unchanged all the time. Note that the rand qualifier must appear
first; const rand is illegal.
It is straightforward to model rigid variables with free variables. For example,
the above declaration of rigid variable r is equivalent to:
rand bit [3:0] r;
assume property (@$global_clock $steady_gclk(r));
This is, essentially, the formal semantics of free variables: rigid variable r is a free
variable with additional assumption G.r D r 0 / imposed (we use research literature
notation here).
Rigid variable initialization is legal, but it renders the rigid variable equivalent to
a non-free constant variable:

rand const bit [3:0] r = 4'd5;