Hardware Reference
In-Depth Information
13.2
Computing Simulation Relations with Language
Equations
We assume to operate with FSMs represented as sequential circuits, so we can talk
of sequential elements as latches (as in Chap. 7). Consider the general topology
of Fig. 13.1 a. The configuration indicates that variables u and v are internal to
.
This is typical of the situation where we want to derive the maximum flexibility
of a submachine FSM from a given one. The given FSM will be the specification
S
S
. The signals u and v can be any signals present in the fixed part
F
, not just
latch outputs of
(as is done in the case of the latch splitting operation of
BALM). We might want to compute the maximum flexibility (or CSF) of the
X
F
part. This is, the maximum FSM solution to the language solving problem,
F.i;o;
.
On the other hand, we will show that we can set up a simulation relation with a
similar configuration shown in Fig. 13.1 b. The only difference is that we have made
u also a pseudo-output of
u
;
v
/ X.i;;
u
;
v
/ S.i;o;; /
. It is a pseudo output since it does not connect to any-
thing in the environment; moreover, we will require that it is preserved. The problem
stated in terms of language solving is
S
F.i;o;
u
;
v
/ X.i;;
u
;
v
/ S.i;o;
u
; /
.
/ sim
We will show that this corresponds to solving
F.i;o;
u
;
v
/ X.i;;
u
;
v
,where sim corresponds to a particular simulation relation between
the states on the left and right sides.
We restate for automata the definition of a simulation relation previously given
for FSMs, since we deal with automata in this section.
S.i;o;; /
a
b
S
S
i
o
i
o
F
F
v
u
v
u
X
X
Fig. 13.1
from a given FSM,
where u is any set of signals in F and v are some inputs to F ;( b ) Configuration for computing a
sub-flexibility for a submachine X from a given FSM, where u is any set of signals in F and v are
some inputs to F ( u is also a pseudo-output of S )
( a ) Regular configuration for computing the CSF for a submachine
X
Search WWH ::




Custom Search