Formal Verification of Microprocessors: Automatic and Scalable Methods for Pipelined, Superscalar, and VLIW Designs

Formal verification is the mathematical proof of correctness of computer systems. Microprocessors are the most important components in computer systems, and are increasingly being used in safety-critical applications, e.g., to monitor the health of patients, to control the engines and breaks of cars, to drive autonomous vehicles and fly autonomous aircraft, and to control weapons systems. As such the correctness of microprocessors is a matter of public safety and national security. Furthermore, for the companies that design and manufacture microprocessors or systems controlled by them, the correctness of microprocessors is a matter of business success or failure. Statistics from industrial microprocessor designs indicate that up to 90% of the engineering effort is spent on verification, which increasingly becomes the bottleneck in developing new products. Formal verification has the potential to significantly reduce the design time, while also guaranteeing complete correctness. However, previous approaches for formal verification of microprocessors either do not scale for complex designs or require prohibitive amounts of manual effort by experts. In contrast, this book presents a highly automatic and scalable method for formal verification of complex processors, including pipelined, superscalar, and VLIW designs.