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

Nikolaos Liveris*, Hai Zhou, Prithviraj Banerjee

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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 ofcircuits. 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 ofretiming 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.

Original languageEnglish (US)
Title of host publicationProceedings of the ASP-DAC 2009
Subtitle of host publicationAsia and South Pacific Design Automation Conference 2009
Pages636-641
Number of pages6
DOIs
StatePublished - Apr 20 2009
EventAsia and South Pacific Design Automation Conference 2009, ASP-DAC 2009 - Yokohama, Japan
Duration: Jan 19 2009Jan 22 2009

Publication series

NameProceedings of the Asia and South Pacific Design Automation Conference, ASP-DAC

Other

OtherAsia and South Pacific Design Automation Conference 2009, ASP-DAC 2009
CountryJapan
CityYokohama
Period1/19/091/22/09

ASJC Scopus subject areas

  • Computer Science Applications
  • Computer Graphics and Computer-Aided Design
  • Electrical and Electronic Engineering

Fingerprint Dive into the research topics of 'Complete-k-distinguishability for retiming and resynthesis equivalence checking without restricting synthesis'. Together they form a unique fingerprint.

  • Cite this

    Liveris, N., Zhou, H., & Banerjee, P. (2009). Complete-k-distinguishability for retiming and resynthesis equivalence checking without restricting synthesis. In Proceedings of the ASP-DAC 2009: Asia and South Pacific Design Automation Conference 2009 (pp. 636-641). [4796552] (Proceedings of the Asia and South Pacific Design Automation Conference, ASP-DAC). https://doi.org/10.1109/ASPDAC.2009.4796552