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

Janett Mohnke; Paul Molitor; Sharad Malik

doi:10.1007/s100090100039

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

Janett Mohnke, Paul Molitor, Sharad Malik

Research output: Contribution to journal › Article › peer-review

11 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 language	English (US)
Pages (from-to)	207-216
Number of pages	10
Journal	International Journal on Software Tools for Technology Transfer
Volume	3
Issue number	2
DOIs	https://doi.org/10.1007/s100090100039
State	Published - 2001

All Science Journal Classification (ASJC) codes

Software
Information Systems

Keywords

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

Access to Document

10.1007/s100090100039

Cite this

@article{ea321f1ee7ae482fbeaeb869a583b5fd,

title = "Application of BDDs in Boolean matching techniques for formal logic combinational verification",

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.",

keywords = "Formal verification, Permutation independent comparison of Boolean functions, Signature of Boolean variables",

author = "Janett Mohnke and Paul Molitor and Sharad Malik",

year = "2001",

doi = "10.1007/s100090100039",

language = "English (US)",

volume = "3",

pages = "207--216",

journal = "International Journal on Software Tools for Technology Transfer",

issn = "1433-2779",

publisher = "Springer Verlag",

number = "2",

}

TY - JOUR

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

AU - Mohnke, Janett

AU - Molitor, Paul

AU - Malik, Sharad

PY - 2001

Y1 - 2001

N2 - 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.

AB - 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.

KW - Formal verification

KW - Permutation independent comparison of Boolean functions

KW - Signature of Boolean variables

UR - http://www.scopus.com/inward/record.url?scp=84896693141&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84896693141&partnerID=8YFLogxK

U2 - 10.1007/s100090100039

DO - 10.1007/s100090100039

M3 - Article

AN - SCOPUS:84896693141

SN - 1433-2779

VL - 3

SP - 207

EP - 216

JO - International Journal on Software Tools for Technology Transfer

JF - International Journal on Software Tools for Technology Transfer

IS - 2

ER -

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

Abstract

All Science Journal Classification (ASJC) codes

Keywords

Access to Document

Other files and links

Fingerprint

Cite this