Reference:

Robert B. Jones. Symbolic Simulation Methods for Industrial Formal Verification. Kluwer Academic Publishers, 2002.

An extended and updated version of my dissertation [Jon99]

From the Preface by David Dill:

The most serious problem in modern hardware design is getting rid of the bugs. The debugging problem is growing much faster than other aspects of design. The main strategy for addressing this situation is incremental improvement of conventional approaches: faster simulators, better test environments, faster computers, and, of course, more money, time, and verification engineers.

As an alternative, people have begun looking at formal verification. Formal verification is characterized by exhaustive analysis of some aspect of design behavior. It is attractive because it is thorough. In contrast, conventional simulation can only check the behavior of a design on few test cases. For large modern designs, the proportion of behavior that can be covered is actually negligible.

This book examines a highly effective and somewhat neglected approach to formal verification: symbolic simulation. Among formal verification methods, model checking has received the lion's share of attention in recent years. Indeed, model checking has many advantages, but it's use is hampered by the so-called state explosion problem. For many designs, even those of modest size, the computational difficulty blows up out of control. Although symbolic simulation still has computational limits (the verification task is inherently hard), those limits are not as severe in practice, and symbolic simulation can be used so that performance degrades gracefully, instead of hitting hard limits.

A symbolic simulator is not a formal verifier by itself. It can be used for formal verification in a variety of ways, some of which are not initially obvious. The most important ideas in this book are new and interesting ways to use symbolic simulation to verify and debug complex hardware designs. For example, the idea of self consistency cleverly circumvents the practical barrier of writing formal specifications of correctness. It does this by comparing the behavior of a design in two modes that are intended by the designer to yield equivalent results.

The author solves a general problem in symbolic simulation: the user wants to prove property Q assuming that the inputs satisfy property P. It is possible to do proofs with a symbolic simulator in this way, but it is much more efficient to initialize the inputs to symbolic values which represent P in parameterized form. Using this transformation, along with the power of a symbolic simulator to simulate several different scenarios, it is possible to prove the correctness of a gate-level description of a floating-point adder used in Intel microprocessors.

By far the most impressive aspect of this work is that it has been battle-tested. It has solved some of the hardest verification problems at one of the world's premier (and dominant) hardware companies. This is particularly impressive, given that so much other work in formal verification has been purely theoretical, or, at best, tested on unrealistically small and simple problems.

In addition to the work that has immediate application, there is also an investigation into the potential of using symbolic simulation for verifying complete microprocessor designs at a much higher level of abstraction. A new approach, called incremental flushing, is proposed for mapping an out-of-order processor core to a simple instruction-set architecture. This extends previous techniques, which were applied to shallow pipelines, to much more deeply pipelined architectures.

The field of symbolic simulation is still immature. While I believe the work described here establishes some landmarks, it does not mark the end of the road. This book should be of interest to researchers in formal verification as well as those who are curious about the state of the art in formal verification.

Download not available.

BibTeX entry:

@book{Jones02Book,
 title 	   = {Symbolic Simulation Methods for 
              Industrial Formal Verification},
 author    = {Robert B. Jones},
 publisher = {Kluwer Academic Publishers},
 year      = 2002,
}