Scalable hybrid verification of complex microprocessors
Maher N. Mneimneh, Fadi Aloul, Chris Weaver, Saugata Chatterjee, Karem A. Sakallah, Todd M. Austin · 2001
We introduce a new verification methodology for modern micro-processors that uses a simple checker processor to validate the exe-cution 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 en-ables the practical deployment of formal methods without impact-ing overall performance.