Incremental FSM Re-encoding for Simplifying Verification by Symbolic Traversal

State space exploration of finite state machines is used to prove properties about sequential behavior, such as the equivalence of two machines. 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 to pairs of machines with different encodings can be achieved through state minimization, partitioning, and re-encoding the FSMs to factor out their differences. This paper focuses on re-encoding: we present an incremental approach to re-encoding for sequential verification. We transform the product machine traversal to a combinational verification in the best case, and to a computationally simpler product machine traversal in the general case. Experimental results demonstrating the effectiveness of these techniques o medium-large circuits where other techniques may fail