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

Chapter 8
The Software Package BALM

8.1 Introduction

Finite automata and their languages are well-studied topics since the early
development of computation theory. Traditional implementations of automata
manipulations are based on explicit state representation, and are limited to automata
with a few thousand states. The manipulation of automata became more practical
with the advent of efficient symbolic techniques based on binary decision diagrams
(BDDs), satisfiability (SAT) solvers and AND-INVERTER graphs (AIGs).
Based on these techniques, the BALM (Berkeley Automata and Language
Manipulation) package provides an experimental environment for more efficient
manipulation of finite automata in various application domains, e.g., synthesis,
verification, control, etc. The BALM package includes the most typical automata
operations, such as determinization and state minimization, as well as a few
visualization capabilities, which rely on the powerful graph visualization software
Graphviz [49]. The applicability of BALM to finite-state machine synthesis is
illustrated by its use in solving several problems that are formulated as unknown
component problems using language equations. BALM is designed like SIS and
MVSIS to have a command line on which a command can be entered. A sequence
of commands can be read from a file, called a script. In the appendix, we list and
briefly explain the presently implemented commands of BALM.
Compared with other automata manipulation utilities, such as Grail [117],
FSA [43], FIRE [41] and many others (see also [144]), BALM provides an
environment particularly suited for language equation solving. It can be used in
component-based sequential hardware synthesis. It is useful as an educational tool,
which can further the understanding of finite automata. In addition, it may be useful
in sequential system optimization, because it can interface with other programs
based on the logic file formats, such as BLIF-MV or BLIF , which are commonly
used to represent designs in academic logic synthesis tools. With BALM, it is
possible to extract sequential flexibilities in implementing a hardware finite state
machine. We will illustrate some of these applications.