The Correctness of the High Speed Array Multiplier Circuits

Hiroshi Yamazaki

Shinshu University, Nagano

Katsumi Wasaki

Shinshu University, Nagano

Summary.

This article introduces the verification of the correctness for the operations and the specification of the high speed array multiplier. We formalize the concepts of 2-by-2 and 3-by-3 bit Plain array multiplier, 3-by-3 Wallace tree multiplier circuit, and show that outputs of the array multiplier are equivalent to outputs of normal (sequencial) multiplier.

MML Identifier: GATE_5

Contents (PDF format)

1. Preliminaries
2. Logical Equivalence of Wallace Tree Multiplier

Bibliography

[1] Yatsuka Nakamura. Logic gates and logical equivalence of adders. Journal of Formalized Mathematics, 11, 1999.