Formal Verification

An Essential Toolkit for Modern VLSI Design
 
 
Morgan Kaufmann (Verlag)
  • 1. Auflage
  • |
  • erschienen am 24. Juli 2015
  • |
  • 408 Seiten
 
E-Book | ePUB mit Adobe DRM | Systemvoraussetzungen
E-Book | PDF mit Adobe DRM | Systemvoraussetzungen
978-0-12-800815-7 (ISBN)
 

Formal Verification: An Essential Toolkit for Modern VLSI Design presents practical approaches for design and validation, with hands-on advice for working engineers integrating these techniques into their work.

Building on a basic knowledge of System Verilog, this book demystifies FV and presents the practical applications that are bringing it into mainstream design and validation processes at Intel and other companies. The text prepares readers to effectively introduce FV in their organization and deploy FV techniques to increase design and validation productivity.


  • Presents formal verification algorithms allowing users to gain full coverage without exhaustive simulation
  • Provides discussion of formal verification tools and how they differ from simulation tools
  • Teaches users how to glean insights into how models work to find initial bugs
  • Presents valuable information from an Intel insider who shares his hard-won knowledge and solutions to complex design problems


Erik has worked at Intel Corporation in Hillsboro, Oregon for over two decades, in a variety of positions involving software, design, simulation, and formal verification. Currently he works in the Design Technology and Solutions division, where he supports formal verification usage for Intel teams worldwide. In his spare time he hosts the 'Math Mutation" podcast, and serves as an elected director on the Hillsboro school board.
  • Englisch
  • San Francisco
  • |
  • USA
Elsevier Science
  • 10,86 MB
