TED+: a data structure for microprocessor verification

Formal verification of microprocessors requires a mechanism for efficient representation and manipulation of both arithmetic and random Boolean functions. Recently, a new canonical and graph-based representation called TED has been introduced for verification of digital systems. Although TED can be used effectively to represent arithmetic expressions at the word-level, it is not memory efficient in representing bit-level logic expressions. In this paper, we present modifications to TED to improve its ability for bit-level logic representation while maintaining its robustness in arithmetic word-level representation. It will be shown that for random Boolean expressions, the modified TED performs the same as BDD representation.