Structural FSM Traversal - Theory and a Practical Algorithm


This talk proposes a new technique for the traversal of finite state machines (FSMs) called structural FSM traversal. The approach is based on a functional decomposition to perform existential abstraction on the set of reachable states at each clock cycle. We present an exact algorithm for structural FSM traversal and discuss its theoretical properties. To make our approach practical we consider an approximation to the decomposition problem and apply our method to sequential logic equivalence checking. For a practical implementation of the proposed FSM traversal the machine is expanded into an iterative circuit array and well-known combinational synthesis techniques are applied in each time frame. Starting from the initial state, for each time frame we check the equivalence of the outputs and the performed circuit transformations are stored ("recorded") in an instruction queue. In subsequent time frames the instruction queue is re-used ("played") and updated when necessary. At some point the instruction queue does not need to be modified any more and is valid in all subsequent time frames. Thus, a fixed point is reached and machine equivalence is proved by induction. Experimental results show the great promise of this approach to verify circuits after re-synthesis and retiming.

Copies of Slides

The slides in postscript format

Relevant Papers

Structural FSM Traversal - Theory and a Practical Algorithm
©2002-2018 U.C. Regents