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.


Published in:
Proceedings of the 2005 conference on Asia South Pacific design automation, 567-572
Presented at:
Asia and South Pacific Design Automation Conference, Shanghai, January 18-21, 2005
Year:
2005
Publisher:
Shanghai
Laboratories:




 Record created 2009-05-23, last modified 2018-03-17


Rate this document:

Rate this document:
1
2
3
 
(Not yet reviewed)