Equivalence checking of integer multipliers

Abstract

In this paper, we address on equivalence checking of integer multipliers, especially for the multipliers without structure similarity. Our approach is based on Hamaguchi's backward substitution method with the following improvements: (1) automatic identification of components to form proper cut points and thus dramatically improve the backward substitution process, (2) a layered-backward substitution algorithm to reduce the number of substitutions, and (3) Multiplicative Power Hybrid Decision Diagrams(*PHDDs) as our word-level representation rather than *BMD in Hamaguchi's approach. Experimental results show that our approach can efficiently check the equivalence of two integer multipliers. To verify the equivalence of a 32 x 32 array multiplier versus a 32 x 32 Wallace tree multiplier, our approach takes about 57 CPU seconds using ii Mbytes, while Stanion's approach took 21027 seconds using 130 MBytes. We also show that the complexity of our approach is upper bounded by O(n(4)), where n is the word size, but our experimental results show that the complexity of our approach grows cubically O(n(3)).