A state space decomposition algorithm for approximate FSM traversal

Approximate FSM traversal is very useful in many applications of interest, when the size of the problem to be solved is too large to be handled by exact methods. The quality of the approximation strongly depends on how state variables are partitioned to decompose the state space, and exploiting circuit structure appears to be the most promising technique to determine a good state variable partition. In this paper we formulate the state space decomposition problem as a graph problem to be solved on the latch connection graph the FSM under investigation. Structural analysis on that graph is used to determine an initial partition; breaking and aggregation, based on seed generation, clustering, and iterative refinement of the current result, are then performed on the initial solution. Approximate FSM traversal results obtained on the largest ISCAS89 examples show the effectiveness of the proposed algorithm