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 | |
| State | Published - 1996 |
Fingerprint
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 journal › Article
}
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 -