978-0-12-800815-7 (9780128008157)
0128008156 (0128008156)
weitere Ausgaben werden ermittelt
  • Front Cover
  • Formal Verification
  • Copyright Page
  • Contents
  • Foreword for "Formal Verification: An Essential Toolkit for Modern VLSI Design"
  • Acknowledgments
  • 1 Formal verification: from dreams to reality
  • What Is FV?
  • Why This Book?
  • A Motivating Anecdote
  • FV: The Next Level of Depth
  • Overall Advantages of FV
  • General Usage Models for FV
  • FV for Complete Coverage
  • FV for Bug Hunting
  • FV for Exploring Designs
  • FV in Real Design Flows
  • FV Methods Not Discussed In This Book
  • The Emergence of Practical FV
  • Early Automated Reasoning
  • Applications to Computer Science
  • Model Checking Becomes Practical
  • The Standardizing of Assertions
  • Challenges in Implementing FV
  • Fundamental Limitations of Mathematics
  • Complexity Theory
  • The Good News
  • Amplifying the Power of Formal
  • Getting the Most Out of This Book
  • Practical Tips from This Chapter
  • Further Reading
  • 2 Basic formal verification algorithms
  • Formal Verification (FV) in the Validation Process
  • A Simple Vending Machine Example
  • Comparing Specifications
  • Cones of Influence
  • Formalizing Operation Definitions
  • Building Truth Tables Intelligently
  • Adding Sequential Logic
  • Boolean Algebra Notation
  • Basic Boolean Algebra Laws
  • Comparing Specifications
  • BDDs
  • Computing a BDD for a Circuit Design
  • Model Checking
  • Boolean Satisfiability
  • Bounded Model Checking
  • Solving the SAT Problem
  • The Davis-Putnam SAT Algorithm
  • The Davis Logemann Loveland (DLL) SAT Algorithm
  • Additional SAT Algorithm Improvements
  • Chapter Summary
  • Further Reading
  • 3 Introduction to systemverilog assertions
  • Basic Assertion Concepts
  • A Simple Arbiter Example
  • What are Assertions?
  • What are Assumptions?
  • What are Cover Points?
  • Clarification on Assertion Statements
  • SVA Assertion Language Basics
  • Immediate Assertions
  • Writing Immediate Assertions
  • Complications of Procedural Code and Motivation for Assert Final
  • Location in Procedural Blocks
  • Boolean Building Blocks
  • Concurrent Assertion Basics and Clocking
  • Sampling and Assertion Clocking
  • Sampled Value Functions
  • Concurrent Assertion Clock Edges
  • Concurrent Assertion Reset (Disable) Conditions
  • Setting Default Clock and Reset
  • Sequences, Properties, and Concurrent Assertions
  • Sequence Syntax and Examples
  • Using sequences instead of $rose/$fell
  • Property Syntax and Examples
  • Named Sequences and Properties
  • Assertions and Implicit Multithreading
  • Writing the Properties
  • Planning properties at the specification phase
  • Embedded properties during RTL development
  • Validation-focused properties
  • Connecting the properties to your design
  • Summary
  • Practical Tips from this Chapter
  • Further Reading
  • 4 Formal property verification
  • What is FPV?
  • Example for this Chapter: Combination Lock
  • Bringing Up a Basic FPV Environment
  • Compiling your RTL
  • Creating cover points
  • Creating assumptions
  • Creating assertions
  • Clocks and resets
  • Running the verification
  • How is FPV Different from Simulation?
  • What Types and Sizes of Models can be Run?
  • How Do We Reach Targeted Behaviors?
  • Simulation
  • FPV
  • What Values are Checked?
  • Simulation
  • FPV
  • How do we constrain the model?
  • Simulation
  • FPV
  • How are constraints on internal nodes handled?
  • Simulation
  • FPV
  • What do we use for debug?
  • Simulation
  • FPV
  • How long are typical traces?
  • Simulation
  • FPV
  • Deciding Where and How to Run FPV
  • Motivations for running FPV
  • Using design exercise FPV
  • Using bug hunting FPV
  • Using full proof FPV
  • Using application-specific FPV
  • Summary
  • Practical Tips from this Chapter
  • Further Reading
  • 5 Effective FPV for design exercise
  • Example for This Chapter: Traffic Light Controller
  • Creating a Design Exercise Plan
  • Design Exercise Goals
  • Major Properties for Design Exercise
  • Complexity Staging Plan
  • Exit Criteria
  • Putting it All Together
  • Setting Up the Design Exercise FPV Environment
  • Cover Points
  • Assumptions
  • Assertions
  • Clocks and Resets
  • Sanity-Checks
  • Wiggling the Design
  • The Wiggling Process
  • Wiggling Stage 1: Our First Short Waveform
  • Debugging Another Short Waveform
  • Exploring More Interesting Behaviors
  • Answering Some New Questions
  • Proving the Assertions
  • Removing Simplifications and Exploring More Behaviors
  • Facing Complexity Issues
  • Summary
  • Practical Tips from this Chapter
  • Further Reading
  • 6 Effective FPV for verification
  • Deciding on Your FPV Goals
  • Bug Hunting FPV
  • Full Proof FPV
  • Staging Your FPV Efforts
  • Example for this Chapter: Simple ALU
  • Understanding the Design
  • Creating the FPV Verification Plan
  • FPV Goals
  • Major Properties for FPV
  • Cover points
  • Assumptions
  • Assertions
  • Reference modeling and properties
  • Addressing Complexity
  • Staging plan
  • Blackboxes
  • Structural abstraction
  • Quality Checks and Exit Criteria
  • Exit criteria
  • Putting it all together
  • Running bug hunting FPV
  • Initial Cover Points
  • Extended Wiggling
  • Expanding the Cover Points
  • Removing Simplifications and Exploring More Behaviors
  • The Road to Full Proof FPV
  • Summary
  • Practical Tips from this Chapter
  • Further Reading
  • 7 FPV "Apps" for specific SOC problems
  • Reusable Protocol Verification
  • Basic Design of the Reusable Property Set
  • Property Direction Issues
  • Verifying Property Set Consistency
  • Checking Completeness
  • Unreachable Coverage Elimination
  • The Role of Assertions in UCE
  • Covergroups and Other Coverage Types
  • Connectivity Verification
  • Model Build for Connectivity
  • Specifying the Connectivity
  • Possible Connectivity FPV Complications
  • Control Register Verification
  • Specifying Control Register Requirements
  • SVA Assertions for Control Registers
  • Major Challenges of Control Register Verification
  • Post-Silicon Debug
  • Building the FPV Environment
  • The Paradox of Too Much Information
  • Using Semiformal Design Exploration
  • Proving your Bug Fixes Correct
  • Summary
  • Practical Tips from this Chapter
  • Further Reading
  • 8 Formal equivalence verification
  • Types of Equivalence to Check
  • Combinational Equivalence
  • Sequential Equivalence
  • Transaction-Based Equivalence
  • FEV Use Cases
  • RTL to Netlist FEV
  • RTL to RTL FEV
  • Parameterization
  • Timing fixes-logic redistribution
  • Timing fixes-critical path reduction
  • Pipeline optimizations
  • Chicken bit validation
  • Clock gating verification
  • Running FEV
  • Choosing the Models
  • Which models to verify?
  • Cell libraries
  • Key Point Selection and Mapping
  • Defining the mappings
  • State negation
  • State replication
  • Unreachable points
  • Delayed and conditional mappings
  • Debugging mapping failures
  • Assumptions and Constraints
  • Removing some functionality
  • Scan (and other netlist-only feature) insertion
  • Debugging Mismatches
  • Additional FEV Challenges
  • Latch/Flop Optimizations
  • Conditional Equivalence
  • Don't Care Space
  • Complexity
  • Summary
  • Practical Tips from this Chapter
  • Further Reading
  • 9 Formal verification's greatest bloopers: the danger of false positives
  • Misuse of the SVA Language
  • The Missing Semicolon
  • Assertion at Both Clock Edges
  • Short-Circuited Function with Assertion
  • Subtle Effects of Signal Sampling
  • Liveness Properties that are Not Alive
  • Preventing SVA-Related False Positives
  • Vacuity Issues
  • Misleading Cover Point with Bad Reset
  • Proven Memory Controller that Failed Simulation
  • Contradiction Between Assumption and Constraint
  • The Queue that Never Fills, Because it Never Starts
  • Preventing Vacuity: Tool and User Responsibility
  • Implicit or Unstated Assumptions
  • Libraries with Schematic Assumptions
  • Expectations for Multiply-Driven Signals
  • Unreachable Logic Elements: Needed or Not?
  • Preventing Misunderstandings
  • Division of Labor
  • Loss of Glue Logic
  • Case-Splitting with Missing Cases
  • Undoing Temporary Hacks
  • Safe Division of Labor
  • Summary
  • Practical Tips from This Chapter
  • Further Reading
  • 10 Dealing with complexity
  • Design State and Associated Complexity
  • Example for this Chapter: Memory Controller
  • Observing Complexity Issues
  • Simple Techniques for Convergence
  • Choosing the Right Battle
  • Engine Tuning
  • Blackboxing
  • Parameters and Size Reduction
  • Case-Splitting
  • Property Simplification
  • Boolean simplifications
  • Making liveness properties finite
  • Cut Points
  • Blackboxes with holes
  • Semiformal Verification
  • Incremental FEV
  • Helper Assumptions . and Not-So-Helpful Assumptions
  • Writing Custom Helper Assumptions
  • Leveraging Proven Assertions
  • Do You have too Many Assumptions?
  • Generalizing Analysis Using Free Variables
  • Exploiting Symmetry with Rigid Free Variables
  • Other Uses of Free Variables
  • Downsides of Free Variables
  • Abstraction Models for Complexity Reduction
  • Counter Abstraction
  • Sequence Abstraction
  • Memory Abstraction
  • Shadow Models
  • Summary
  • Practical Tips from this Chapter: Summary
  • Further Reading
  • 11 Your new FV-aware lifestyle
  • Uses of FV
  • Design Exercise
  • Bug Hunting FPV
  • Full Proof FPV
  • Specialized FPV Using Apps
  • Formal Equivalence Verification
  • Getting Started
  • Engineer Preparation to Use FV
  • Tool Preparation
  • Making Your Manager Happy
  • ROI Calculation
  • Bug Complexity Ranking
  • Progress Tracking
  • What Do FVers Really Do?
  • Summary
  • Further Reading
  • Index

