A practical methodology for verifying pipelined microarchitectures

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.