Formal verification using edge-valued binary decision diagrams

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.