Hardware Reference
In-Depth Information
Fig. 21.2
Formal verification
model corresponding to
module
m
i
ic
io
ioc
c
o
oc
Example 21.7.
Consider the module
m
defined by
module
m(
input logic
i, c,
output
o);
wire
a=!i;
always
@(
posedge
c)
o<=a;
endmodule
:m
This module can be represented as an FV model. It seems at first that V should
consist of the four variables i; a; c, and o. But it is easy to see that the value of a is
uniquely determined by the value of i . Therefore, the variable a is redundant. This
situation can be generalized:
Only state variables and primary inputs should be included in the variable set
V of an FV model. The signals that are Boolean functions of other signals
should not be included in the variable set.
For the FV model of
m
, we thus have V
Df
i; c; o
g
and Q consists of the eight states
;
,
f
i
g
;
f
c
g
;
f
o
g
;:::;
f
i; c; o
g
. The transitions of this model are depicted in Fig.
21.2
.
Note that the input signals i and c may have any initial values, and that the
initial value of o is unknown. In simulation, this unknown value is designated as
x
, while in the FV model the unknown value just means that both initial values 0
and 1 for o are possible. All the eight combinations of these variables may occur at
system initialization. It follows that all the states of this model are also initial states,
i.e., I
D
Q.
We now explain the transitions on several examples. Note that the output o can
change only when c changes from 0 to 1. Therefore, if no input changes then neither
does the output change. Consequently, from any state there is a transition to the
same state in Fig.
21.2
, a self-loop. The input i may change independently of c
and o. Therefore, transitions for all values of i are possible. This explains why there
are vertical bidirectional edges in Fig.
21.2
. When c changes from 0 to 1, the next
value of o must be equal to the negation of the current value of i . This yields the
transitions
;!f
o; c
g
,
;!f
i; o; c
g
,
f
i
g!f
c
g
, and
f
i
g!f
i; c
g
.Weleavethe
explanation of the other transitions as an exercise to the reader.
t
Search WWH ::
Custom Search