Mining unreachable cross-timeframe state-pairs for bounded sequential equivalence checking

Lynn C.L. Chang, Charles H.P. Wen

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

Abstract

One common practice of checking equivalence for two sequential circuits often limits the timeframe expansion to a fixed number, and is known as bounded sequential equivalence checking (BSEC). Although the recent advances of Boolean satisfiability (SAT) solvers make combinational equivalence checking scalable for large designs, solving BSEC problems by SAT remains computationally inefficient. Therefore, this paper proposes a 3-stage method to exploit constraints to facilitate SAT solving for BSEC. The candidate set are first accumulated by checking each composition of functions derived by a data-mining algorithm for every two cross-timeframe flip-flop states. Each candidate can be further removed if it matches simulation data in history and its validity is finally confirmed through gate-level netlist. The verified set is feedbacked as constraints in SAT solving for the original BSEC problem. Experimental results show a 40X speedup in average on ISCAS 89 circuits.

Original languageEnglish
Title of host publication9th International Workshop on Microprocessor Test and Verification
Subtitle of host publicationCommon Challenges and Solutions, MTV 2008
PublisherInstitute of Electrical and Electronics Engineers Inc.
Pages33-38
Number of pages6
ISBN (Print)9780769535814
DOIs
StatePublished - 1 Jan 2008
Event2009 9th International Workshop on Microprocessor Test and Verification: Common Challenges and Solutions, MTV 2008 - Austin, TX, United States
Duration: 8 Dec 200810 Dec 2008

Publication series

NameProceedings - International Workshop on Microprocessor Test and Verification
ISSN (Print)1550-4093

Conference

Conference2009 9th International Workshop on Microprocessor Test and Verification: Common Challenges and Solutions, MTV 2008
CountryUnited States
CityAustin, TX
Period8/12/0810/12/08

Fingerprint Dive into the research topics of 'Mining unreachable cross-timeframe state-pairs for bounded sequential equivalence checking'. Together they form a unique fingerprint.

  • Cite this

    Chang, L. C. L., & Wen, C. H. P. (2008). Mining unreachable cross-timeframe state-pairs for bounded sequential equivalence checking. In 9th International Workshop on Microprocessor Test and Verification: Common Challenges and Solutions, MTV 2008 (pp. 33-38). [5070931] (Proceedings - International Workshop on Microprocessor Test and Verification). Institute of Electrical and Electronics Engineers Inc.. https://doi.org/10.1109/MTV.2008.23