Improving structural FSM traversal by constraint-satisfying logic simulation

We increase the reasoning power of the Record & Play algorithm for structural FSM traversal (Stoffel and Kunz, 1997), by incorporating a constraint-satisfying simulation technique. Combinational verification tools often use simulation to identify candidates for internally equivalent functions. This can significantly reduce the computational costs of proving the equivalence of two circuits. The key idea to improve Record & Play is to perform a random simulation in every time frame that satisfies stored equivalences and constants which are needed to represent the state set. Our experimental results show the benefit of the proposed approach