A structural approach to state space decomposition for approximate reachability analysis

Exploiting circuit structure is a key issue in the implementation of algorithms for state space decomposition when the target is approximate FSM traversal. Given the gate-level description of a sequential circuit, the information about its structure can be captured by evaluating the affinity between pairs or groups of latches. Two main factors have to be considered in carrying out the structural analysis of a sequential circuit: latch connectivity and latch correlation. We estimate the affinity of two latches by combining these two factors, and we use this measure to translate the state space decomposition problem into a graph partitioning problem. Traversal results obtained on the largest ISCAS´89 benchmarks show the effectiveness of the method