Hardware Reference
In-Depth Information
Fig. 18.1
Topology for
the synthesis of
!
-automata
i
o
F
S
v
u
X
This has multi-valued input signal
o
whose values are taken from the alphabet
S
D
.Q
S
;˙
o
;q
0
;
S
;A/
˙
o
. Thus
,where
A
is the stable set. The fixed part
F
(or context) is assumed to be an FSM with multi-valued inputs
i
and
v
and
multi-valued outputs
(although an FSM) is interpreted as a special
deterministic Buchi automaton, represented by
o
and
u
.
F
D
.Q
F
;˙
i;
u
;
v
;o
;q
0
;
F
;B/
F
,
where the accepting set
is required to be a deterministic
FSM, because we want to implement it as a sequential network.
The objective is to find an FSM implementation of
B
is the set of
all
states.
X
X
such that its synchronous
composition with
F
satisfies the co-Buchi specification
S
. Solutions are obtained
by solving a corresponding
!
-language containment problem: find
X
such that
F
X
S
, i.e., the
!
-language represented by the
!
-automaton
F
X
is contained
in the
!
-language represented by the
!
-automaton
S
.
The most general solution
(not necessarily an FSM) of
F
X
S
is
X
D
F
S
as derived in Chap. 2 and
interpreted as an
-automaton. Particular FSM solutions are derived by eliminating
from the graph of the most general solution loops that contain non-accepting states
while being input-progressive, as discussed in detail in Sect.
18.4.2
.
!
18.4
The Synthesis Flow
The general synthesis flow has the following steps, that pattern those already seen
for finite automata, except that the latter are replaced
-automata. All operations
are done on Buchi or co-Buchi automata and are
explai
ned below in more detail.
The steps of the procedure to compute
!
X
D
F
S
and the FSM sub-solutions
are:
1. ComplementOmega(
S
); (complement the co-Buchi automaton
S
by dualizing
the acceptance condition).
2. Complete(
F
); (complete the FSM
F
as a Buchi automaton).
Search WWH ::
Custom Search