Formal Verification

An Essential Toolkit for Modern VLSI Design

Erik Seligman, Tom Schubert, M. V. Achutha Kiran Kumar, M V Achutha Kiran Kumar

• Publisher: Morgan Kaufmann
• Year: 2015
• eBook ISBN: 9780128008157
• Topic: Computer Science
• Subtopic: Programming
• Index: Computer Science

Formal Verification: An Essential Toolkit for Modern VLSI Design presents practical approaches for design and validation, with hands-on advice to help working engineers integrate these techniques into their work. Formal Verification (FV) enables a designer to directly analyze and mathematically explore the quality or other aspects of a Register Transfer Level (RTL) design without using simulations. This can reduce time spent validating designs and more quickly reach a final design for manufacturing. Building on a basic knowledge of SystemVerilog, this book demystifies FV and presents the practical applications that are bringing it into mainstream design and validation processes at Intel and other companies. After reading this book, readers will be prepared to introduce FV in their organization and effectively deploy FV techniques to increase design and validation productivity.- Learn formal verification algorithms to gain full coverage without exhaustive simulation- Understand formal verification tools and how they differ from simulation tools- Create instant test benches to gain insight into how models work and find initial bugs- Learn from Intel insiders sharing their hard-won knowledge and solutions to complex design problems

Chapter 1

Formal verification

From dreams to reality

In Chapter 1, we introduce Formal Verification (FV): the use of tools that mathematically analyze the space of possible behaviors of a design, rather than computing results for particular values. We begin by describing the general concepts and motivations for using FV methods rather than simpler alternatives. We then discuss several major use cases: complete coverage, bug hunting, and exploring designs, as well as providing a brief discussion of more detailed methods used in typical industrial design and validation flows. Having introduced the general topic, we take a step back and briefly trace the historical development of the concepts of formal verification, from Leibniz’s 17th-century dreams to the realities of modern industry EDA tools. We discuss how FV relates to our understanding of the fundamental limitations of computing and mathematics, and the major techniques we use to get around these limitations and make FV a useful and powerful engineering technique. Finally, we provide some advice for getting the most out of this book.

Keywords

Assertions; Formal Verification (FEV); Formal Equivalence Verification (FEV); Formal Property Verification (FPV); Satisfiability; Undecidability; Complexity; NP-complete

It seems to me now that mathematics is capable of an artistic excellence as great as that of any music, perhaps greater; not because the pleasure it gives (although very pure) is comparable, either in intensity or in the number of people who feel it, to that of music, but because it gives in absolute perfection that combination, characteristic of great art, of godlike freedom, with the sense of inevitable destiny; because, in fact, it constructs an ideal world where everything is perfect and yet true.

—Bertrand Russell

Are you an engineer working on designing complex modern chips or System On Chips (SOCs) at the Register Transfer Level (RTL)? Have you ever been in one of the following frustrating situations?

• Your RTL designs suffered a major (and expensive) bug escape due to insufficient coverage of corner cases during simulation testing.

• You created a new RTL module and want to see its real flows in simulation, but realize this will take another few weeks of testbench development work.

• You tweaked a piece of RTL to aid synthesis or timing and need to spend weeks simulating to make sure you did not actually change its functionality.

• You are in the late stages of validating a design, and the continuing stream of new bugs makes it clear that your randomized simulations are just not providing proper coverage.

• You modified the control register specification for your design and need to spend lots of time simulating to make sure your changes to the RTL correctly implement these registers.

If so, congratulations: you have picked up the right book! Each of these situations can be addressed using formal verification (FV) to significantly increase both your overall productivity and your confidence in your results. You will achieve this by using formal mathematical tools to create orders-of-magnitude increases in efficiency and productivity, as well as introducing mathematical certainty into areas previously dependent on informal testing.

What is FV?

Let’s start with a simple definition:

• FV is the use of tools that mathematically analyze the space of possible behaviors of a design, rather than computing results for particular values.

What does this mean? Essentially, an FV tool will look at the full space of possible simulations, rather than trying specific values. It is not actually running all possible simulations, of course, but it will use clever mathematical techniques to consider all their possible behaviors. Figure 1.1 illustrates the difference between simulation and FV: simulation looks at individual points in the space of possible tests, while FV covers that whole space at once.

Figure 1.1 Coverage of your design space by simulation and FV. Simulation is like throwing darts at a target, while FV covers your whole target with a paint roller.

From this simple definition, you can probably already sense the amazing power we can gain from using this technique. In many areas, using this powerful method is no longer viewed as optional. You probably heard of the famous Pentium FDIV bug from the early 1990s, where certain rare cases were discovered in which Intel microprocessors could generate incorrect division results. This was a case where simulation-based verification simply failed to “throw the dart” at the right random test cases that would have revealed the issue before the product was on the market. Intel took a USD $475 million charge that year (about USD $755 million in 2014 dollars) to replace the processors; when you account for Intel’s growth since then, a similar recall today would have a cost in the billions. Thus, in mission-critical areas, FV is seen as essential for preventing dangerous bug escapes.

