TED+: a data structure for microprocessor verification
P. Lotfi-Kamran, Mohammad Hosseinabady, H. Shojaei, M. Massoumi, Zain Navabi · Proceedings of the ASP-DAC 2005. Asia and South Pacific Design Automation Conference, 2005. · 2005
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.