The Software Package BALM - The Unknown Component Problem: Theory and Applications - page 136

.model spec
..inputs
..outputs out
..mv out 3 OK notOK done
..table ->out
.OK
.done
..end

Fig. 8.1 BLIF-MV description of the automaton discussed in Example 8.4

a b c

OK
done

OK
done

1 OK 1 1

notOK done notOK

OK, done, notOK

2 3 2

OK, done, notOK

OK, done, notOK

Fig. 8.2 Illustration of Example 8.4 .( a ) Automaton Structure 1; ( b ) Automaton Structure
corresponding to BLIF-MV description in Fig. 8.1 ;( c ) Automaton Structure 2

8.2.4 Describing an Automaton Using BLIF-MV

The BLIF-MV format does not have the notion of accepting states, and therefore
has a limited ability to describe an automaton. By default it describes an FSM and
hence all states are accepting. The only possibility for having a non-accepting state
is adding a state to an incomplete automaton when it is completed. Thus BLIF-MV
can only be used to describe automata where all states are accepting except one.
The reason why this is still useful is that if the specification automaton can be
described in BLIF-MV , then the efficient method of Chap. 7 can be used to solve for
an FSM solution. In many examples, having only one non-accepting state is enough,
as shown in Example 8.4 .

Example 8.4. Suppose that we want to specify in BLIF-MV the automaton with 3
states shown in Fig. 8.2 a.

The states 1 and 3 are accepting states and 2 is a non-accepting state. Consider
the BLIF-MV description shown in Fig. 8.1 .
The table for out does not produce the output value notOK . Consider what
happens when this FSM is converted into an automaton and out becomes the
input. Since it has no latches, it is an FSM with only one state, as shown in