Hardware Reference
In-Depth Information
23.3
Free Variables in Simulation
So far we have discussed the formal semantics of free variables. In this section, we
discuss the behavior of free variables in simulation.
As their syntax suggests, free variables are randomized in simulation. All
uninitialized free variables are randomized initially. Otherwise, only unassigned free
variables are randomized. The following rules are applicable to all randomized free
variables:
A randomized free variable may change its value at most once during each
simulation tick.
If a randomized free variable gets a new random value in some simulation tick,
this value becomes ready before the Observed region.
A sampled value of a free variables is its current value.
The sampled value of a free variable coincides with its current value.
23.3.1
Unconstrained Free Variables
If there are no assumptions in a checker or any of its child checkers, and a checker
variable is neither assigned nor initialized then it can get a new value at any time
step.
Example 23.19.
In the original code of Example
23.18
, there are no assumptions,
and so the simulator may assign free variable
start
a new random value at any
simulation step. One extreme case would be assigning it a random value only once,
at its initialization, and then leaving it unchanged. The other extreme case would be
assigning it a new random value at each simulation step. Both behaviors are legal.
However, the first behavior is too “boring”, while the second one is an overkill:
there is no advantage in changing the value of
start
every simulation tick since all
the assignments and the assertions where it is used are controlled by
clk
. Therefore,
most simulators will assign
start
a new random value at every tick of
clk
.
t
23.3.2
Assigned Free Variables
If a free variable is assigned a value, then it is only randomized at its initialization,
provided it is not initialized. If a free variable is unassigned, but initialized, it is
Search WWH ::
Custom Search