Automatic and Scalable Methods for Pipelined, Superscalar, and VLIW Designs
2015, 490 p.
Springer eBooks may be purchased by end-customers only and are sold without copy protection (DRM free). Instead, all eBooks include personalized watermarks. This means you can read the Springer eBooks across numerous devices such as Laptops, eReaders, and tablets.
You can pay for Springer eBooks with Visa, Mastercard, American Express or Paypal.
After the purchase you can directly download the eBook file or read it online in our Springer eBook Reader. Furthermore your eBook will be stored in your MySpringer account. So you can always re-download your eBooks.
digitally watermarked, no DRM
The eBook version of this title will be available soon
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 the VLIW microprocessors
Provides exercises and projects
Includes a large collection of student bugs from past implementations of the projects to design and verify processors, including variants
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.
Content Level »Professional/practitioner
Keywords »Design Debugging - Formal Methods - Formal Verification - Model Checking - Pipelined Verification - SAT Solvers - Superscalar Verification - VLIW Verification - Verification of Microprocessors
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 Superscalar Processor 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 of Parallel Processor Environments for SAT Solving.- Putting the SAT Techniques All Together.