Foreword for “Formal Verification: An Essential Toolkit for Modern VLSI Design”

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:

However, this approach has a number of drawbacks:

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