Formal verification using edge-valued binary decision diagrams

Yung Te Lai; Massoud Pedram; Sarma B.K. Vrudhula

doi:10.1109/12.485378

Formal verification using edge-valued binary decision diagrams

Yung Te Lai, Massoud Pedram, Sarma B.K. Vrudhula

Computing, Informatics and Decision Systems Engineering, School of (CIDSE)

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

24 Scopus citations

Abstract

In this paper we present a new data structure called Edge-Valued Binary-Decision Diagrams (EVBDD). An EVBDD is a directed acyclic graph, that provides a canonical and compact representation of functions that involve both Boolean and integer quantities. In general, EVBDDS provide a more versatile and powerful representation than Ordinary Binary Decision Diagrams. We first describe the structure and properties of EVBDDS, and present a general algorithm for performing a variety of binary operations. Next, we describe an important extension of EVBDDS, called Structural EVBDDS, and show how they can be used for hierarchical verification.

Original language	English (US)
Pages (from-to)	247-255
Number of pages	9
Journal	IEEE Transactions on Computers
Volume	45
Issue number	2
DOIs	https://doi.org/10.1109/12.485378
State	Published - 1996

Keywords

Binary decision diagrams
Boolean functions
Pseudo-Boolean functions
Verification

ASJC Scopus subject areas

Software
Theoretical Computer Science
Hardware and Architecture
Computational Theory and Mathematics

Access to Document

10.1109/12.485378

Fingerprint Dive into the research topics of 'Formal verification using edge-valued binary decision diagrams'. Together they form a unique fingerprint.

Cite this

@article{204bd6820c0742c9aa768b0b2ec084a9,

title = "Formal verification using edge-valued binary decision diagrams",

abstract = "In this paper we present a new data structure called Edge-Valued Binary-Decision Diagrams (EVBDD). An EVBDD is a directed acyclic graph, that provides a canonical and compact representation of functions that involve both Boolean and integer quantities. In general, EVBDDS provide a more versatile and powerful representation than Ordinary Binary Decision Diagrams. We first describe the structure and properties of EVBDDS, and present a general algorithm for performing a variety of binary operations. Next, we describe an important extension of EVBDDS, called Structural EVBDDS, and show how they can be used for hierarchical verification.",

keywords = "Binary decision diagrams, Boolean functions, Pseudo-Boolean functions, Verification",

author = "Lai, {Yung Te} and Massoud Pedram and Vrudhula, {Sarma B.K.}",

note = "Funding Information: This work was supported in part by National Science Foundation Research Initiation Awards under contract nos. MIP-9211668 and MIP-9111206. Copyright: Copyright 2011 Elsevier B.V., All rights reserved.",

year = "1996",

doi = "10.1109/12.485378",

language = "English (US)",

volume = "45",

pages = "247--255",

journal = "IEEE Transactions on Computers",

issn = "0018-9340",

publisher = "IEEE Computer Society",

number = "2",

}

TY - JOUR

T1 - Formal verification using edge-valued binary decision diagrams

AU - Lai, Yung Te

AU - Pedram, Massoud

AU - Vrudhula, Sarma B.K.

N1 - Funding Information: This work was supported in part by National Science Foundation Research Initiation Awards under contract nos. MIP-9211668 and MIP-9111206. Copyright: Copyright 2011 Elsevier B.V., All rights reserved.

PY - 1996

Y1 - 1996

N2 - In this paper we present a new data structure called Edge-Valued Binary-Decision Diagrams (EVBDD). An EVBDD is a directed acyclic graph, that provides a canonical and compact representation of functions that involve both Boolean and integer quantities. In general, EVBDDS provide a more versatile and powerful representation than Ordinary Binary Decision Diagrams. We first describe the structure and properties of EVBDDS, and present a general algorithm for performing a variety of binary operations. Next, we describe an important extension of EVBDDS, called Structural EVBDDS, and show how they can be used for hierarchical verification.

AB - In this paper we present a new data structure called Edge-Valued Binary-Decision Diagrams (EVBDD). An EVBDD is a directed acyclic graph, that provides a canonical and compact representation of functions that involve both Boolean and integer quantities. In general, EVBDDS provide a more versatile and powerful representation than Ordinary Binary Decision Diagrams. We first describe the structure and properties of EVBDDS, and present a general algorithm for performing a variety of binary operations. Next, we describe an important extension of EVBDDS, called Structural EVBDDS, and show how they can be used for hierarchical verification.

KW - Binary decision diagrams

KW - Boolean functions

KW - Pseudo-Boolean functions

KW - Verification

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

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

U2 - 10.1109/12.485378

DO - 10.1109/12.485378

M3 - Article

AN - SCOPUS:2342578484

VL - 45

SP - 247

EP - 255

JO - IEEE Transactions on Computers

JF - IEEE Transactions on Computers

SN - 0018-9340

IS - 2

ER -

Formal verification using edge-valued binary decision diagrams

Abstract

Keywords

ASJC Scopus subject areas

Access to Document

Other files and links

Cite this