Journal of Formalized Mathematics
Volume 12, 2000
University of Bialystok
Copyright (c) 2000 Association of Mizar Users

The Correctness of the High Speed Array Multiplier Circuits

Hiroshi Yamazaki
Shinshu University, Nagano
Katsumi Wasaki
Shinshu University, Nagano


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

The terminology and notation used in this paper have been introduced in the following articles [1]

Contents (PDF format)

  1. Preliminaries
  2. Logical Equivalence of Wallace Tree Multiplier


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

Received August 28, 2000

[ Download a postscript version, MML identifier index, Mizar home page]