FV, however, is no longer just about finding rare bugs. As we will see when we explore the various techniques that are now available, FV should really be thought of as a general-purpose toolkit for interacting with, verifying, and understanding our designs. From the start of early development up through the post-silicon debug process, leveraging formal methods appropriately at every design phase can provide increased throughput, increase design confidence, and reduce time to market.

Why This Book?

Our goal is to provide useful tools for VLSI design and validation engineers. In the past, there have been numerous publications on FV from an academic standpoint, such as [Mcm93] and [Kro99]. However, these books have generally focused on theoretical foundations, the kind of things you would need to know to implement an advanced FV tool, rather than practical advice for the engineer who wants to apply such tools to solve real problems. In some ways, this is understandable, since until sometime during the past decade, FV was very difficult to use, and largely in the domain of researchers who specialized in the area.

On the other hand, in recent years, FV techniques have reached a level of maturity that few believed possible when they were first introduced. These techniques are easily usable by any engineer familiar with RTL design concepts and regularly used at all major companies doing VLSI design. We have used them in a variety of areas on numerous major projects at Intel, and have achieved a solid track record of valuable results: increasing productivity, identifying tricky corner-case bugs, and reducing time to market.

We still see, however, a large number of engineers who are somewhat afraid to tread into the waters of FV. Because formal methods do involve looking at your design in a fundamentally different way from simulation, mathematically examining the space of possible computations instead of trying out individual values, they do require a change of mindset that can be tricky at first. There is also the issue that many engineers still vaguely remember hearing that FV is something that those with PhDs do and are afraid to get started if they don’t have that level of qualification.

To those who are afraid to get started with FV, we have a clear message: Dive in! Two of the three authors of this book (Erik and Kiran) have no PhD, but they have successfully done FV on many different projects. The third (Tom) has managed a large and influential FV team whose members came in with a variety of qualifications and experience. Based on these experiences, we believe that FV has reached a level of maturity where an intelligent engineer without specialized training should consider it both highly usable and a regular part of their design and validation toolkit.

We also are focusing on RTL designs. While there are numerous levels of abstraction used in the design process, and constant claims that the industry is moving away from RTL to more abstract methods, we still see the majority of logic design activity occurring at the level of RTL. This is also where the Electronic Design Automation (EDA) industry currently delivers the most mature tools, due to the inherent compatibility of RTL with Boolean expression and logical analysis and the well-understood relationship between RTL designs and implemented circuits. For a practicing engineer looking to incorporate FV methods for the first time, we consider using mature industry tools on RTL models the best way to start.

Thus, our focus on this book is on practical RTL-related FV techniques that can be used by real engineers using off-the-shelf EDA tools. If you read about some technique in this book, you should be able to go straight to your desk and try it out afterwards.

A Motivating Anecdote

Many years ago, one of the authors of this book (Erik) was working in a small team in Intel’s Circuit Research Lab, designing and validating test chips to demonstrate new circuit techniques. One day a colleague stopped by his desk, holding a schematic diagram similar to Figure 1.2.

Figure 1.2 Example schematic implementing some complex logic.

The actual case had many more inputs and outputs, but this should give you the general flavor. Along with this schematic, he also had a specification table, similar to the one in Figure 1.3.

Figure 1.3 Specification for Table 3 schematic.

Due to the late arrival of the correct specification table and critical timing requirements in that area, the designer had decided to hand-implement an optimized schematic, a sea of gates that he believed was equivalent to the specified truth table. He had inserted an RTL view of the new version (in other words, a conversion of the schematic into a set of gates in our RTL language) into our full-chip model and verified that our simulation test suite did not generate any failures, but was nervous that our regression would only cover a small subset of the possible behaviors. This was a valid concern: even with this reduced example, you can see that it is very easy for a human to make a mistake that impacts only a small subset of the possible test cases. Take a close look at the schematic and the table. Can you spot the one case in the Figure 1.3 table that does not logically match the schematic in Figure 1.2? (It is the 1101 entry.)

Due to this risk, the colleague asked Erik if he could set up some kind of standalone validation environment for this recoded block that would quickly simulate all the possible input cases. However, reme...

Table of contents

• Cover image
• Title page
• Table of Contents
• Copyright
• Foreword for “Formal Verification: An Essential Toolkit for Modern VLSI Design”
• Acknowledgments
• Chapter 1. Formal verification: From dreams to reality
• Chapter 2. Basic formal verification algorithms
• Chapter 3. Introduction to systemverilog assertions
• Chapter 4. Formal property verification
• Chapter 5. Effective FPV for design exercise
• Chapter 6. Effective FPV for verification
• Chapter 7. FPV “Apps” for specific SOC problems
• Chapter 8. Formal equivalence verification
• Chapter 9. Formal verification’s greatest bloopers: The danger of false positives
• Chapter 10. Dealing with complexity
• Chapter 11. Your new FV-aware lifestyle
• Index