This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Proofs of Correctness and Properties of Integer Adder Circuits
January 2010 (vol. 59 no. 1)
pp. 134-136
ASCII Text
x 
 
Gang Chen, Feng Liu, "Proofs of Correctness and Properties of Integer Adder Circuits," IEEE Transactions on Computers, vol. 59, no. 1, pp. 134-136, January, 2010.
 
 
BibTex
x
 
@article{ 10.1109/TC.2009.137,
author = {Gang Chen and Feng Liu},
title = {Proofs of Correctness and Properties of Integer Adder Circuits},
journal ={IEEE Transactions on Computers},
volume = {59},
number = {1},
issn = {0018-9340},
year = {2010},
pages = {134-136},
doi = {http://doi.ieeecomputersociety.org/10.1109/TC.2009.137},
publisher = {IEEE Computer Society},
address = {Los Alamitos, CA, USA},
}
 
 
RefWorks Procite/RefMan/Endnote
x 
 
TY - JOUR
JO - IEEE Transactions on Computers
TI - Proofs of Correctness and Properties of Integer Adder Circuits
IS - 1
SN - 0018-9340
SP134
EP136
EPD - 134-136
A1 - Gang Chen,
A1 - Feng Liu,
PY - 2010
KW - Formal method
KW - computer arithmetic
KW - adder circuits.
VL - 59
JA - IEEE Transactions on Computers
ER -
 
Gang Chen, Lingcore Laboratory, King City
Feng Liu, National Lab of Parallel Distributing Processing, Hunan
Adder circuits have been extensively studied. Their formal properties are well known, but the proofs are either incomplete or difficult to find. This short contribution intends to integrate all formal proofs related to adders in a single place and to add the details when necessary. The presentation is accessible to general VLSI designer. Another goal of this study is to put together relevant materials for the preparation of further formal studies in computer arithmetic. The presentation is made as concise as possible.

[1] R.P. Brent and H.T. Kung, “A Regular Layout for Parallel Adders,” IEEE Trans. Computers, vol. 31, no. 3, pp. 260-264, Mar. 1982.
[2] R. Jackson and S. Talwar, “High Speed Binary Addition,” Proc. Conf. Record of the 38th Asilomar Conf. Signals, Systems and Computers, vol. 2, pp. 1350-1353, Nov. 2004.
[3] D. Kapur and M. Subramaniam, “Mechanical Verification of Adder Circuits Using Rewrite Rule Laboratory,” Formal Methods in System Design, vol. 13, no. 2, pp. 127-158, Oct. 1998.
[4] P.M. Kogge and H.S. Stone, “A Parallel Algorithm for the Efficient Solution of a General Class of Recurrence Equations,” IEEE Trans. Computers, vol. 22, no. 8, pp. 786-793, Aug. 1973.
[5] I. Koren, Computer Arithmetic Algorithms, second ed. A.K. Peters, 2002.
[6] R. Ladner and M. Fischer, “A Regular Layout for Parallel Adders,” J. ACM, vol. 27, no. 4, pp. 831-838, Oct. 1980.
[7] T. Lynch and E.E. Swartzlander, “A Spanning Tree Carry Lookahead Adder,” IEEE Trans. Computers, vol. 41, no. 8, pp. 931-939, Aug. 1992.
[8] J. O'Donnell and G. Rünger, “Derivation of a Carry Lookahead Addition Circuit,” J. Functional Programming, vol. 14, no. 6, pp. 127-158, Oct. 2004.
[9] M. Sheeran, “Hardware Design and Functional Programming: A Perfect Match,” J. Universal Computer Science, vol. 11, no. 7, pp. 1135-1158, 2005.

Index Terms:
Formal method, computer arithmetic, adder circuits.
Citation:
Gang Chen, Feng Liu, "Proofs of Correctness and Properties of Integer Adder Circuits," IEEE Transactions on Computers, vol. 59, no. 1, pp. 134-136, Jan. 2010, doi:10.1109/TC.2009.137
Usage of this product signifies your acceptance of the Terms of Use.