Title :
Scalable hybrid verification of complex microprocessors
Author :
Mneimneh, Maher ; Aloul, Fadi ; Weaver, Chris ; Chatterjee, Saugata ; Sakallah, Karem ; Austin, Todd
Author_Institution :
Michigan Univ., Ann Arbor, MI, USA
Abstract :
We introduce a new verification methodology for modern microprocessors that uses a simple checker processor to validate the execution of a companion high-performance processor. The checker can be viewed as an at-speed emulator that is formally verified to be compliant to an ISA specification. This verification approach enables the practical deployment of formal methods without impacting overall performance.
Keywords :
Boolean functions; development systems; formal verification; logic CAD; microprocessor chips; ISA specification; at-speed emulator; checker processor; complex microprocessors; formal methods; scalable hybrid verification; Batteries; Computer bugs; Degradation; Instruction sets; Microprocessors; Modems; Out of order; Permission; Testing; Virtual manufacturing;
Conference_Titel :
Design Automation Conference, 2001. Proceedings
Print_ISBN :
1-58113-297-2
DOI :
10.1109/DAC.2001.156105
