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.



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.




E-Mail, 30.09.1999