Integrating a Boolean satisfiability checker and BDDs for combinational equivalence checking

Aarti Gupta, Pranav Ashar

Research output: Contribution to conferencePaper

19 Scopus citations

Abstract

There has been much interest in techniques which combine the advantages of function-based methods, such as BDDs, with structure-based methods such as ATPG, for verifying the equivalence of combinational circuits. However, most existing efforts have focused on exploiting circuit similarity through use of learning and/or ATPG-based methods rather than on making the integration between BDDs and ATPG techniques efficient. This paper presents a new technique, where the focus is on improving the equivalence check itself, thereby making it more robust in the absence of circuit similarity. It is based on tight integration of a Boolean Satisfiability Checker with BDDs, whereby BDDs are effectively used to reduce both the problem size and the number of backtracks for the satisfiability problem. This methodology does not preclude exploitation of circuit similarity, when it exists, since the improved check can be easily incorporated as the inner loop of the well-known iterative framework involving search and replacement of internally equivalent nodes. We demonstrate the significance of our contributions with practical results on the ISCAS benchmark circuits.

Original languageEnglish (US)
Pages222-225
Number of pages4
StatePublished - Jan 1 1998
Externally publishedYes
EventProceedings of the 1998 11th International Conference on VLSI Design - Chennai, India
Duration: Jan 4 1998Jan 7 1998

Other

OtherProceedings of the 1998 11th International Conference on VLSI Design
CityChennai, India
Period1/4/981/7/98

All Science Journal Classification (ASJC) codes

  • Hardware and Architecture
  • Electrical and Electronic Engineering

Fingerprint Dive into the research topics of 'Integrating a Boolean satisfiability checker and BDDs for combinational equivalence checking'. Together they form a unique fingerprint.

  • Cite this

    Gupta, A., & Ashar, P. (1998). Integrating a Boolean satisfiability checker and BDDs for combinational equivalence checking. 222-225. Paper presented at Proceedings of the 1998 11th International Conference on VLSI Design, Chennai, India, .