Publication
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.
Giovanni De Micheli, Mathias Soeken, Dewmini Sudara Marakkalage, Eleonora Testa, Heinz Riener
Giovanni De Micheli, Mathias Soeken, Winston Jason Haaswijk, Zhufei Chu