Lotfi-Kamran, P.Hosseinabady, M.Shojaei, H.Massoumi, M.Navabi, Z.2009-05-232009-05-232009-05-23200510.1109/ASPDAC.2005.1466228https://infoscience.epfl.ch/handle/20.500.14299/40222Formal 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.text::conference output::conference proceedings::conference paper