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

In addition to most of the traditional explicit graph enumeration algorithms for
automata manipulations, BALM provides computation algorithms based on state-
of-the-art symbolic techniques. This allows most manipulations of automata to
be done implicitly or using a mixture of explicit and implicit techniques. With
these, the system can handle millions of states. For example, complementation
(determinization) of nondeterministic automata, which is an operation based on
hybrid representations, can produce deterministic automata with 100 K states in
several seconds on modern computers.

8.2 Describing FSMs and Automata

BALM supports two file formats, the BLIF-MV (and BLIF ) format for describing
FSMs as multi-level netlists of logic, and the AUT format for describing automata.
The AUT format is a restricted form of BLIF-MV .

8.2.1 The BLIF-MV Format

BLIF-MV was created for VIS [15, 16], a verification package, and is an extension
of BLIF (Berkeley Logic Interchange Format) to efficiently specify sequential
systems in the form of multi-level multi-valued (possibly nondeterministic) logic
networks. Compared to BLIF , BLIF-MV allows (1) multi-valued signals, and (2)
nondeterministic nodes 1 , which can be used to model nondeterministic systems. For
instance, this is useful in the early stages of design development, when a sequential
system may contain non-determinism because some of its components are still to
be specified, and only an abstraction is known. BLIF-MV supports multi-valued
variables, which often simplifies the specification of a system. Each multi-valued
variable is given a size and optionally a list of value names. Currently, the number of
values of the multi-valued variables in the implementation of BALM is limited to 32;
however, the number of values of multi-valued variables denoting states variables in
the AUT format is not limited.
The semantics of BLIF-MV is defined using a combinational/sequential concur-
rency model. There are three basic primitives: variables, tables (nondeterministic
nodes), and latches. A variable can take values from a finite domain. A relation
defined over a set of variables is represented using a table. A table has only one
output and any number of inputs. A particular variable can be designated as the
output of at most one table. Several tables are conceptually inter-connected if they
share the same variable name, i.e. if there is a common name at the output of one

1 Such a node generates, for a given input, a randomly selected output value from a specified subset
of output values.