Equivalence Checking of Arithmetic Circuits

Although equivalence checking technology has matured greatly during the last few years and designs with millions of gates can be handled, some specific problems remain to be difficult. Formal verification of arithmetic circuits, especially if multiplication is involved, is one of these problems. In this chapter we analyze origin and nature of this problem. We then review the most important research contributions targetting equivalence checking of arithmetics. Specifically, we outline techniques exploiting arithmetic functional properties and techniques based on binary decision diagrams, both on the bit and word levels. We also report on our own experiments with Multiplicative Binary Moment Diagrams (*BMDs). Finally, we introduce a new pragmatic approach to equivalence checking of arithmetic circuits. It extracts from a gate-level netlist an arithmetic bit-level representation of the circuit. Verification is carried out on this representation using a simple arithmetic calculus rather than a Boolean one. We show experimental results for successfully equivalence checking a large number of industrial multipliers as well as other circuits implementing more complex arithmetic expressions.