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

by
Hiroshi Yamazaki, and
Katsumi Wasaki

MML identifier: GATE_5
[ Mizar article, MML identifier index ]

```environ

vocabulary GATE_1, BOOLE, GATE_5;
notation XBOOLE_0, GATE_1;
constructors GATE_1, XBOOLE_0;
clusters XBOOLE_0;

begin

::The following 4 definitions are for normal 2-by-2 bit multiplier.

definition let x0,x1,y0,y1 be set;
func MULT210(x1,y1,x0,y0) -> set equals
:: GATE_5:def 1
AND2(x0,y0);

func MULT211(x1,y1,x0,y0) -> set equals
:: GATE_5:def 2

func MULT212(x1,y1,x0,y0) -> set equals
:: GATE_5:def 3

func MULT213(x1,y1,x0,y0) -> set equals
:: GATE_5:def 4
CARR2({},AND2(x1,y1),AND2(x1,y0),AND2(x0,y1),{});
end;

::
:: Logical Equivalence of 2-by-2 bit Plain Array Multiplier.
::

::The following theorem shows that
:: outputs of '2-by-2 bit plain Array Multiplier' are equivalent to
:: outputs of '2-by-2 normal Multiplier'
:: We assume that there is no feedback loop in multiplier.

theorem :: GATE_5:1 ::2AM:
for x0,x1,y0,y1,z0,z1,z2,z3,q00,q01,c01,q11,c11 being set holds
(\$q00 iff \$AND2(x0,y0))&
(\$q01 iff \$XOR3(AND2(x1,y0),AND2(x0,y1),{} ))&
(\$c01 iff \$MAJ3(AND2(x1,y0),AND2(x0,y1),{} ))&
(\$q11 iff \$XOR3(AND2(x1,y1),{} ,c01))&
(\$c11 iff \$MAJ3(AND2(x1,y1),{} ,c01))&
(\$z0 iff \$q00)&
(\$z1 iff \$q01)&
(\$z2 iff \$q11)&
(\$z3 iff \$c11)
implies
(\$z0 iff \$MULT210(x1,y1,x0,y0))&
(\$z1 iff \$MULT211(x1,y1,x0,y0))&
(\$z2 iff \$MULT212(x1,y1,x0,y0))&
(\$z3 iff \$MULT213(x1,y1,x0,y0));

::
:: Logical Equivalence of 3-by-3 bit Plain Array Multiplier.
::

::[sequence 1]
::The following 5 definitions are for normal 3-by-2 bit multiplier.

definition let x0,x1,x2,y0,y1 be set;
func MULT310(x2,x1,y1,x0,y0) -> set equals
:: GATE_5:def 5
AND2(x0,y0);

func MULT311(x2,x1,y1,x0,y0) -> set equals
:: GATE_5:def 6

func MULT312(x2,x1,y1,x0,y0) -> set equals
:: GATE_5:def 7
AND2(x1,y0),AND2(x0,y1),{});

func MULT313(x2,x1,y1,x0,y0) -> set equals
:: GATE_5:def 8
AND2(x2,y0),AND2(x1,y1),
AND2(x1,y0),AND2(x0,y1),{});

func MULT314(x2,x1,y1,x0,y0) -> set equals
:: GATE_5:def 9
CARR3({} ,AND2(x2,y1),
AND2(x2,y0),AND2(x1,y1),
AND2(x1,y0),AND2(x0,y1),{});
end;

::[sequence 2]
::The following 4 definitions are for normal 3-by-3 bit multiplier.

definition let x0,x1,x2,y0,y1,y2 be set;
func MULT321(x2,y2,x1,y1,x0,y0) -> set equals
:: GATE_5:def 10

func MULT322(x2,y2,x1,y1,x0,y0) -> set equals
:: GATE_5:def 11
MULT312(x2,x1,y1,x0,y0),AND2(x0,y2),{});

func MULT323(x2,y2,x1,y1,x0,y0) -> set equals
:: GATE_5:def 12
MULT313(x2,x1,y1,x0,y0),AND2(x1,y2),
MULT312(x2,x1,y1,x0,y0),AND2(x0,y2),{});

func MULT324(x2,y2,x1,y1,x0,y0) -> set equals
:: GATE_5:def 13
CARR3(MULT314(x2,x1,y1,x0,y0),AND2(x2,y2),
MULT313(x2,x1,y1,x0,y0),AND2(x1,y2),
MULT312(x2,x1,y1,x0,y0),AND2(x0,y2),{});
end;

::The following theorem shows that
:: outputs of '3-by-3 bit plain Array Multiplier' are equivalent to
:: outputs of '3-by-3 normal (sequencial) Multiplier'
:: We assume that there is no feedback loop in multiplier.

theorem :: GATE_5:2 ::3AM:
for x0,x1,x2,y0,y1,y2,z0,z1,z2,z3,z4,z5,
q00,q01,q02,c01,c02,q11,q12,c11,c12,q21,q22,c21,c22 being set holds
(\$q00 iff \$AND2(x0,y0))&
(\$q01 iff \$XOR3(AND2(x1,y0),AND2(x0,y1),{} ))&
(\$c01 iff \$MAJ3(AND2(x1,y0),AND2(x0,y1),{} ))&
(\$q02 iff \$XOR3(AND2(x2,y0),AND2(x1,y1),{} ))&
(\$c02 iff \$MAJ3(AND2(x2,y0),AND2(x1,y1),{} ))&
(\$q11 iff \$XOR3(q02 ,AND2(x0,y2),c01))&
(\$c11 iff \$MAJ3(q02 ,AND2(x0,y2),c01))&
(\$q12 iff \$XOR3(AND2(x2,y1),AND2(x1,y2),c02))&
(\$c12 iff \$MAJ3(AND2(x2,y1),AND2(x1,y2),c02))&
(\$q21 iff \$XOR3(q12 ,{} ,c11))&
(\$c21 iff \$MAJ3(q12 ,{} ,c11))&
(\$q22 iff \$XOR3(AND2(x2,y2),c21 ,c12))&
(\$c22 iff \$MAJ3(AND2(x2,y2),c21, c12))&
(\$z0 iff \$q00)&
(\$z1 iff \$q01)&
(\$z2 iff \$q11)&
(\$z3 iff \$q21)&
(\$z4 iff \$q22)&
(\$z5 iff \$c22)
implies
(\$z0 iff \$MULT310(x2, x1,y1,x0,y0))&
(\$z1 iff \$MULT311(x2, x1,y1,x0,y0))&
(\$z2 iff \$MULT321(x2,y2,x1,y1,x0,y0))&
(\$z3 iff \$MULT322(x2,y2,x1,y1,x0,y0))&
(\$z4 iff \$MULT323(x2,y2,x1,y1,x0,y0))&
(\$z5 iff \$MULT324(x2,y2,x1,y1,x0,y0));

begin :: Logical Equivalence of Wallace tree Multiplier.

::
:: Logical Equivalence of 3-by-3 bit Wallace tree Multiplier.
::

::The following theorem shows that
:: outputs of '3-by-3 bit Wallace tree Multiplier' are equivalent to
:: outputs of '3-by-3 normal (sequencial) Multiplier'
:: We assume that there is no feedback loop in multiplier.

theorem :: GATE_5:3 ::3WTM:
for x0,x1,x2,y0,y1,y2,z0,z1,z2,z3,z4,z5,
q00,q01,q02,q03,c01,c02,c03,q11,q12,q13,c11,c12,c13 being set holds
(\$q00 iff \$AND2(x0,y0))&
(\$q01 iff \$XOR3(AND2(x1,y0),AND2(x0,y1),{}))&
(\$c01 iff \$MAJ3(AND2(x1,y0),AND2(x0,y1),{}))&
(\$q02 iff \$XOR3(AND2(x2,y0),AND2(x1,y1),AND2(x0,y2)))&
(\$c02 iff \$MAJ3(AND2(x2,y0),AND2(x1,y1),AND2(x0,y2)))&
(\$q03 iff \$XOR3(AND2(x2,y1),AND2(x1,y2),{}))&
(\$c03 iff \$MAJ3(AND2(x2,y1),AND2(x1,y2),{}))&
(\$q11 iff \$XOR3(q02 ,c01 ,{}))&
(\$c11 iff \$MAJ3(q02 ,c01 ,{}))&
(\$q12 iff \$XOR3(q03 ,c02 ,c11))&
(\$c12 iff \$MAJ3(q03 ,c02 ,c11))&
(\$q13 iff \$XOR3(AND2(x2,y2),c03 ,c12))&
(\$c13 iff \$MAJ3(AND2(x2,y2),c03 ,c12))&
(\$z0 iff \$q00)&
(\$z1 iff \$q01)&
(\$z2 iff \$q11)&
(\$z3 iff \$q12)&
(\$z4 iff \$q13)&
(\$z5 iff \$c13)
implies
(\$z0 iff \$MULT310(x2, x1,y1,x0,y0))&
(\$z1 iff \$MULT311(x2, x1,y1,x0,y0))&
(\$z2 iff \$MULT321(x2,y2,x1,y1,x0,y0))&
(\$z3 iff \$MULT322(x2,y2,x1,y1,x0,y0))&
(\$z4 iff \$MULT323(x2,y2,x1,y1,x0,y0))&
(\$z5 iff \$MULT324(x2,y2,x1,y1,x0,y0));

::
:: (This eqivalency has been checked out by the theorem GATE_1:44.)
::

::The following two definitions are for CLA 1 bit adder.
definition let a1,b1,c be set;
redefine func XOR3(a1,b1,c);

redefine func MAJ3(a1,b1,c);
synonym CLACARR1(a1,b1,c);
end;

::The following two definitions are for CLA 2 bit adder.
definition let a1,b1,a2,b2,c be set;
canceled 2;

:: GATE_5:def 16
XOR3(a2,b2,MAJ3(a1,b1,c));

func CLACARR2(a2,b2,a1,b1,c) -> set equals
:: GATE_5:def 17
OR2(AND2(a2,b2),AND2(OR2(a2,b2),MAJ3(a1,b1,c)));
end;

::The following two definitions are for CLA 3 bit adder.
definition let a1,b1,a2,b2,a3,b3,c be set;
:: GATE_5:def 18
XOR3(a3,b3,CLACARR2(a2,b2,a1,b1,c));

func CLACARR3(a3,b3,a2,b2,a1,b1,c) -> set equals
:: GATE_5:def 19
OR3(AND2(a3,b3),AND2(OR2(a3,b3),AND2(a2,b2)),
AND3(OR2(a3,b3),OR2(a2,b2),MAJ3(a1,b1,c)));
end;

::The following two definitions are for CLA 4 bit adder.
definition let a1,b1,a2,b2,a3,b3,a4,b4,c be set;
:: GATE_5:def 20
XOR3(a4,b4,CLACARR3(a3,b3,a2,b2,a1,b1,c));

func CLACARR4(a4,b4,a3,b3,a2,b2,a1,b1,c) -> set equals
:: GATE_5:def 21
OR4(AND2(a4,b4),AND2(OR2(a4,b4),AND2(a3,b3)),
AND3(OR2(a4,b4),OR2(a3,b3),AND2(a2,b2)),
AND4(OR2(a4,b4),OR2(a3,b3),OR2(a2,b2),MAJ3(a1,b1,c)));
end;

::The following theorem shows that
:: outputs of '3-by-3 bit Wallace tree Multiplier' by using Carry Look-up
:: Multiplier'.
:: We assume that there is no feedback loop in multiplier.

theorem :: GATE_5:4 ::3WTMCLA:
for x0,x1,x2,y0,y1,y2,z0,z1,z2,z3,z4,z5,
q00,q01,q02,q03,c01,c02,c03 being set holds
(\$q00 iff \$AND2(x0,y0))&
(\$q01 iff \$XOR3(AND2(x1,y0),AND2(x0,y1),{}))&
(\$c01 iff \$MAJ3(AND2(x1,y0),AND2(x0,y1),{}))&
(\$q02 iff \$XOR3(AND2(x2,y0),AND2(x1,y1),AND2(x0,y2)))&
(\$c02 iff \$MAJ3(AND2(x2,y0),AND2(x1,y1),AND2(x0,y2)))&
(\$q03 iff \$XOR3(AND2(x2,y1),AND2(x1,y2),{}))&
(\$c03 iff \$MAJ3(AND2(x2,y1),AND2(x1,y2),{}))&
(\$z0 iff \$q00)&
(\$z1 iff \$q01)&