Hardware Reference
In-Depth Information
Fig. 12.1
FSM composition
I
M
A
O
M
C
U
V
M
B
Z
given component
M
A
j
, while preserving the original composition, i.e., any valid
M
A
j
replacement
M
A
1
M
A
j
M
A
n
are equivalent. Due to the fact that the synchronous composition
operator is commutative and associative,
1
it holds that
of
M
A
j
is such that
M
A
1
M
A
j
M
A
n
and
M
A
1
M
A
j
M
A
n
and
M
A
j
.M
A
1
M
A
j 1
M
A
j C1
M
A
n
/
are equivalent. Therefore the
previous equation can be rewritten as:
M
X
M
A
1
::: M
A
j 1
M
A
j C1
M
A
n
Š M
A
1
M
A
j 1
M
A
j
M
A
j C1
M
A
n
:
The associative property of the composition operator simplifies the operation to
build the FSM composition
M
A
1
M
A
n
, because the composition of several
FSMs can be derived by iterating the composition of two machines. To resynthesize
a component FSM
M
A
i
based on equation solving, we lump together all the
remaining FSMs to obtain the context FSM
M
A
1
M
A
j 1
M
A
j C1
M
A
n
Š
M
Context
, and then we further compose
M
A
i
with
M
Context
to obtain the specification
FSM
M
A
i
M
Context
Š M
spec
; at the end we set up the equation
M
X
M
Context
Š
M
A
j
M
Context
or
M
Context
M
X
Š M
spec
).
We remind from Chap. 3 that the largest solution of the equation
M
X
M
Context
Š M
spec
(or symmetrically
M
Context
M
X
Š M
spec
is expressed by an observable FSM. Any solution of the equation is a
reduction of the largest solution, i.e., the behavior of each FSM that is a solution
of the equation is contained in the largest solution. The converse is not always
true: not each reduction of the largest solution is a solution of the equation. The
complete characterization of such valid reductions still remains unknown. However,
for an equation over complete deterministic FSMs there are known cases where
1
Given FSMs
M
A
;M
B
;M
C
M
A
M
B
Š M
B
M
A
.M
A
M
B
/ M
C
Š
it holds that
and that
M
A
.M
B
M
C
/
.
Search WWH ::
Custom Search