Prof. Dr. Paul Molitor -- Abstracts

Banner
der Martin-Luther-Universitaet Halle-Wittenberg

Title An Efficient Heuristic for State Encoding Minimizing the BDD Representations of the Transition Relations of Finite State Machines.

Authors R. Forth and P. Molitor.

How published In Proceedings of IEEE/ACM Asia and South Pacific Design Automation Conference ASP-DAC 2000, Tokyo, Japan, February 2000.

Abstract
An efficient representation of the (smoothed) transition relation of a synchronous finite state machine (FSM) speeds up the traversal based symbolic verification and the functional simulation of the FSM. When using reduced ordered binary decision diagrams (BDDs), dynamic reordering algorithms are applied in order to keep the sizes of the BDDs tractable. However, when FSMs are represented by BDDs, the state encoding can be used as an additional optimization criteria. In this paper, we present a new algorithm for state encoding of FSMs that minimizes the BDD representations of the corresponding (smoothed) transition relations. Experimental results show the approach to very efficient.

Downloading
PostScript

E-Mail, 30.09.1999

Title		An Efficient Heuristic for State Encoding Minimizing the BDD Representations of the Transition Relations of Finite State Machines.
Authors		R. Forth and P. Molitor.
How published		In Proceedings of IEEE/ACM Asia and South Pacific Design Automation Conference ASP-DAC 2000, Tokyo, Japan, February 2000.
Abstract		An efficient representation of the (smoothed) transition relation of a synchronous finite state machine (FSM) speeds up the traversal based symbolic verification and the functional simulation of the FSM. When using reduced ordered binary decision diagrams (BDDs), dynamic reordering algorithms are applied in order to keep the sizes of the BDDs tractable. However, when FSMs are represented by BDDs, the state encoding can be used as an additional optimization criteria. In this paper, we present a new algorithm for state encoding of FSMs that minimizes the BDD representations of the corresponding (smoothed) transition relations. Experimental results show the approach to very efficient.
Downloading		PostScript