Improving Logic-Level Representation of Taylor Expansion Diagram Using Attributed Edges

Formal verification of complex digital systems requires a mechanism for efficient representation and manipulation of arithmetic as well as random Boolean functions. Although the Taylor Expansion Diagram can be used effectively to represent arithmetic expressions at the vector level, it is not efficient in the use of memory for representing bit-level logic expressions. In this paper, we present modifications to TED that will improve its ability for logic representation while maintaining its robustness in arithmetic representation. Our experimental results show a 30% reduction in the number of nodes in some benchmarks.