Volume 15, 2003

University of Bialystok

Copyright (c) 2003 Association of Mizar Users

**Masaaki Niimura**- Shinshu University, Nagano
**Yasushi Fuwa**- Shinshu University, Nagano

- In this article, a new adder algorithm using Radix-$2^k$ sub signed-digit numbers is defined and properties for the hardware-realization is discussed.\par Until now, we proposed Radix-$2^k$ sub signed-digit numbers in consideration of the hardware realization. In this article, we proposed High Speed Adder Algorithm using this Radix-$2^k$ sub signed-digit numbers. This method has two ways to speed up at hardware-realization. One is 'bit compare' at carry calculation, it is proposed in another article. Other is carry calculation between two numbers. We proposed that $n$ digits Radix-$2^k$ signed-digit numbers is expressed in $n+1$ digits Radix-$2^k$ sub signed-digit numbers, and addition result of two $n+1$ digits Radix-$2^k$ sub signed-digit numbers is expressed in $n+1$ digits. In this way, carry operation between two Radix-$2^k$ sub signed-digit numbers can be processed at $n+1$ digit adder circuit and additional circuit to operate carry is not needed.\par In the first section of this article, we prepared some useful theorems for operation of Radix-$2^k$ numbers. In the second section, we proved some properties about carry on Radix-$2^k$ sub signed-digit numbers. In the last section, we defined the new addition operation using Radix-$2^k$ sub signed-digit numbers, and we clarified its correctness.

- Preliminaries
- Carry Operation at $n+1$ Digits Radix-$2^k$ Sub Signed-Digit Number
- Definition for Adder Operation on Radix-$2^k$ Sub Signed-Digit Number

- [1]
Grzegorz Bancerek.
The fundamental properties of natural numbers.
*Journal of Formalized Mathematics*, 1, 1989. - [2]
Grzegorz Bancerek.
Joining of decorated trees.
*Journal of Formalized Mathematics*, 5, 1993. - [3]
Grzegorz Bancerek and Krzysztof Hryniewiecki.
Segments of natural numbers and finite sequences.
*Journal of Formalized Mathematics*, 1, 1989. - [4]
Czeslaw Bylinski.
Functions and their basic properties.
*Journal of Formalized Mathematics*, 1, 1989. - [5]
Yoshinori Fujisawa and Yasushi Fuwa.
Definitions of radix-$2^k$ signed-digit number and its adder algorithm.
*Journal of Formalized Mathematics*, 11, 1999. - [6]
Andrzej Kondracki.
The Chinese Remainder Theorem.
*Journal of Formalized Mathematics*, 9, 1997. - [7]
Masaaki Niimura and Yasushi Fuwa.
Improvement of radix-$2^k$ signed-digit number for high speed circuit.
*Journal of Formalized Mathematics*, 15, 2003. - [8]
Takaya Nishiyama and Yasuho Mizuhara.
Binary arithmetics.
*Journal of Formalized Mathematics*, 5, 1993. - [9]
Andrzej Trybulec.
Tarski Grothendieck set theory.
*Journal of Formalized Mathematics*, Axiomatics, 1989. - [10]
Michal J. Trybulec.
Integers.
*Journal of Formalized Mathematics*, 2, 1990. - [11]
Zinaida Trybulec.
Properties of subsets.
*Journal of Formalized Mathematics*, 1, 1989.

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