Formal verification using edge-valued binary decision diagrams

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

Research output: Contribution to journalArticle

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

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

  • Cite this