Computation of Flexibility in Sequential Networks - The Unknown Component Problem: Theory and Applications - page 169

extract_aut MB.aut
support v6,v5,v4,v3,v2,v1,v0,v9,v8,v7,v12,v11,v10 MB.aut
MBs.aut
product MBs.aut MAd_min.aut MBi.aut
prefix MBi.aut MBifsm.aut
This produces the automaton shown in Fig. 10.8 that represents the incompletely
specified FSM obtained by Wang-Brayton's procedure. The input labels have been
left off the STG because it would be unreadable.
To compare this with the language solving approach, we execute the latch split
script produced by the BALM latch split command:
\# Language solving script (partitioned) generated by MVSIS
\# for latch splitting of sequential network s386.blif
\# on Wed Jun 06 09:02:05 2007
\# Command line was: latch_split 0-2.
\# We use the previous results generated by latch-splitting
\# s386.blif, which created the environment automaton
\# s386f.blif
echo Solving the language equation ...
solve_fsm_equ s386f.blif s386.blif v6,v5,v4,v3,v2,v1,v0,v9,
v8,v7 v12,v11,v10 s386xs.aut
print_stats_aut s386xs.aut
Executing print stats aut gives the following output
Solving the language equation ...
Progressive = 0.00 sec
"csf":incomplete(14 st), deterministic, non-progressive(14 st),
and non-Moore(14 st).
13 inputs(13 FSM inputs) 15 states(15 accepting) 59 trans
Inputs = { v6,v5,v4,v3,v2,v1,v0,v9,v8,v7,v12,v11,v10 }
We now check if the language of the automaton MBifsm.aut , produced
by the W&B-K&N procedure, is contained in the most general FSM solution,
s386xs.aut :
balm > contain s386xs.aut MBifsm.aut
Warning: Automaton 1 is completed before checking.
Warning: Automaton 2 is completed before checking.
The behavior of automaton 1 contains the behavior of
automaton 2.
and fortunately it is.
The next steps would be to use the incompleteness of MBifsm.aut to state
minimize it as an incompletely specified FSM. The program STAMINA could
be used. In contrast, the NDFSM s386xs.aut , produced by language solving,
needs to be minimized but there are no good general procedures for this at the
moment. The operator dcmin can be used and in this case it does produce an
NDFSM automaton with 6 states (from 15 states), but the original machine for
this part, s386a.blif , has only 5 reachable states. We did not try STAMINA
on MBifsm.aut to see what kind of minimization can be done.