Chen and Bushnell describe an improved branch-and-bound search method for logic justification, a problem in computer-aided design (CAD). The improvement arises from avoiding duplicate computations (without using search decision trees).

In addition to providing an extensive set of references, the authors supply their SEST program on an accompanying disk. SEST is a deterministic gate-level sequential circuit automatic test pattern generation program (ATPG) for stuck-at faults. Thus, rather than having to implement Chen and Bushnell’s ideas, it is possible to see their immediate application.

There are two parts to the book. Part 1 (chapters 1–3) contains the theoretical foundation for the improved branch-and-bound technique. Part 2 (chapters 4–9) provides applications of the technique and a discussion of experimental results. The appendix is a user guide for SEST, and gives complete instructions for installing it on Unix.

Chapter 1 is an introduction, illustrating the savings possible when duplicate computations can be identified and avoided in the branch-and-bound search. Justification in logic circuits is the process of finding consistent input values in order to satisfy a given output value. Since this problem is NP-complete, Chen and Bushnell introduce their new concept of justification equivalence in chapter 2 to recognize when search decision spaces are identical. This is the key to their improved efficiency in branch-and-bound.

Chapter 3 shows that search efficiency is improved without using state-transition graphs. Instead, the authors present a method that dynamically gathers justification information while traversing the state space.

The chapters in Part 1 contain clear definitions and straightforward proofs of theorems. The many figures and examples are helpful in understanding the ideas behind justification equivalence.

Chapter 4 presents the application of sequential circuit test generation, showing how justification equivalence can improve search efficiency, as compared with many other methods. The stuck-at fault model is introduced in chapter 5. Some care is required to determine whether prior justifications are eligible, meaning that the fault does not change the subsequent decision tree.

Chapter 6 is devoted to describing the SEST algorithm. Test generation has four phases in SEST: preprocessing, target fault analysis, test generation, and postprocessing. The sequential circuit model, fault model, and ATPG search heuristics used are also described. The flow charts of the algorithms are provided, as is a detailed description of the methods of retrieving learned justification information. In chapter 7, experimental results of justification equivalence are tabulated and analyzed. The results are compared with other test generation programs. Currently, the retrieval process is the bottleneck in SEST.

Chapters 8 and 9 present two final applications. In order to remove redundancy from a circuit, it must first be identified. Chapter 8 shows how justification equivalence is used to improve redundancy identification. In chapter 9, the logic verification problem is reduced to a test generation problem.

Like those in Part 1, all chapters in Part 2 are accompanied by a large number of figures and examples. This short book provides a detailed and easy-to-understand description of justification equivalence. For readers not familiar with ATPG, it may be helpful to read chapter 4 first.