Incremental re-encoding for symbolic traversal of product machines

State space exploration of finite state machines is used to prove properties. The three paradigms for exploring reachable states, forward traversal, backward traversal and a combination of the two, reach their limits on large practical examples. Approximate techniques and combinational verification are far less expensive but these imply sufficient, not strictly necessary conditions. Extending the applicability of the purely combinational check can be achieved through state minimization, partitioning, and re-encoding the FSMs to factor out their differences. This paper focuses on re-encoding presenting an incremental approach to re-encoding for sequential verification. Experimental results demonstrate the effectiveness of this solution on medium-large circuits where other techniques may fail.