Hardware Reference
In-Depth Information
23.2.2.1
Unconditional Assignment to Free Variables
We consider first the case when the free variable assignment does not belong to
the scope of any conditional or looping statement. Let us start with the following
example.
Example 23.8.
The following checker fragment defines a periodic clock,
myclk
:
rand bit
myclk;
always_ff
@$global_clock
myclk <= !myclk;
In this example,
myclk
is assigned, but uninitialized.
myclk
changes its value with
each tick of the global clock. Nevertheless,
myclk
is nondeterministic. Since
myclk
is uninitialized, it has two possible patterns:
0101
::: and
1010
:::.
t
Formal Semantics (Global Clock).
The formal semantics of a free variable NBA
controlled by the global clock
rand
some_type v;
always_ff
@$global_clock v <= e;
is defined as:
assume property
(@$global_clock $future_gclk(v) === e);
For readability, we extend the formal notation from Chap.
21
. Free variable assign-
ment will be designated as
v
0
e, meaning that the next state variable
v
0
is
assigned the value e. This is just a shortcut notation for the invariant defined by
the assumption G.
v
0
D
e/. This invariant defines a transition relation that happens
to be a function: the value of next state variable
v
0
is uniquely determined from
the values of the current state variables forming the expression e. Such a transition
relation is called a
next state function
. Because of their explicit unidirectionality, free
variable assignments may be handled more efficiently by FV tools than an equivalent
set of assumptions.
3
Example 23.9.
The assignment form Example
23.8
can be rewritten as
assume property
(@$global_clock $changing_gclk(myclk));
but this version might be less efficient since the explicit unidirectionality of the
assignment of the free variable
myclk
has been lost.
t
Formal Semantics (Arbitrary Clock).
The semantics of free variable assignment
v
0
@(
edge
clk
)
e, which is controlled by clocking event
@(
edge
clk
)
, is defined
as
v
0
.clk
ยค
clk
0
/
?
e
:
v
. This means that
v
gets the value e only when
the clock ticks, and it retains its old value when the clock does not tick. In this
3
Note that NBAs in a checker may conflict with assumptions, but not with other assignments. In
a checker, NBAs are allowed only within
always_ff
procedures (Sect.
9.2.2.2
), and thus their
targets cannot be overridden by other processes (Sect.
2.2.1.3
).
Search WWH ::
Custom Search