Issue No. 02 - February (1996 vol. 45)
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/12.485378
<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>
Binary decision diagrams, Boolean functions, pseudo-Boolean functions, verification
S. B. Vrudhula, M. Pedram and Y. Lai, "Formal Verification Using Edge-Valued Binary Decision Diagrams," in IEEE Transactions on Computers, vol. 45, no. , pp. 247-255, 1996.