Foreword for "Formal Verification: An Essential Toolkit for Modern VLSI Design"


Robert Bentley, Former Director, Formal Verification Center of Expertise, Intel

Complex VLSI designs pervade almost every aspect of modern life. We take for granted the existence of cell phones, or antilock braking systems, or web servers, without even being aware of the technology under the hood. As users or customers, we also take it for granted that these devices will function correctly. The impact of an undetected functional failure can range from mild annoyance to major catastrophe, and the potential cost-to individuals, to companies, to society as a whole-can be immense. As just one example, the Pentium® "FDIV" bug in 1994 resulted in Intel Corporation taking a $475M charge against earnings to cover the cost associated with replacement of the defective CPUs.

The danger of an undetected functional failure is compounded by the relentless march of semiconductor process technology-"Moore's Law"-that allows us to put ever more complex designs onto a single piece of silicon. With this complexity come an increasing number of bugs, which need to be found and fixed before the design can be qualified for production use. With shorter design cycles and increased competitive pressure to get products to market faster, verification is now the critical path to production. The authors of the 2011 International Technology Roadmap for Semiconductors described verification as "a bottleneck that has now reached crisis proportions."

The traditional "dynamic testing" approach to design verification has been to:

 Create a verification wrapper or "testbench" around all or part of the design

 Write focused tests, or generate directed random tests, in order to stimulate the design

 Run these tests on an executable software model of the design (typically written at the Register Transfer Level, or RTL for short)

 Debug any resulting failures, fix the offending component (either the RTL, the testbench, or the test itself), and re-run tests until the design is "clean"

