:: Correctness of the High Speed Array Multiplier Circuits
:: by Hiroshi Yamazaki and Katsumi Wasaki
::
:: Received August 28, 2000
:: Copyright (c) 2000-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies GATE_1, XBOOLE_0, GATE_5;
notations XBOOLE_0, GATE_1;
constructors XBOOLE_0, GATE_1;
registrations XBOOLE_0, GATE_1;
theorems GATE_1;
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
AND2(x0,y0);
correctness;
func MULT211(x1,y1,x0,y0) -> set equals
ADD1(AND2(x1,y0),AND2(x0,y1),{});
correctness;
func MULT212(x1,y1,x0,y0) -> set equals
ADD2({},AND2(x1,y1),AND2(x1,y0),AND2
(x0,y1),{});
correctness;
func MULT213(x1,y1,x0,y0) -> set equals
CARR2({},AND2(x1,y1),AND2(x1,y0),
AND2(x0,y1),{});
correctness;
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
for x0,x1,y0,y1,z0,z1,z2,z3,q00,q01,c01,q11,c11 being set holds (q00
is not empty iff AND2(x0,y0) is not empty)& (q01 is not empty iff XOR3(AND2(x1,
y0),AND2(x0,y1),{} ) is not empty)& (c01 is not empty iff MAJ3(AND2(x1,y0),AND2
(x0,y1),{} ) is not empty)& (q11 is not empty iff XOR3(AND2(x1,y1),{} ,c01) is
not empty)& (c11 is not empty iff MAJ3(AND2(x1,y1),{} ,c01) is not empty)& (z0
is not empty iff q00 is not empty)& (z1 is not empty iff q01 is not empty)& (z2
is not empty iff q11 is not empty)& (z3 is not empty iff c11 is not empty)
implies (z0 is not empty iff MULT210(x1,y1,x0,y0) is not empty)& (z1 is not
empty iff MULT211(x1,y1,x0,y0) is not empty)& (z2 is not empty iff MULT212(x1,
y1,x0,y0) is not empty)& (z3 is not empty iff MULT213(x1,y1,x0,y0) is not empty
)
proof
let x0,x1,y0,y1,z0,z1,z2,z3,q00,q01,c01,q11,c11 be set;
assume that
A1: q00 is not empty iff AND2(x0,y0) is not empty and
A2: q01 is not empty iff XOR3(AND2(x1,y0),AND2(x0,y1),{} ) is not empty and
A3: c01 is not empty iff MAJ3(AND2(x1,y0),AND2(x0,y1),{} ) is not empty and
A4: q11 is not empty iff XOR3(AND2(x1,y1),{} ,c01) is not empty and
A5: c11 is not empty iff MAJ3(AND2(x1,y1),{} ,c01) is not empty and
A6: z0 is not empty iff q00 is not empty and
A7: z1 is not empty iff q01 is not empty and
A8: z2 is not empty iff q11 is not empty and
A9: z3 is not empty iff c11 is not empty;
thus z0 is not empty iff MULT210(x1,y1,x0,y0) is not empty by A1,A6;
thus z1 is not empty iff MULT211(x1,y1,x0,y0) is not empty by A2,A7;
set m212 = MULT212(x1,y1,x0,y0);
set x1y1 = AND2(x1,y1);
set x0y1 = AND2(x0,y1);
set x1y0 = AND2(x1,y0);
m212 = XOR3({},x1y1,MAJ3(x1y0,x0y1,{})) by GATE_1:def 35;
then
m212 is not empty iff x1y1 is not empty & not MAJ3(x1y0,x0y1,{}) is not
empty or not x1y1 is not empty & MAJ3(x1y0,x0y1,{}) is not empty;
hence z2 is not empty iff MULT212(x1,y1,x0,y0) is not empty by A3,A4,A8;
set m213 = MULT213(x1,y1,x0,y0);
m213 = MAJ3({},x1y1,MAJ3(x1y0,x0y1,{})) by GATE_1:def 36;
then m213 is not empty iff x1y1 is not empty & MAJ3(x1y0,x0y1,{}) is not
empty;
hence thesis by A3,A5,A9;
end;
::
:: 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
AND2(x0,y0);
correctness;
func MULT311(x2,x1,y1,x0,y0) -> set equals
ADD1(AND2(x1,y0),AND2(x0,y1),{});
correctness;
func MULT312(x2,x1,y1,x0,y0) -> set equals
ADD2(AND2(x2,y0),AND2(x1,y1),
AND2(x1,y0),AND2(x0,y1),{});
correctness;
func MULT313(x2,x1,y1,x0,y0) -> set equals
ADD3({} ,AND2(x2,y1), AND2(x2,y0)
,AND2(x1,y1), AND2(x1,y0),AND2(x0,y1),{});
correctness;
func MULT314(x2,x1,y1,x0,y0) -> set equals
CARR3({} ,AND2(x2,y1), AND2(x2,y0
),AND2(x1,y1), AND2(x1,y0),AND2(x0,y1),{});
correctness;
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
ADD1(MULT312(x2,x1,y1,x0,y0),
AND2(x0,y2),{});
correctness;
func MULT322(x2,y2,x1,y1,x0,y0) -> set equals
ADD2(MULT313(x2,x1,y1,x0,y0),
AND2(x1,y2), MULT312(x2,x1,y1,x0,y0),AND2(x0,y2),{});
correctness;
func MULT323(x2,y2,x1,y1,x0,y0) -> set equals
ADD3(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),{});
correctness;
func MULT324(x2,y2,x1,y1,x0,y0) -> set equals
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),{});
correctness;
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 ::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 is not empty iff AND2(x0,y0) is
not empty)& (q01 is not empty iff XOR3(AND2(x1,y0),AND2(x0,y1),{} ) is not
empty)& (c01 is not empty iff MAJ3(AND2(x1,y0),AND2(x0,y1),{} ) is not empty)&
(q02 is not empty iff XOR3(AND2(x2,y0),AND2(x1,y1),{} ) is not empty)& (c02 is
not empty iff MAJ3(AND2(x2,y0),AND2(x1,y1),{} ) is not empty)& (q11 is not
empty iff XOR3(q02,AND2(x0,y2),c01) is not empty)& (c11 is not empty iff MAJ3(
q02,AND2(x0,y2),c01) is not empty)& (q12 is not empty iff XOR3(AND2(x2,y1),AND2
(x1,y2),c02) is not empty)& (c12 is not empty iff MAJ3(AND2(x2,y1),AND2(x1,y2),
c02) is not empty)& (q21 is not empty iff XOR3(q12,{} ,c11) is not empty)& (c21
is not empty iff MAJ3(q12,{} ,c11) is not empty)& (q22 is not empty iff XOR3(
AND2(x2,y2),c21,c12) is not empty)& (c22 is not empty iff MAJ3(AND2(x2,y2),c21,
c12) is not empty)& (z0 is not empty iff q00 is not empty)& (z1 is not empty
iff q01 is not empty)& (z2 is not empty iff q11 is not empty)& (z3 is not empty
iff q21 is not empty)& (z4 is not empty iff q22 is not empty)& (z5 is not empty
iff c22 is not empty) implies (z0 is not empty iff MULT310(x2, x1,y1,x0,y0) is
not empty)& (z1 is not empty iff MULT311(x2, x1,y1,x0,y0) is not empty)& (z2 is
not empty iff MULT321(x2,y2,x1,y1,x0,y0) is not empty)& (z3 is not empty iff
MULT322(x2,y2,x1,y1,x0,y0) is not empty)& (z4 is not empty iff MULT323(x2,y2,x1
,y1,x0,y0) is not empty)& (z5 is not empty iff MULT324(x2,y2,x1,y1,x0,y0) is
not empty)
proof
let 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 be set;
assume that
A1: q00 is not empty iff AND2(x0,y0) is not empty and
A2: q01 is not empty iff XOR3(AND2(x1,y0),AND2(x0,y1),{} ) is not empty and
A3: ( c01 is not empty iff MAJ3(AND2(x1,y0),AND2(x0,y1),{} ) is not
empty)&( q02 is not empty iff XOR3(AND2(x2,y0),AND2(x1,y1),{} ) is not empty)
and
A4: c02 is not empty iff MAJ3(AND2(x2,y0),AND2(x1,y1),{} ) is not empty and
A5: q11 is not empty iff XOR3(q02,AND2(x0,y2),c01) is not empty and
A6: c11 is not empty iff MAJ3(q02,AND2(x0,y2),c01) is not empty and
A7: q12 is not empty iff XOR3(AND2(x2,y1),AND2(x1,y2),c02) is not empty and
A8: c12 is not empty iff MAJ3(AND2(x2,y1),AND2(x1,y2),c02) is not empty and
A9: q21 is not empty iff XOR3(q12,{} ,c11) is not empty and
A10: c21 is not empty iff MAJ3(q12,{} ,c11) is not empty and
A11: q22 is not empty iff XOR3(AND2(x2,y2),c21,c12) is not empty and
A12: c22 is not empty iff MAJ3(AND2(x2,y2),c21,c12) is not empty and
A13: z0 is not empty iff q00 is not empty and
A14: z1 is not empty iff q01 is not empty and
A15: z2 is not empty iff q11 is not empty and
A16: z3 is not empty iff q21 is not empty and
A17: z4 is not empty iff q22 is not empty and
A18: z5 is not empty iff c22 is not empty;
set x0y2 = AND2(x0,y2);
A19: c11 is not empty iff q02 is not empty & x0y2 is not empty or x0y2 is
not empty & c01 is not empty or c01 is not empty & q02 is not empty by A6;
thus z0 is not empty iff MULT310(x2,x1,y1,x0,y0) is not empty by A1,A13;
thus z1 is not empty iff MULT311(x2,x1,y1,x0,y0) is not empty by A2,A14;
set m312 = MULT312(x2,x1,y1,x0,y0);
set x1y1 = AND2(x1,y1);
set x0y1 = AND2(x0,y1);
set x2y0 = AND2(x2,y0);
set x1y0 = AND2(x1,y0);
A20: m312 = XOR3(x2y0,x1y1,MAJ3(x1y0,x0y1,{})) by GATE_1:def 35;
then
A21: m312 is not empty iff ( x2y0 is not empty & not x1y1 is not empty or
not x2y0 is not empty & x1y1 is not empty ) & not MAJ3(x1y0,x0y1,{}) is not
empty or not ( x2y0 is not empty & not x1y1 is not empty or not x2y0 is not
empty & x1y1 is not empty ) & MAJ3(x1y0,x0y1,{}) is not empty;
A22: m312 is not empty iff ( x2y0 is not empty & not x1y1 is not empty or
not x2y0 is not empty & x1y1 is not empty ) & not (x1y0 is not empty & x0y1 is
not empty) or not ( x2y0 is not empty & not x1y1 is not empty or not x2y0 is
not empty & x1y1 is not empty ) & x1y0 is not empty & x0y1 is not empty by A20;
q11 is not empty iff ( q02 is not empty & not x0y2 is not empty or not
q02 is not empty & x0y2 is not empty ) & not c01 is not empty or not ( q02 is
not empty & not x0y2 is not empty or not q02 is not empty & x0y2 is not empty )
& c01 is not empty by A5;
hence z2 is not empty iff MULT321(x2,y2,x1,y1,x0,y0) is not empty by A3,A15
,A21;
set x1y2 = AND2(x1,y2);
set x2y1 = AND2(x2,y1);
A23: q12 is not empty iff ( x2y1 is not empty & not x1y2 is not empty or not
x2y1 is not empty & x1y2 is not empty ) & not c02 is not empty or not ( x2y1 is
not empty & not x1y2 is not empty or not x2y1 is not empty & x1y2 is not empty
) & c02 is not empty by A7;
set m324 = MULT324(x2,y2,x1,y1,x0,y0);
set m323 = MULT323(x2,y2,x1,y1,x0,y0);
set m314 = MULT314(x2,x1,y1,x0,y0);
set x2y2 = AND2(x2,y2);
A24: m314 = MAJ3({},x2y1,CARR2(x2y0,x1y1,x1y0,x0y1,{})) by GATE_1:def 38
.= MAJ3({},x2y1,MAJ3(x2y0,x1y1,MAJ3(x1y0,x0y1,{}))) by GATE_1:def 36;
set m322 = MULT322(x2,y2,x1,y1,x0,y0);
set m313 = MULT313(x2,x1,y1,x0,y0);
A25: m313 = XOR3({},x2y1,CARR2(x2y0,x1y1,x1y0,x0y1,{})) by GATE_1:def 37
.= XOR3({},x2y1,MAJ3(x2y0,x1y1,MAJ3(x1y0,x0y1,{}))) by GATE_1:def 36;
m322 = XOR3(m313,x1y2,MAJ3(m312,x0y2,{})) by GATE_1:def 35;
hence z3 is not empty iff MULT322(x2,y2,x1,y1,x0,y0) is not empty by A3,A4,A9
,A16,A19,A23,A22,A25;
A26: m323 = XOR3(m314,x2y2,CARR2(m313,x1y2,m312,x0y2,{})) by GATE_1:def 37
.= XOR3(m314,x2y2,MAJ3(m313,x1y2,MAJ3(m312,x0y2,{}))) by GATE_1:def 36;
q22 is not empty iff ( x2y2 is not empty & not c21 is not empty or not
x2y2 is not empty & c21 is not empty ) & not c12 is not empty or not ( x2y2 is
not empty & not c21 is not empty or not x2y2 is not empty & c21 is not empty )
& c12 is not empty by A11;
hence
z4 is not empty iff MULT323(x2,y2,x1,y1,x0,y0) is not empty by A3,A4,A8,A10
,A17,A19,A23,A22,A25,A24,A26;
A27: m324 = MAJ3(m314,x2y2,CARR2(m313,x1y2,m312,x0y2,{})) by GATE_1:def 38
.= MAJ3(m314,x2y2,MAJ3(m313,x1y2,MAJ3(m312,x0y2,{}))) by GATE_1:def 36;
c22 is not empty iff x2y2 is not empty & c21 is not empty or c21 is not
empty & c12 is not empty or c12 is not empty & x2y2 is not empty by A12;
hence thesis by A3,A4,A8,A10,A18,A19,A23,A22,A25,A24,A27;
end;
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
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 is not empty iff AND2(x0,y0) is
not empty)& (q01 is not empty iff XOR3(AND2(x1,y0),AND2(x0,y1),{}) is not empty
)& (c01 is not empty iff MAJ3(AND2(x1,y0),AND2(x0,y1),{}) is not empty)& (q02
is not empty iff XOR3(AND2(x2,y0),AND2(x1,y1),AND2(x0,y2)) is not empty)& (c02
is not empty iff MAJ3(AND2(x2,y0),AND2(x1,y1),AND2(x0,y2)) is not empty)& (q03
is not empty iff XOR3(AND2(x2,y1),AND2(x1,y2),{}) is not empty)& (c03 is not
empty iff MAJ3(AND2(x2,y1),AND2(x1,y2),{}) is not empty)& (q11 is not empty iff
XOR3(q02,c01,{}) is not empty)& (c11 is not empty iff MAJ3(q02,c01,{}) is not
empty)& (q12 is not empty iff XOR3(q03,c02,c11) is not empty)& (c12 is not
empty iff MAJ3(q03,c02,c11) is not empty)& (q13 is not empty iff XOR3(AND2(x2,
y2),c03,c12) is not empty)& (c13 is not empty iff MAJ3(AND2(x2,y2),c03,c12) is
not empty)& (z0 is not empty iff q00 is not empty)& (z1 is not empty iff q01 is
not empty)& (z2 is not empty iff q11 is not empty)& (z3 is not empty iff q12 is
not empty)& (z4 is not empty iff q13 is not empty)& (z5 is not empty iff c13 is
not empty) implies (z0 is not empty iff MULT310(x2, x1,y1,x0,y0) is not empty)&
(z1 is not empty iff MULT311(x2, x1,y1,x0,y0) is not empty)& (z2 is not empty
iff MULT321(x2,y2,x1,y1,x0,y0) is not empty)& (z3 is not empty iff MULT322(x2,
y2,x1,y1,x0,y0) is not empty)& (z4 is not empty iff MULT323(x2,y2,x1,y1,x0,y0)
is not empty)& (z5 is not empty iff MULT324(x2,y2,x1,y1,x0,y0) is not empty)
proof
let 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 be set;
assume that
A1: q00 is not empty iff AND2(x0,y0) is not empty and
A2: q01 is not empty iff XOR3(AND2(x1,y0),AND2(x0,y1),{}) is not empty and
A3: c01 is not empty iff MAJ3(AND2(x1,y0),AND2(x0,y1),{}) is not empty and
A4: q02 is not empty iff XOR3(AND2(x2,y0),AND2(x1,y1),AND2(x0,y2)) is
not empty and
A5: c02 is not empty iff MAJ3(AND2(x2,y0),AND2(x1,y1),AND2(x0,y2)) is
not empty and
A6: q03 is not empty iff XOR3(AND2(x2,y1),AND2(x1,y2),{}) is not empty and
A7: c03 is not empty iff MAJ3(AND2(x2,y1),AND2(x1,y2),{}) is not empty and
A8: q11 is not empty iff XOR3(q02,c01,{}) is not empty and
A9: c11 is not empty iff MAJ3(q02,c01,{}) is not empty and
A10: q12 is not empty iff XOR3(q03,c02,c11) is not empty and
A11: c12 is not empty iff MAJ3(q03,c02,c11) is not empty and
A12: q13 is not empty iff XOR3(AND2(x2,y2),c03,c12) is not empty and
A13: c13 is not empty iff MAJ3(AND2(x2,y2),c03,c12) is not empty and
A14: z0 is not empty iff q00 is not empty and
A15: z1 is not empty iff q01 is not empty and
A16: z2 is not empty iff q11 is not empty and
A17: z3 is not empty iff q12 is not empty and
A18: z4 is not empty iff q13 is not empty and
A19: z5 is not empty iff c13 is not empty;
thus z0 is not empty iff MULT310(x2,x1,y1,x0,y0) is not empty by A1,A14;
thus z1 is not empty iff MULT311(x2,x1,y1,x0,y0) is not empty by A2,A15;
set m312 = MULT312(x2,x1,y1,x0,y0);
set x0y2 = AND2(x0,y2);
set x1y1 = AND2(x1,y1);
set x0y1 = AND2(x0,y1);
set x2y0 = AND2(x2,y0);
set x1y0 = AND2(x1,y0);
A20: m312 = XOR3(x2y0,x1y1,MAJ3(x1y0,x0y1,{})) by GATE_1:def 35;
set m323 = MULT323(x2,y2,x1,y1,x0,y0);
set m314 = MULT314(x2,x1,y1,x0,y0);
set x2y2 = AND2(x2,y2);
set m322 = MULT322(x2,y2,x1,y1,x0,y0);
set m313 = MULT313(x2,x1,y1,x0,y0);
set x1y2 = AND2(x1,y2);
set x2y1 = AND2(x2,y1);
A21: q03 is not empty iff x2y1 is not empty & not x1y2 is not empty or not
x2y1 is not empty & x1y2 is not empty by A6;
A22: q02 is not empty iff ( x2y0 is not empty & not x1y1 is not empty or not
x2y0 is not empty & x1y1 is not empty ) & not x0y2 is not empty or not ( x2y0
is not empty & not x1y1 is not empty or not x2y0 is not empty & x1y1 is not
empty ) & x0y2 is not empty by A4;
hence z2 is not empty iff MULT321(x2,y2,x1,y1,x0,y0) is not empty by A3,A8
,A16,A20;
A23: m313 = XOR3({},x2y1,CARR2(x2y0,x1y1,x1y0,x0y1,{})) by GATE_1:def 37
.= XOR3({},x2y1,MAJ3(x2y0,x1y1,MAJ3(x1y0,x0y1,{}))) by GATE_1:def 36;
m322 = XOR3(m313,x1y2,MAJ3(m312,x0y2,{})) by GATE_1:def 35;
hence
z3 is not empty iff MULT322(x2,y2,x1,y1,x0,y0) is not empty by A3,A5,A9,A10
,A17,A22,A21,A20,A23;
A24: m314 = MAJ3({},x2y1,CARR2(x2y0,x1y1,x1y0,x0y1,{})) by GATE_1:def 38
.= MAJ3({},x2y1,MAJ3(x2y0,x1y1,MAJ3(x1y0,x0y1,{}))) by GATE_1:def 36;
set m324 = MULT324(x2,y2,x1,y1,x0,y0);
A25: m324 = MAJ3(m314,x2y2,CARR2(m313,x1y2,m312,x0y2,{})) by GATE_1:def 38
.= MAJ3(m314,x2y2,MAJ3(m313,x1y2,MAJ3(m312,x0y2,{}))) by GATE_1:def 36;
A26: m323 = XOR3(m314,x2y2,CARR2(m313,x1y2,m312,x0y2,{})) by GATE_1:def 37
.= XOR3(m314,x2y2,MAJ3(m313,x1y2,MAJ3(m312,x0y2,{}))) by GATE_1:def 36;
q13 is not empty iff ( x2y2 is not empty & not c03 is not empty or not
x2y2 is not empty & c03 is not empty ) & not c12 is not empty or not ( x2y2 is
not empty & not c03 is not empty or not x2y2 is not empty & c03 is not empty )
& c12 is not empty by A12;
hence
z4 is not empty iff MULT323(x2,y2,x1,y1,x0,y0) is not empty by A3,A5,A7,A9
,A11,A18,A22,A21,A20,A23,A24,A26;
c13 is not empty iff x2y2 is not empty & c03 is not empty or c03 is not
empty & c12 is not empty or c12 is not empty & x2y2 is not empty by A13;
hence thesis by A3,A5,A7,A9,A11,A19,A22,A21,A20,A23,A24,A25;
end;
::
:: Carry Look-up Ahead (CLA) Adder
:: (This eqivalency has been checked out by the theorem GATE_1:44.)
::
::The following two definitions are for CLA 1 bit adder.
notation
let a1,b1,c be set;
synonym CLAADD1(a1,b1,c) for XOR3(a1,b1,c);
synonym CLACARR1(a1,b1,c) for MAJ3(a1,b1,c);
end;
::The following two definitions are for CLA 2 bit adder.
definition
let a1,b1,a2,b2,c be set;
func CLAADD2(a2,b2,a1,b1,c) -> set equals
XOR3(a2,b2,MAJ3(a1,b1,c));
correctness;
func CLACARR2(a2,b2,a1,b1,c) -> set equals
OR2(AND2(a2,b2),AND2(OR2(a2,b2),
MAJ3(a1,b1,c)));
correctness;
end;
::The following two definitions are for CLA 3 bit adder.
definition
let a1,b1,a2,b2,a3,b3,c be set;
func CLAADD3(a3,b3,a2,b2,a1,b1,c) -> set equals
XOR3(a3,b3,CLACARR2(a2,b2,a1
,b1,c));
correctness;
func CLACARR3(a3,b3,a2,b2,a1,b1,c) -> set equals
OR3(AND2(a3,b3),AND2(OR2(a3
,b3),AND2(a2,b2)), AND3(OR2(a3,b3),OR2(a2,b2),MAJ3(a1,b1,c)));
correctness;
end;
::The following two definitions are for CLA 4 bit adder.
definition
let a1,b1,a2,b2,a3,b3,a4,b4,c be set;
func CLAADD4(a4,b4,a3,b3,a2,b2,a1,b1,c) -> set equals
XOR3(a4,b4,CLACARR3(a3
,b3,a2,b2,a1,b1,c));
correctness;
func CLACARR4(a4,b4,a3,b3,a2,b2,a1,b1,c) -> set equals
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)));
correctness;
end;
::The following theorem shows that
:: outputs of '3-by-3 bit Wallace tree Multiplier' by using Carry Look-up
:: Ahead Adder are equivalent to outputs of '3-by-3 normal (sequencial)
:: Multiplier'.
:: We assume that there is no feedback loop in multiplier.
theorem ::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 is not empty iff AND2(x0,y0) is not empty)& (q01 is not
empty iff XOR3(AND2(x1,y0),AND2(x0,y1),{}) is not empty)& (c01 is not empty iff
MAJ3(AND2(x1,y0),AND2(x0,y1),{}) is not empty)& (q02 is not empty iff XOR3(AND2
(x2,y0),AND2(x1,y1),AND2(x0,y2)) is not empty)& (c02 is not empty iff MAJ3(AND2
(x2,y0),AND2(x1,y1),AND2(x0,y2)) is not empty)& (q03 is not empty iff XOR3(AND2
(x2,y1),AND2(x1,y2),{}) is not empty)& (c03 is not empty iff MAJ3(AND2(x2,y1),
AND2(x1,y2),{}) is not empty)& (z0 is not empty iff q00 is not empty)& (z1 is
not empty iff q01 is not empty)& (z2 is not empty iff CLAADD1( q02,c01,{}) is
not empty)& (z3 is not empty iff CLAADD2( q03,c02,q02,c01,{}) is not empty)& (
z4 is not empty iff CLAADD3(AND2(x2,y2),c03,q03,c02,q02,c01,{}) is not empty)&
(z5 is not empty iff CLACARR3(AND2(x2,y2),c03,q03,c02,q02,c01,{}) is not empty)
implies (z0 is not empty iff MULT310(x2, x1,y1,x0,y0) is not empty)& (z1 is not
empty iff MULT311(x2, x1,y1,x0,y0) is not empty)& (z2 is not empty iff MULT321(
x2,y2,x1,y1,x0,y0) is not empty)& (z3 is not empty iff MULT322(x2,y2,x1,y1,x0,
y0) is not empty)& (z4 is not empty iff MULT323(x2,y2,x1,y1,x0,y0) is not empty
)& (z5 is not empty iff MULT324(x2,y2,x1,y1,x0,y0) is not empty)
proof
let x0,x1,x2,y0,y1,y2,z0,z1,z2,z3,z4,z5, q00,q01,q02,q03,c01,c02,c03 be set;
assume that
A1: q00 is not empty iff AND2(x0,y0) is not empty and
A2: q01 is not empty iff XOR3(AND2(x1,y0),AND2(x0,y1),{}) is not empty and
A3: c01 is not empty iff MAJ3(AND2(x1,y0),AND2(x0,y1),{}) is not empty and
A4: q02 is not empty iff XOR3(AND2(x2,y0),AND2(x1,y1),AND2(x0,y2)) is
not empty and
A5: c02 is not empty iff MAJ3(AND2(x2,y0),AND2(x1,y1),AND2(x0,y2)) is
not empty and
A6: q03 is not empty iff XOR3(AND2(x2,y1),AND2(x1,y2),{}) is not empty and
A7: c03 is not empty iff MAJ3(AND2(x2,y1),AND2(x1,y2),{}) is not empty and
A8: z0 is not empty iff q00 is not empty and
A9: z1 is not empty iff q01 is not empty and
A10: z2 is not empty iff CLAADD1( q02,c01,{}) is not empty and
A11: z3 is not empty iff CLAADD2( q03,c02,q02,c01,{}) is not empty and
A12: z4 is not empty iff CLAADD3(AND2(x2,y2),c03,q03,c02,q02,c01,{}) is
not empty and
A13: z5 is not empty iff CLACARR3(AND2(x2,y2),c03,q03,c02,q02,c01,{}) is
not empty;
set x0y2 = AND2(x0,y2);
set x1y1 = AND2(x1,y1);
set x2y0 = AND2(x2,y0);
thus z0 is not empty iff MULT310(x2,x1,y1,x0,y0) is not empty by A1,A8;
thus z1 is not empty iff MULT311(x2,x1,y1,x0,y0) is not empty by A2,A9;
set m312 = MULT312(x2,x1,y1,x0,y0);
set x0y1 = AND2(x0,y1);
set x1y0 = AND2(x1,y0);
A14: m312 = XOR3(x2y0,x1y1,MAJ3(x1y0,x0y1,{})) by GATE_1:def 35;
then
A15: m312 is not empty iff ( x2y0 is not empty & not x1y1 is not empty or
not x2y0 is not empty & x1y1 is not empty ) & not (x1y0 is not empty & x0y1 is
not empty) or not ( x2y0 is not empty & not x1y1 is not empty or not x2y0 is
not empty & x1y1 is not empty ) & x1y0 is not empty & x0y1 is not empty;
set x1y2 = AND2(x1,y2);
set x2y1 = AND2(x2,y1);
A16: q03 is not empty iff x2y1 is not empty & not x1y2 is not empty or not
x2y1 is not empty & x1y2 is not empty by A6;
set m324 = MULT324(x2,y2,x1,y1,x0,y0);
set m323 = MULT323(x2,y2,x1,y1,x0,y0);
set m314 = MULT314(x2,x1,y1,x0,y0);
set x2y2 = AND2(x2,y2);
A17: m314 = MAJ3({},x2y1,CARR2(x2y0,x1y1,x1y0,x0y1,{})) by GATE_1:def 38
.= MAJ3({},x2y1,MAJ3(x2y0,x1y1,MAJ3(x1y0,x0y1,{}))) by GATE_1:def 36;
set m322 = MULT322(x2,y2,x1,y1,x0,y0);
set m313 = MULT313(x2,x1,y1,x0,y0);
A18: m313 = XOR3({},x2y1,CARR2(x2y0,x1y1,x1y0,x0y1,{})) by GATE_1:def 37
.= XOR3({},x2y1,MAJ3(x2y0,x1y1,MAJ3(x1y0,x0y1,{}))) by GATE_1:def 36;
q02 is not empty iff ( x2y0 is not empty & not x1y1 is not empty or not
x2y0 is not empty & x1y1 is not empty ) & not x0y2 is not empty or not ( x2y0
is not empty & not x1y1 is not empty or not x2y0 is not empty & x1y1 is not
empty ) & x0y2 is not empty by A4;
hence z2 is not empty iff MULT321(x2,y2,x1,y1,x0,y0) is not empty by A3,A10
,A14;
A19: c02 is not empty iff x2y0 is not empty & x1y1 is not empty or x1y1 is
not empty & x0y2 is not empty or x0y2 is not empty & x2y0 is not empty by A5;
m322 = XOR3(m313,x1y2,MAJ3(m312,x0y2,{})) by GATE_1:def 35;
then m322 is not empty iff ( m313 is not empty & not x1y2 is not empty or
not m313 is not empty & x1y2 is not empty ) & not (m312 is not empty & x0y2 is
not empty) or not ( m313 is not empty & not x1y2 is not empty or not m313 is
not empty & x1y2 is not empty ) & m312 is not empty & x0y2 is not empty;
hence z3 is not empty iff MULT322(x2,y2,x1,y1,x0,y0) is not empty by A3,A4
,A11,A19,A16,A15,A18;
m323 = XOR3(m314,x2y2,CARR2(m313,x1y2,m312,x0y2,{})) by GATE_1:def 37
.= XOR3(m314,x2y2,MAJ3(m313,x1y2,MAJ3(m312,x0y2,{}))) by GATE_1:def 36;
then m323 is not empty iff ( m314 is not empty & not x2y2 is not empty or
not m314 is not empty & x2y2 is not empty ) & not ( m313 is not empty & x1y2 is
not empty or x1y2 is not empty & m312 is not empty & x0y2 is not empty or m312
is not empty & x0y2 is not empty & m313 is not empty ) or not ( m314 is not
empty & not x2y2 is not empty or not m314 is not empty & x2y2 is not empty ) &
( m313 is not empty & x1y2 is not empty or x1y2 is not empty & m312 is not
empty & x0y2 is not empty or m312 is not empty & x0y2 is not empty & m313 is
not empty );
hence
z4 is not empty iff MULT323(x2,y2,x1,y1,x0,y0) is not empty by A3,A4,A7,A12
,A19,A16,A15,A18,A17;
m324 = MAJ3(m314,x2y2,CARR2(m313,x1y2,m312,x0y2,{})) by GATE_1:def 38
.= MAJ3(m314,x2y2,MAJ3(m313,x1y2,MAJ3(m312,x0y2,{}))) by GATE_1:def 36;
then m324 is not empty iff m314 is not empty & x2y2 is not empty or x2y2 is
not empty & ( m313 is not empty & x1y2 is not empty or x1y2 is not empty & m312
is not empty & x0y2 is not empty or m312 is not empty & x0y2 is not empty &
m313 is not empty ) or ( m313 is not empty & x1y2 is not empty or x1y2 is not
empty & m312 is not empty & x0y2 is not empty or m312 is not empty & x0y2 is
not empty & m313 is not empty ) & m314 is not empty;
hence thesis by A3,A4,A7,A13,A19,A16,A15,A18,A17;
end;