Digital systems verification is a very important topic of research and industrial practice. Anecdotally, about 70 percent of silicon design efforts today go into validation/verification.

Formal verification has made some inroads into industrial verification teams after the Pentium floating-point division bug fiasco, and subsequent demonstration of formal verification of the floating-point division implementation. At the moment, no top-of-the-line microprocessor design team lets a floating-point unit go without formal verification. However, control-oriented designs with large data paths pose a challenge. Simulation-based verification does not have adequate coverage; hence, it needs to be enhanced by some formal modeling and techniques, whether for more coverage-driven test generation, or for formal verification.

This book is a very short overview of formal and simulation-based verification. This vast topic could easily cover volumes, and books of about 900 pages exist that cover only model checking. There are books on discrete-event simulation that are equally large. One cannot expect, then, to learn a lot from a 79-page overview-type discourse on the two topics and their combination.

Consequently, the authors intend for this book to familiarize engineers and engineering managers--who might be completely new to pre-silicon validation and its terminologies--with the topic, and to briefly outline the most prevalent concepts. If I were a manager just taking over responsibility of a validation team from a past design-oriented job, I might read this book in a few hours to become familiar with the concepts.

The book covers a good range of concepts. It discusses behavior-driven development (BDD), satisfiability (SAT) and SAT solvers, state machines, pre/post image computation and combining BDD and SAT for state space “tunneling” (the term glorified by Jasper Design Automation), and genetic algorithm methods, giving each no more than one to two pages. The book then covers simulation techniques, briefly discussing compiled versus event-driven simulation, pros and cons, and simulation with more than two-valued signal logic. Finally, the book discusses combining simulation with formal verification, emphasizing symbolic simulation.

The authors seem to have collected a set of freely available tools--including Verification Interacting with Synthesis (VIS); Symbolic Trajectory Evaluation (STE); Speed5 (a five-valued simulation engine); and the Southern Methodist University Equivalence Checker (SMU-EQ)--and created a combination methodology and environment where they are available for design validation engineers to use in combination to achieve their goals. Industry validation managers such as Intel’s Bob Bentley have, in various invited talks, actually emphasized numerous times the need for combining all of these methods; hence, this is a useful chapter for the heretofore uninitiated engineer.

In summary, the book is cursory and is not a good source for teaching material or for in-depth learning of techniques. However, reading this book will give the uninitiated a quick overview to help them quickly grasp the big picture; busy professionals could read it in a few hours.