Equivalence checking of integer multipliers

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×32 array multiplier versus a 32×32 Wallace tree multiplier, our approach takes about 57 CPU seconds using 11 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⁴), where n is the word size, but our experimental results show that the complexity of our approach grows cubically O(n³)