Structural FSM traversal

This paper discusses a "structural" technique for traversing the state space of a finite state machine (FSM) and its application to equivalence checking of sequential circuits. The key ingredient to a state-space traversal is a data structure to represent state sets. In structural FSM, traversal-state sets are represented noncanonically and implicitly as gate netlists. First, we present an exact algorithm, which is based on an iterative expansion of the FSM into time frames and a network-decomposition procedure serving the same purpose as an existential quantification operation. Then, we discuss approximative algorithms for the application of structural FSM traversal to sequential equivalence checking. We theoretically analyze the properties of the exact as well as the approximative algorithms. Finally, we give details on the implementation of a sequential equivalence checker and present experimental results that demonstrate the effectiveness of the proposed approach for equivalence checking of optimized and retimed circuits.