Improving Logic-Level Representation of BMD/TED Diagrams

Formal verification of complex digital systems requires a mechanism for efficient representation and manipulation of both arithmetic as well as random Boolean functions. Although BMD and its generalization TED can be used effectively to represent arithmetic expressions, they are not memory efficient in representing logic expressions. In this paper, we present modifications to BMD/TED that will improve their ability for logic representation while maintaining their robustness in arithmetic representation. Our experimental results show a 30% reduction in the number of nodes in some benchmarks.

Keywords:

Decision Diagrams , Binary Moment Diagrams , Taylor Expansion Diagrams , Formal Verification