
Any reader familiar with computer organization knows the importance of the motherboard, the digital circuit for arithmetic logic units (ALUs), and the multiplier circuit for multiplying numbers. The subject of this book is verifying multiplier circuits. Specifically, it addresses some of the challenges in verification of structurally complex multiplier circuits.
First, the book gives an overview of verification methods for multiplier circuits. The overview mentions equivalence checking using binary decision diagrams, binary moment diagrams, and term rewriting systems. However, the book’s major contribution is the use of a symbolic computer algebra (SCA)-based method for verification. In the SCA-based verification method, the task is to formally prove that the gate-level netlist of the multiplier circuit is equivalent to the given specification polynomial.
Optimized circuits add complexity. Chapter 7 presents a method to verify such structurally complex multiplier circuits, including an algorithm, thorough explanations, and experimental results on various benchmarks. Chapter 8 has a method for debugging, along with the related algorithm. The complexity challenges are identified and addressed as a vanishing mononomial (chapter 4) and backward rewriting (chapters 5 and 6). The core algebra revolves around polynomial divisibility. Chapter 7’s algorithm uses four algorithms given in previous chapters. For details, the book’s appendix lists a website and references.
The book presents a method for integer multiplier circuits. Chapter 9 mentions that the method can also be used for verifying and debugging modular multipliers, truncated multipliers, and dividers. In addition to its research-related significance, the contribution can also be useful in commercial circuit designs.