Hardware Reference
In-Depth Information
always_latch
if
(c)q=i;
Both representations are equivalent from the perspective of formal semantics, and
we will consider the latter representation. The assignment to
q
is
incomplete
in the
sense that it is executed only when condition
c
is true. The rewriting produces a
continuous assignment with a combinational self-loop: the assignment right-hand
side depends on its target:
assign
q=c?i:q;
To reflect the dependency of the new value of
q
on its previous value, this assignment
should be modeled in terms of its next state variables, and therefore it is represented
with the following next state function:
q
0
c
0
?
i
0
:
q
Representation of the initialization of
q
is straightforward:
init q
0
t
23.2.2.5
Checker Data Model
We give here a summary of the FV model build from the modeling code of a
synthesizable checker. We assume that all variables are split into individual bits.
Each variable
v
introduces one and only one of the following options:
v
has neither assignment nor initialization.
Initialization init
v
e
1
, corresponding to Boolean assumption
v
D
e
1
.Heree
1
is an expression containing current state variables only.
Next state function
v
0
e
2
, corresponding to assumption G.
v
0
D
e
2
/.Heree
2
is
an expression that may contain both current and next state variables.
Both initialization and next state function.
Current state function
v
e
1
, corresponding to invariant assumption G.
v
D
e
1
/.
Here e
1
is an expression containing current state variables only.
The current state function is actually redundant, as it is equivalent to the combination
of an initialization and a next state function:
init
v
e
1
I
v
0
e
1
Essentially the same transition relation is created to build an FV model for
general SystemVerilog modules and interfaces, provided they conform to restric-
tions for “FV synthesizability”. The details of such a build are much more
complicated, involving multiple assignments to nets, general purpose
always
procedures,
initial
procedures, etc. Support for an FV model build has been
tacitly assumed in Sect.
21.2
.
Search WWH ::
Custom Search