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.
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...