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.
- ISBN10 1441909559
- ISBN13 9781441909558
- Publish Date 1 May 2010
- Publish Status Cancelled
- Out of Print 16 February 2017
- Publish Country US
- Imprint Springer-Verlag New York Inc.
- Edition 2015 ed.
- Format Hardcover
- Pages 490
- Language English