An exact input encoding algorithm for BDDs representing FSMs

Author

Sangiovanni-Vincentelli, Alberto L.

Author_Institution

Dept. of Electr. Eng. & Comput. Sci., California Univ., Berkeley, CA

fYear

1998

fDate

19-21 Feb 1998

Firstpage

294

Lastpage

300

Abstract

We address the problem of encoding the state variables of a finite state machine such that the BDD representing its characteristic function has the minimum number of nodes. We present an exact formulation of the problem. Our formulation characterizes the two BDD reduction rules by deriving conditions under which these reduction rules can be applied. We then provide an algorithm that finds these conditions and solves the problem by formulating it as a 2-CNF formula and extracting all its prime implicants. In addition to this, we implemented a simulated annealing algorithm for this problem and provide a thorough experiment of the impact of encoding on a BDD representing an FSM with different orderings

Keywords

Boolean functions; finite state machines; logic CAD; simulated annealing; 2-CNF formula; BDDs; FSMs; characteristic function; exact input encoding algorithm; prime implicants; reduction rules; simulated annealing algorithm; state variables; Automata; Binary decision diagrams; Boolean functions; Circuit synthesis; Counting circuits; Data mining; Data structures; Encoding; Heuristic algorithms; Logic; Simulated annealing;

fLanguage

English

Publisher

ieee

Conference_Titel

VLSI, 1998. Proceedings of the 8th Great Lakes Symposium on

Conference_Location

Lafayette, LA

ISSN

1066-1395

Print_ISBN

0-8186-8409-7

Type

conf

DOI

10.1109/GLSV.1998.665275

Filename

665275