Abelardo Pardo: Publications

Modular Verification of Multipliers

Kavita Ravi, Abelardo Pardo, Gary D. Hachtel, and Fabio Somenzi

Formal Methods in Computer Aided Design, LNCS 1196, pp. 49-63, Nov. 1996

Abstract

We present a new method for the efficient verification of multipliers and other arithmetic circuits. It is based on modular arithmetic like Kimura's approach, and on composition, like Hamaguchi's approach. It differs from both in several important respects, which make it more robust. The technique builds the residue Algebraic Decision Diagram (ADD) of as many variables as the number of outputs in the multiplier and composes the implementation circuit from the outputs to the inputs into the residue. Finally, the residue ADD is checked against the specification.

Click here to download the compressed postscript version.

BibTeX Entry

@InCollection{Ravi96,
  author = 	 {Kavita Ravi and Abelardo Pardo and G. Hachtel and
                  F. Somenzi},
  title = 	 {Modular Verification of Multipliers},
  booktitle = 	 {Formal Methods in Computer Aided Design},
  publisher =	 {Springer Verlag},
  year =	 1996,
  address =	 {Berlin},
  month =	 nov,
  pages =	 {49-63},
  note =	 {LNCS 1166}
}

Return to the home page