However, this approach has a number of drawbacks:

 Testbench development can be a lengthy process-typically of the order of months for complex areas of the design

 Testbench development is an error-prone activity, often creating a number of bugs in the testbench equal to or greater than the number that exist in the actual RTL

 Test execution is an expensive business-Intel dedicates tens of thousands of high-performance computer servers to this problem running around the clock, along with dedicated emulation hardware and FPGA-based solutions

 Tests themselves may contain errors that either mask problems in the RTL (false positives) or wrongly indicate errors that do not in fact exist (false negatives)

 Debug of failing tests is a major effort drain-often the largest single component of validation effort-in part because the failure is often detected only long after the point at which it occurred

 It is in general hard to tell how much of the design has been exercised ("covered") by any given set of tests, so even if all tests are passing it still isn't clear that the design is really clean

 Bug detection via dynamic testing is an inherently sequential process, often referred to as "peeling the onion," since bugs can and do hide behind other bugs

 Some bugs-like the Pentium® FDIV bug mentioned earlier-are data-dependent, or involve such a complex set of microarchitectural conditions that it is highly unlikely that they will be hit by random testing on an RTL model

A different approach, formal verification (FV), has gained acceptance in recent years as a shorter-time, lower-effort, and more comprehensive alternative to dynamic testing. The purpose of this book is to explain what FV is, why it offers at least a partial solution to the limitations of dynamic testing, and how, when, and where it should be applied.

FV is a powerful technique that enables a design or validation engineer to directly analyze and mathematically explore the quality or other aspects of an RTL design, providing 100% coverage of large subsets of the design space without needing to create a simulation testbench or test vectors. Its usage and development have been growing at Intel over the last two decades, and it is now increasingly considered a mainstream technique for both design and validation.

The authors of this book start by describing their goal: helping VLSI designers and validators who focus on RTL to do their jobs more effectively and efficiently by leveraging FV techniques. This approach is sometimes referred to at Intel as the democratization of FV, or "FV for All," since the intent is to expand the use of FV beyond the realm of FV experts and enable much wider use of FV tools and techniques. They briefly describe the history of FV: how early artificial intelligence concepts led to formal verification; theoretical objections to formal verification and why they are not true blocking issues; and general techniques for abstracting problems to make them more tractable for formal verification.

Chapter 2 describes basic FV algorithms in enough detail to convince the reader that FV isn't some form of black magic-these techniques really do gain full coverage without requiring exhaustive (and computationally infeasible) simulation cycles. In particular, the Boolean satisfiability (SAT) problem is explained, along with a description of the model-checking algorithms and tools that allow it to be solved for many classes of problem.

Chapter 3 provides an introduction to System Verilog Assertions (SVAs): what they are (and the different types of SVAs such as simple Boolean conditions, temporal assertions, etc.) and how they can be combined into sequences and properties. Chapter 4 builds on this by introducing the concept of Formal Property Verification (FPV): what it is; how it compares with dynamic simulation; and usage models such as design exploration, bug hunting, and bounded- and full-proofs.

The heart of the book lies in Chapters 5 and 6, which explain how to make effective use of FPV for Design Exercise and Verification, respectively. The authors' extensive experience with the application of FPV to real-world problems illuminates almost every page of these two chapters with examples gleaned from current and past Intel development projects, along with many helpful hints that will enable the novice user to make effective use of FPV tools.

Chapter 7 switches gears to describe how FPV can be used to create "Apps" for different design domains such as post-silicon bug reproduction, SoC connectivity checking, standard (non-project-specific) protocol verification, unreachable coverage elimination, and control register access policies. These apps enable design and validation engineers who do not have an FV background to quickly apply formal verification methods to the targeted domains, rather than relying on expensive and time-consuming dynamic simulation.

Chapter 8 discusses Formal Equivalence Verification (FEV), which is one of the most mature FV techniques and one that has been deployed at Intel for many years to ensure that RTL matches schematics, and hence that validation results from RTL simulation or formal verification will be applicable to the functional correctness of actual silicon.

