Logo - springer
Slogan - springer

Engineering - Circuits & Systems | Formal Verification of Microprocessors - Automatic and Scalable Methods for Pipelined, Superscalar,

Formal Verification of Microprocessors

Automatic and Scalable Methods for Pipelined, Superscalar, and VLIW Designs

Velev, Miroslav

2015, 490 p.

Available Formats:
eBook
Information

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.

 

ISBN 978-1-4419-0956-5

digitally watermarked, no DRM

The eBook version of this title will be available soon


learn more about Springer eBooks

add to marked items

Hardcover
Information

Hardcover version

You can pay for Springer Books with Visa, Mastercard, American Express or Paypal.

Standard shipping is free of charge for individual customers.

 
approx. $99.00

(net) price for USA

ISBN 978-1-4419-0955-8

free shipping for individuals worldwide

Due: August 3, 2015


add to marked items

  • About this textbook

  • 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

Related subjects » Circuits & Systems - Information Systems and Applications

Table of contents 

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.

Popular Content within this publication 

 

Articles

Services for this book

New Book Alert

Get alerted on new Springer publications in the subject area of Circuits and Systems.