Formal verification using edge-valued binary decision diagrams

Yung Te Lai, Massoud Pedram, Sarma Vrudhula

Research output: Contribution to journalArticle

23 Citations (Scopus)

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 languageEnglish (US)
Pages (from-to)247-255
Number of pages9
JournalIEEE Transactions on Computers
Volume45
Issue number2
DOIs
StatePublished - 1996

Fingerprint

Binary decision diagrams
Decision Diagrams
Formal Verification
Binary
Binary operation
Directed Acyclic Graph
Data structures
Data Structures
Integer
Formal verification

Keywords

  • Binary decision diagrams
  • Boolean functions
  • Pseudo-Boolean functions
  • Verification

ASJC Scopus subject areas

  • Electrical and Electronic Engineering
  • Hardware and Architecture

Cite this

Formal verification using edge-valued binary decision diagrams. / Lai, Yung Te; Pedram, Massoud; Vrudhula, Sarma.

In: IEEE Transactions on Computers, Vol. 45, No. 2, 1996, p. 247-255.

Research output: Contribution to journalArticle

Lai, Yung Te ; Pedram, Massoud ; Vrudhula, Sarma. / Formal verification using edge-valued binary decision diagrams. In: IEEE Transactions on Computers. 1996 ; Vol. 45, No. 2. pp. 247-255.
@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 Sarma Vrudhula",
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

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 -