A practical methodology for verifying pipelined microarchitectures
Ravi Hosabettu, Ganesh K. Gopalakrishnan, Mandayam K. Srivas · IEEE Design & Test of Computers · 2003
Complete formal verification has thus far never been achieved for a state-of-the-art, high-performance commercial microprocessor. However, this article presents a completion functions methodology, based on theorem proving, that has been applied successfully to a large variety of example pipelined architectures.