Complete-k-distinguishability for retiming and resynthesis equivalence checking without restricting synthesis

ABSTRACT

Iterative retiming and resynthesis is a powerful way to optimize sequential 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) property 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. Experimental results demonstrate that enforcing C-k-D property can speed up the verification process.

REFERENCES

• 1: Pranav Ashar , Aarti Gupta , Sharad Malik, Using complete-1-distinguishability for FSM equivalence checking, ACM Transactions on Design Automation of Electronic Systems (TODAES), v.6 n.4, p.569-590, October 2001 [doi>10.1145/502175.502183]
• 2: Jason Baumgartner , Andreas Kuehlmann , Jacob A. Abraham, Property Checking via Structural Analysis, Proceedings of the 14th International Conference on Computer Aided Verification, p.151-165, July 27-31, 2002
• 3: Berkeley Logic Synthesis and Verification Group. ABC: A System for Sequential Synthesis and Verification, Release, 70930, http://www.eecs.berkeley.edu/alanmi/abc/.
• 4: Robert K. Brayton , Gary D. Hachtel , Alberto L. Sangiovanni-Vincentelli , Fabio Somenzi , Adnan Aziz , Szu-Tsung Cheng , Stephen A. Edwards , Sunil P. Khatri , Yuji Kukimoto , Abelardo Pardo , Shaz Qadeer , Rajeev K. Ranjan , Shaker Sarwary , Thomas R. Shiple , Gitanjali Swamy , Tiziano Villa, VIS: A System for Verification and Synthesis, Proceedings of the 8th International Conference on Computer Aided Verification, p.428-432, August 03, 1996
• 5: Edmund M. Clarke, Jr. , Orna Grumberg , Doron A. Peled, Model checking, MIT Press, Cambridge, MA, 2000
• 6: Gagan Hasteer , Anmol Mathur , Prithviraj Banerjee, Efficient equivalence checking of multi-phase designs using retiming, Proceedings of the 1998 IEEE/ACM international conference on Computer-aided design, p.557-562, November 08-12, 1998, San Jose, California, United States [doi>10.1145/288548.289086]
• 7: Jiang, J.-H. R., and Brayton, R. K. Retiming and resynthesis: A complexity perspective. Computer-Aided Design of Integrated Circuits and Systems, IEEE Transactions on 25, 12 (Dec. 2006), 2674--2686.
• 8: Jie-Hong R. Jiang , Wei-Lun Hung, Inductive equivalence checking under retiming and resynthesis, Proceedings of the 2007 IEEE/ACM international conference on Computer-aided design, November 05-08, 2007, San Jose, California
• 9: Andreas Kuehlmann , Jason Baumgartner, Transformation-Based Verification Using Generalized Retiming, Proceedings of the 13th International Conference on Computer Aided Verification, p.104-117, July 18-22, 2001
• 10: Leiserson, C. E., and Saxe, J. B. Retiming synchronous circuitry. Algorithmica 6, 1 (1991), 5--35.
• 11: Malik, S., Sentovich, E., Brayton, R., and Sangiovanni-Vincentelli, A. Retiming and resynthesis: optimizing sequential networks with combinational techniques. Computer-Aided Design of Integrated Circuits and Systems, IEEE Transactions on 10, 1 (Jan 1991), 74--84.
• 12: Kenneth L. McMillan, Applying SAT Methods in Unbounded Symbolic Model Checking, Proceedings of the 14th International Conference on Computer Aided Verification, p.250-264, July 27-31, 2002
• 13: Mishchenko, A., and Brayton, R. K. Recording synthesis history for sequential verification. In IWLS (2008).
• 14: van Eijk, C. A. J. Sequential equivalence checking based on structural similarities. IEEE Transactions on Computer Aided Design of Integrated Circuits and Systems 19, 7 (2000), 814--819.
• 15: Zhou, H., Singhal, V., and Aziz, A. How powerful is retiming? In IWLS (1998).