Inductive Equivalence Checking under Retiming and Resynthesis
Journal
IEEE/ACM Int'l Conf. on Computer-Aided Design (ICCAD'07)
Pages
326-333
Date Issued
2007-11
Author(s)
Abstract
Retiming and resynthesis are among the most important tech- niques for practical sequential circuit optimization. However, their applicability is much limited due to verification con- cerns. 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 com- plete 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 un- der various retiming and resynthesis scenarios. Experimental results demonstrate the scalability of the approach. Several previously unverifiable circuits and unverifiable transforma- tion scenarios can now be verified effectively.
SDGs
Type
conference paper