This book is best described as a collection of independent papers that describe experimental tool development and/or current research projects in the field of formal verification. It will be a good starting point for those contemplating new research projects on formal verification techniques, and a good reference source for those evaluating the state of the art in formal verification tools and methods that might be useful in current design projects. A unique feature of this book is the inclusion of formal verification methods for nonlinear analog circuits, as well as for traditional logic circuits. Although each set of authors is clearly biased toward their own experimental tool development, or their own research projects, each chapter, in addition to describing achievements, does an adequate job of identifying limitations and assumptions, outlining open problems, and suggesting avenues for future work.

As indicated by the word “advanced” in the title, some background in the basics of formal verification terminology is necessary to read the text. Many basic terms are either not defined, or, when defined, are not present in the index. I spent a lot of time searching the text for definitions, and a lot of time in the library looking up references to fill in the gaps in the development. A good index and glossary would have been very useful.

Chapter 1 describes the application of SAT-solvers (programs that solve the Boolean satisfiability problem: either find a set of values for the Boolean variables that cause a conjunctive normal form expression to evaluate to logic 1, or decide that no such solution exists) to determine whether two circuits display equivalent behavior. Since the SAT problem is known to be nondeterministic polynomial time (NP) complete, an efficient general solution is almost guaranteed not to exist. In this chapter, the authors introduce an efficient SAT algorithm that can determine whether two circuits that have a common specification are equivalent, and describe new research on stable sets of points that “may lead to SAT algorithms that are more efficient than the ones currently implemented in state of the art SAT-solvers.”

Chapter 2 compares the SAT-solver approach with the binary decision diagram (BDD) approach. It begins by introducing the two main approaches to formal verification: equivalence checking and model checking (also known as property checking). The authors’ research indicates that SAT and BDD methodologies have different classes of tractable instances, for both equivalence checking and model checking. Therefore, several admittedly immature approaches are described that attempt to combine the two techniques to exploit the best features of each.

Chapter 3 describes recent advances in equivalence checking for arithmetic circuits, which is known to be a particularly difficult problem. The main conclusion is that existing methods are only partial solutions, and that a great deal of research is needed to effectively address the equivalence of complex arithmetic circuits, particularly those containing multipliers.

Chapters 4 and 5 describe the property checking approach. Limitations of the property checking approach include knowing when enough properties have been checked to achieve a high degree of confidence that the design is functionally correct, and the fact that it is currently limited to relatively small circuit-level designs, because system-level properties, such as those needed to verify systems on a chip (SOC), do not exist. Chapter 4 introduces a tool, being developed by industry, that works by converting a property checking problem into an SAT problem, and then using a proprietary SAT-solver to prove the property. Chapter 5 describes a property specification language that is being developed to support assertion-based verification strategies.

Chapter 6, the most self-contained chapter in the book, describes formal verification methods for nonlinear analog systems. Since the approach is highly theoretical, a strong background in theoretical control system theory would enhance the reader’s ability to understand the methods. This chapter addresses both equivalence checking and model checking, and contains complete examples of each. Both approaches employ state-space models of the analog systems being verified. Currently, the approach is limited to time domain properties. Expansion to frequency domain properties is a future research direction.