Complete-k-distinguishability for retiming and resynthesis equivalence checking without restricting synthesis
Nikolaos I. Liveris, Hai Ming Zhou, Prithviraj Banerjee · 2009
Iterative retiming and resynthesis is a powerful way to optimize se-quential circuits but its massive adoption has been hampered by the hardness of verification. This paper tackles the problem of retiming and resynthesis equivalence checking on a pair of circuits. For this purpose we define the Complete-k-Distinguishability (C-k-D) prop-erty for any natural number k based on C-1-D. We show how the equivalence checking problem can be simplified if the circuits satisfy this property and prove that the method is complete for any number of retiming and resynthesis steps. We also provide a way to enforce C-k-D on the circuits without restricting the optimization power of retiming and resynthesis or increasing their complexity. Experimen-tal results demonstrate that enforcing C-k-D property can speed up the verification process. 1