Application of BDDs in Boolean matching techniques for formal logic combinational verification

Janett Mohnke, Paul Molitor, Sharad Malik

Research output: Contribution to journalArticle

9 Scopus citations

Abstract

Verifying that an implementation of a combinational circuit meets its golden specification is an important step in the design process. As inputs and outputs can be swapped by synthesis tools or by interaction of the designer, the correspondence between the inputs and the outputs of the synthesized circuit and the inputs and the outputs of the golden specification has to be restored before checking equivalence. In this paper, we review the main approaches to this isomorphism problem and show how to apply OBDDs in order to obtain efficient methods.

Original languageEnglish (US)
Pages (from-to)207-216
Number of pages10
JournalInternational Journal on Software Tools for Technology Transfer
Volume3
Issue number2
DOIs
StatePublished - Dec 1 2001

All Science Journal Classification (ASJC) codes

  • Software
  • Information Systems

Keywords

  • Formal verification
  • Permutation independent comparison of Boolean functions
  • Signature of Boolean variables

Fingerprint Dive into the research topics of 'Application of BDDs in Boolean matching techniques for formal logic combinational verification'. Together they form a unique fingerprint.

  • Cite this