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 andnational security. Furthermore, for the companies that design and manufacturemicroprocessors 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 newproducts. 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 VLIWdesigns. Presents a highly automatic and scalable method for formal verification of a wide variety of modern microprocessors Includes a companion software tool flow for design and formal verification of pipelined, superscalar, and VLIW microprocessors Provides exercises and projects to use the tool flow to design and verify microprocessors of increasing complexity Includes a large collection of student bugs from past implementations of the projects to design and verify processors, including variants with exceptions and branch prediction—excellent basis for training in debugging Presents content in an accessible manner to readers with no previous background in formal methods Class-tested at Georgia Institute of Technology, and University of Illinois at Chicago INDICE: Introduction.- Symbolic Simulation.- High-Level Modeling of Microprocessors.- Boolean Satisfiability Procedures.- Proving Safety of Pipelined Microprocessors by Exploiting Positive Equality.- Formal Verification of Pipelined Microprocessors with Exceptions, Branch Prediction, and Multicycle Functional Units.- Analysis of Counterexamples.- Formal Verification of Pipelined Microprocessors with Instruction Queues.- Formal Verification of Pipelined Microprocessors with Delayed Branches.- Formal Verification of Pipelined Microprocessors with Data Value Prediction.- Formal Verification of Binary Code Compatibility of Pipelined Microprocessors.- Using Positive Equality to Prove Liveness of Pipelined Microprocessors.- Proving Liveness for Pipelined Microprocessors with Multicycle Functional Units.- Formal Verification of a VLIW Processor Inspired by the Intel Itanium.- Formal Verification of an Out-of-Order SuperscalarProcessor Inspired by the PowerPC 750.- Translating Equational Logic to Boolean Formulas.- Applying Rewriting Rules to Automatically Abstract Memories.- Efficient Translation to CNF by Exploiting the Block-Level Structure of Boolean Formulas.- Exploiting Unobservability in Translation to SAT.- Efficient Use ofParallel Processor Environments for SAT Solving.- Putting the SAT Techniques All Together.- Appendix A: The High-Level Hardware Description Language AbsHDL.- Appendix B: The Tool Flow for Formal Verification of Pipelined/Superscalar/VLIW Microprocessors.- Appendix C: Classification and Description of Student Bugs from Past Implementations of the Projects.

• ISBN: 978-1-4419-0955-8
• Editorial: Springer
• Encuadernacion: Cartoné
• Páginas: 490
• Fecha Publicación: 01/05/2010
• Nº Volúmenes: 1
• Idioma: Inglés