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

In checker check2 , assertion a2 fails for the same reason as in checker check1 .
The behavior of assertion a1 now depends on the waveform of clk :if clk ticks
for the first time at time 0 then assertion a1 will not fail, as in the checker check1 .
Otherwise, it will also fail since the value of rst is constrained only in global clock
tick 0.

t

Assignment to checker variables, including free variables, is forbidden in
initial procedures to avoid contention. For example, if the code
bit v; // or rand bit v
initial v = 1'b0;
initial v = 1'b1;
were legal, what would the resulting initial value of v be?

Formal Semantics. A free variable initialization

rand some_type v = e;
is equivalent to the following assumption:

initial
assume property (@$global_clock v === e);
Essentially, there is nothing specific for free variables here. The same definition is
applicable to the initialization of any variable.
Using notation from research literature, we will also write the initialization as

init v D e;

and the initial assumption is just the Boolean property v D e.

23.2.2 Free Variable Assignment

A free variable may be written as the left-hand side of a nonblocking assignment
(NBA). It is also possible to assign expressions containing free variables to regular
variables in blocking, nonblocking and continuous assignments. A free variable may
not be written as the left-hand side of a blocking or continuous assignment.

It is illegal to assign to a free variable in a blocking or continuous assignment.