The Community for Technology Leaders
Green Image
ABSTRACT
<p><b>Abstract</b>-In this paper we present a new data structure called Edge-Valued Binary-Decision Diagrams (<scp>EVBDD</scp>). An <scp>EVBDD</scp> is a directed acyclic graph, that provides a canonical and compact representation of functions that involve both Boolean and integer quantities. In general, <scp>EVBDD</scp>s provide a more versatile and powerful representation than Ordinary Binary Decision Diagrams. We first describe the structure and properties of <scp>EVBDD</scp>s, and present a general algorithm for performing a variety of binary operations. Next, we describe an important extension of <scp>EVBDD</scp>s, called <it>Structural</it><scp>EVBDD</scp>s, and show how they can be used for hierarchical verification.</p>
INDEX TERMS
Binary decision diagrams, Boolean functions, pseudo-Boolean functions, verification
CITATION
Sarma B.K. Vrudhula, Massoud Pedram, Yung-Te Lai, "Formal Verification Using Edge-Valued Binary Decision Diagrams", IEEE Transactions on Computers, vol. 45, no. , pp. 247-255, February 1996, doi:10.1109/12.485378
99 ms
(Ver 3.1 (10032016))