An efficient heuristic for state encoding minimizing the BDD representations of the transistion relations of finite state machines
Riccardo Forth, Paul Molitor · 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 be very efficient.