Hardware Reference
In-Depth Information
Procedure 3.1.5. Input: Complete FSM M ; Output: Largest submachine of M that
is a Moore FSM, denoted by Moore .M / ,ifitexists.
9 s 0 2 Ms:t:.i;s;s 0 ;o/ 2
Given a state s 2 M , define the set K s Df o 2 O
j8 i 2 I
T M g , K s
O.
1. Iterate for each state s 2 M until M does not change.
(a) Compute the set K s
O.
ยค; delete from T M each transition .i;s;s 0 ;o/such that o 62 K s ;
(b) If K s
if K s
D; delete s with all its incoming edges from M .
2. If the initial state has been deleted then there is no submachine of M that is a
Moore FSM, otherwise Moore .M / D M .
Theorem 3.9. Any Moore FSM M 0 that is a reduction of M is a reduction of
Moore .M / , the output of Procedure 3.1.5 .
Proof. Define a state s of FSM M as 1-nonMoore if K s D; . State s is k-nonMoore,
k>1,ifforsomei 2 I and for all o 2 O each state reached from s under the
transition labeled .i=o/ is j -nonMoore, j<k. State s is nonMoore if it is k-
nonMoore for some k 1. Moore .M / is obtained from M by removing iteratively
the nonMoore states and, from the remaining states s, the transitions .i;s;s 0 ;o/such
that o 62 K s . Notice that by construction Moore .M / is guaranteed to be complete.
We must prove that if L.M 0 / L.M / and L.M 0 / is Moore then L.M 0 /
L. Moore .M //. The proof goes by induction. If L.M 0 / is Moore, there is no string
in L.M 0 / that takes the FSM M from the initial state to a 1-nonMoore state.
Suppose now by induction hypothesis that no string in L.M 0 / takes M to a k-
nonMoore state, k>1. We must conclude that, if L.M 0 / is Moore, there is also
no string that takes M to a .k C 1/-nonMoore state, otherwise, by definition of
.k C 1/-nonMoore, L.M 0 / has a string that takes M to some j -nonMoore state,
j k. Therefore no string in L.M 0 / takes the FSM M to a nonMoore state, i.e.,
L.M 0 / L. Moore .M //.
t
Moore machines play a role in guaranteeing that the composition of FSMs is a
complete FSM (see Theorem 3.12 ).
3.2
Composition of Finite State Machines
Different types of composition between pairs of FSMs may be defined, according
to the protocol by which signals are exchanged. For a given composition operator
and pair of FSMs we must establish whether the composition of this pair is defined,
meaning that it yields a set of behaviors that can be described by another FSM.
In general, the composition of FSMs is a partially specified function from pairs
of FSMs to an FSM. In our approach we define the composition of FSMs by
means of the composition operators over languages introduced in Sect. 2.1. Thus
Search WWH ::




Custom Search