FORMAL VERIFICATION USING EDGE-VALUED BINARY DECISION DIAGRAMS

In this paper we present a new data structure called Edge-Valued Binar y-Decision Diagrams (EVBDD). An EVBDD is a directed acyclic graph, tha t provides a canonical and compact representation of functions that in volve both Boolean and integer quantities. In general, EVBDDS provide a more versatile and powerful representation that Ordinary Binary Deci sion Diagrams. We first describe the structure and properties of EVBDD S, 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 ver ification.