Edge-valued binary decision for multi-level hierarchical verification

The authors present a new data structure called edge-valued binary decision diagrams (EVs) as a representation of functions. An EV is an extension of ordered binary decision diagrams that allows for multilevel and hierarchical verification. It is shown that an EV is a compact and canonical representation for arbitrary integer functions. Hence, the specification can be at a higher level than the implementation. The variable ordering strategy for an EV can be derived from a higher-level functional specification instead of the gate-level specification. Examples of the design of a 64-b comparator and of a 64-b ripple-carry adder are included