Induction-based gate-level verification of multipliers

We propose a method based on unrolling the inductive definition of binary number multiplication to verify gate-level implementations of multipliers. The induction steps successively reduce the size of the multiplier under verification. Through induction, the verification of an n-bit multiplier is decomposed into n equivalence checking problems. The resulting equivalence checking problems could be significantly sped up by simple structural analysis. This method could be generalized to the verification of more general arithmetic circuits and the equivalence checking of complex datapaths.