Hardware Reference
In-Depth Information
Example 23.11.
Consider the following code:
checker
check1(a, b,
event
clk = $inferred_clock);
rand var type
(b)v=a;
always_ff
@clk v <= b;
endchecker
: check1
In checker
check1
free variable
v
is fully assigned, and it may be replaced with a
regular checker variable, as in the checker
check2
:
checker
check2(a, b,
event
clk = $inferred_clock);
var type
(b)v=a;
always_ff
@clk v <= b;
endchecker
: check2
t
Thus, regular checker variables may be considered a special case of free
variables, and the formal semantics of their NBA is a special case of the formal
semantics of free variable NBA provided that the same limitations are imposed (e.g.,
they are not assigned in tasks, etc.)
23.2.2.4
Assigning Free Variables to Checker Variables
It is legal to assign an expression containing free variables to a regular checker vari-
able; it is also possible to initialize a regular variable with an expression containing
free variables. This means that the regular variables may also be nondeterministic.
However, the regular variables do not introduce any new nondeterminism to the
system; their values are completely defined by the values of the variables on which
they depend.
Example 23.12.
Consider the following checker fragment:
bit
[3:0] a;
rand bit
[3:0] v;
always_ff
@clk a <= v;
If the value of
v
is nondeterministic, then starting from clock tick 1 the value of
a
is
also nondeterministic. The initial value of
a
is
0
by default—only a free variable can
introduce nondeterminism through its initial value, and then only if it has not been
explicitly initialized. Nevertheless,
a
is deterministic in the following sense: its value
is uniquely defined by the value of
v
;
a
does not introduce any new nondeterminism.
t
Example 23.13.
Nondeterminism can also be introduced by an event control, as
illustrated by the following checker fragment:
rand bit
clk;
bit
[3:0] a;
always_ff
@clk
a <= e; // e - deterministic expression defined elsewhere
Search WWH ::
Custom Search