Pejman Lotfi-Kamran - Electrical and Computer Engineering Department, Faculty of Engineering, University of Tehran, Tehran, Iran
Hamid Shojaei - Electrical and Computer Engineering Department, Faculty of Engineering, University of Tehran, Tehran, Iran
Hadi Parandeh-Afshar - Electrical and Computer Engineering Department, Faculty of Engineering, University of Tehran, Tehran, Iran
Mostafa Naderi - Electrical and Computer Engineering Department, Faculty of Engineering, University of Tehran, Tehran, Iran

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.

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