Chapter 9-"FV's Greatest Bloopers: False Positives in Formal Verification" is worth the price of the book all by itself. It discusses some of the limitations of formal methods, in particular, the so-called "vacuity" issue, which is an assumption or set of assumptions that rules out legal data and hence leads to false positives (the absence of counter-examples). The examples given in this chapter, and the tips for avoiding these kinds of real-world problems, are worth their weight in gold!

With all of the benefits that FV can provide, the astute reader may be wondering why the technique is not already used more widely as an integral part of the VLSI design process. The answer is that design complexity, and the capacity needed to handle it, can overwhelm even the best FV tools. Chapter 10 addresses this critical issue, first describing the general concepts of complexity and NP-completeness, and then identifying complexity reduction techniques such as black boxing, case splitting, and property simplification that can be used to make FV a tractable solution. Here again, the authors' experience with complex real-world designs enables them to provide practical advice and solutions to what can appear to be daunting problems.

Chapter 11 wraps things up by describing how the reader can introduce the techniques described in this book into his or her organization, and effectively deploy them to increase design and validation productivity. Once again, the emphasis is on the practical: solving real-life problems, using small experiments to demonstrate the power of FPV techniques, getting measurable results and data that help to convince skeptics.

This book is a valuable addition to the library of both experienced and novice users of formal tools and methods. It has my highest...

Dateiformat: EPUB
Kopierschutz: Adobe-DRM (Digital Rights Management)

Systemvoraussetzungen:

Computer (Windows; MacOS X; Linux): Installieren Sie bereits vor dem Download die kostenlose Software Adobe Digital Editions (siehe E-Book Hilfe).

Tablet/Smartphone (Android; iOS): Installieren Sie bereits vor dem Download die kostenlose App Adobe Digital Editions (siehe E-Book Hilfe).

E-Book-Reader: Bookeen, Kobo, Pocketbook, Sony, Tolino u.v.a.m. (nicht Kindle)

Das Dateiformat EPUB ist sehr gut für Romane und Sachbücher geeignet - also für "fließenden" Text ohne komplexes Layout. Bei E-Readern oder Smartphones passt sich der Zeilen- und Seitenumbruch automatisch den kleinen Displays an. Mit Adobe-DRM wird hier ein "harter" Kopierschutz verwendet. Wenn die notwendigen Voraussetzungen nicht vorliegen, können Sie das E-Book leider nicht öffnen. Daher müssen Sie bereits vor dem Download Ihre Lese-Hardware vorbereiten.

Weitere Informationen finden Sie in unserer E-Book Hilfe.


Dateiformat: PDF
Kopierschutz: Adobe-DRM (Digital Rights Management)

Systemvoraussetzungen:

Computer (Windows; MacOS X; Linux): Installieren Sie bereits vor dem Download die kostenlose Software Adobe Digital Editions (siehe E-Book Hilfe).

Tablet/Smartphone (Android; iOS): Installieren Sie bereits vor dem Download die kostenlose App Adobe Digital Editions (siehe E-Book Hilfe).

E-Book-Reader: Bookeen, Kobo, Pocketbook, Sony, Tolino u.v.a.m. (nicht Kindle)

Das Dateiformat PDF zeigt auf jeder Hardware eine Buchseite stets identisch an. Daher ist eine PDF auch für ein komplexes Layout geeignet, wie es bei Lehr- und Fachbüchern verwendet wird (Bilder, Tabellen, Spalten, Fußnoten). Bei kleinen Displays von E-Readern oder Smartphones sind PDF leider eher nervig, weil zu viel Scrollen notwendig ist. Mit Adobe-DRM wird hier ein "harter" Kopierschutz verwendet. Wenn die notwendigen Voraussetzungen nicht vorliegen, können Sie das E-Book leider nicht öffnen. Daher müssen Sie bereits vor dem Download Ihre Lese-Hardware vorbereiten.

Weitere Informationen finden Sie in unserer E-Book Hilfe.


Download (sofort verfügbar)

85,62 €
inkl. 19% MwSt.
Download / Einzel-Lizenz
ePUB mit Adobe DRM
siehe Systemvoraussetzungen
PDF mit Adobe DRM
siehe Systemvoraussetzungen
Hinweis: Die Auswahl des von Ihnen gewünschten Dateiformats und des Kopierschutzes erfolgt erst im System des E-Book Anbieters
E-Book bestellen

Unsere Web-Seiten verwenden Cookies. Mit der Nutzung dieser Web-Seiten erklären Sie sich damit einverstanden. Mehr Informationen finden Sie in unserem Datenschutzhinweis. Ok