Inductive equivalence checking under retiming and resynthesis

Retiming and resynthesis are among the most important techniques for practical sequential circuit optimization. However, their applicability is much limited due to verification concerns. Overcoming the verification bottleneck is a supreme task. This paper studies both the theoretical and practical aspects of inductive verification on the equivalence between circuits under retiming and resynthesis transformation. We study the completeness condition of the inductive approach to equivalence checking and show that prior work is only complete for circuits transformed under retiming or resynthesis. but not both. We overcome prior limitation and make complete the equivalence checking for circuits transformed up to retiming+resynthesis-!-retiming. The theoretical insights lead to a robust satisfiability formulation of verification under various retiming and resynthesis scenarios. Experimental results demonstrate the scalability of the approach. Several previously unverifiable circuits and unverifiable transformation scenarios can now be verified effectively.