Equivalence checking of integer multipliers

Abstract — In this paper, we address on equivalence checking of integer multipliers, especially for the multipliers without struc-ture similarity. Our approach is based on Hamaguchi’s backward substitution method with the following improvements: (1) auto-matic 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 Di-agrams(*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 array multiplier versus a 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 complex-ity of our approach is upper bounded by , where is the word size, but our experimental results show that the complexity of our approach grows cubically I