Abstract
Few designs, mostly those of Texas Instruments, continue to use two’s complement floating point units. Such units are simpler to build and to validate, but they do not comply to the dominant IEEE standard for floating point arithmetic. We compare some properties of the two systems in this text. Some features are lost, but others remain unchanged. One strong example is the case of Sterbenz’s theorem and our recent extension. We show in the paper that the theorem and its extension hold for the two’s complement architecture. Still, users should ensure that results are large enough on circuits that do not implement gradual underflow. Theorems have been proven and validated using the Coq automatic proof checker.
Similar content being viewed by others
References
Amerkad A, Bertot Y, Rideau L, Pottier L (2001) Mathematics and proof presentation in Pcoq. In: Proceedings of the conference on proof transformation and presentation and proof complexities, Siena, Italy. Available at: http://www-sop.inria.fr/lemme/Laurence.Rideau/proof-pcoq.ps.gz
Barrett G (1989) Practical algorithm for selection on coarse grained parallel computers. IEEE Trans Softw Eng 15:611–621. http://dlib.computer.org/ts/books/ts1989/pdf/e0611.pdf
Boldo S, Daumas M (2002) Properties of the subtraction valid for any floating point system. In: Proceedings of the 7th international workshop on formal methods for industrial critical systems, Málaga, Spain, pp 137–149
Carreño VA, Miner PS (1995) Specification of the IEEE-854 floating-point standard in HOL and PVS. In: Proceedings of the 1995 international workshop on higher order logic theorem proving and its applications, Aspen Grove, UT, supplemental proceedings. Available at: http://shemesh.larc.nasa.gov/fm/ftp/larc/vac/hug95.ps
Chen YA, Clarke E, Ho PH, Hoskote Y, Kam T, Khaira M, O’Leary J, Zhao X (1996) Verification of all circuits in a floating point unit using word level model checking. In: Srivas M, Camilleri A (eds) Proceedings of the 1st international conference on formal methods in computer-aided design, Palo Alto, CA, pp 19–33
Cody WJ, Karpinski R et al (1984) A proposed radix and word-length independent standard for floating point arithmetic. IEEE Micro 4:86–100
Collins RR (1997) Inside the Pentium II math bug. Dr. Dobb’s Journal 22(8):52, 55–57. Available at: http://www.ddj.com/articles/1997/9708/9708f/9708f.htm
Coonen JT (1978) Specification for a proposed standard for floating point arithmetic. Memorandum ERL M78/72, University of California, Berkeley
Cowlishaw MF (2003) Decimal floating point: algorithm for computers. In: Bajard JC, Schulte M (eds) Proceedings of the 16th symposium on computer arithmetic, Santiago de Compostela, Spain, 2003, pp 104–111. Available at: http://csdl.computer.org/comp/proceedings/arith/2003/1894/00/1894toc.htm
Daumas M, Langlois P (2003) Additive symmetries: the non-negative case. Theor Comput Sci 291:143–157. Available at: http://dx.doi.org/10.1016/S0304-3975(02)00223-2
Daumas M, Matula DW (1997) Validated roundings of dot products by sticky accumulation. IEEE Trans Comput 46:623–629.
Daumas M, Rideau L, Théry L (2001) A generic library of floating-point numbers and its application to exact computing. In: Proceedings of the 14th international conference on theorem proving in higher order logics. Edinburgh, UK, pp 169–184.
Demmel J (1984) Underflow and the reliability of numerical software. SIAM J Sci Stat Comput 5:887–919
Goldberg D (1991) What every computer scientist should know about floating point arithmetic. ACM Comput Surv 23:5–47. Available at: http://www.acm.org/pubs/articles/journals/surveys/1991-23-1/p5-goldberg/p5-goldberg.pdf
Harrison J (1999) A machine-checked theory of floating point arithmetic. In: Bertot Y, Dowek G, Hirschowitz A, Paulin C, Théry L (eds) Proceedings of the 12th international conference on theorem proving in higher order logics, Nice, France, pp 113–130. Available at: http://www.cl.cam.ac.uk/users/jrh/papers/fparith.ps.gz
Harrison J (2000) Formal verification of floating point trigonometric functions. In: Hunt WA, Johnson SD (eds) Proceedings of the 3rd international conference on formal methods in computer-aided design, Austin, TX, pp 217–233. Available at: http://www.link.springer.de/link/service/series/0558/papers/1954/19540217.pdf
Higham NJ (1996) Accuracy and stability of numerical algorithms. SIAM, Philadelphia. Available at: http://www.ma.man.ac.uk/∼higham/asna.html. Also at: http://www.maths.man.ac.uk/∼higham/asna/
Huet G, Kahn G, Paulin-Mohring C (1997) The Coq proof assistant: a tutorial: version 6.1. Technical Report 204, Institut National de Recherche en Informatique et en Automatique, Le Chesnay, France. Available at: ftp://ftp.inria.fr/INRIA/publication/publi-pdf/RT/RT-0204.pdf
Jacobi C (2001) Formal verification of a theory of IEEE rounding. In: Proceedings of the 14th international conference on theorem proving in higher order logics, Edinburgh, UK, pp 239–254, supplemental proceedings. Available at: http://www.informatics.ed.ac.uk/publications/online/0046/b239.pdf
Kern C, Greenstreet MR (1999) Formal verification in hardware design: a survey. ACM Trans Des Automat Electron Sys 4:123–193. Available at: http://delivery.acm.org/10.1145/310000/307989/p123-kern.pdf
Knuth DE (1997) The art of computer programming: seminumerical algorithms, 3rd edn. Addison-Wesley, Reading, MA
Kulisch U (2000) Rounding near zero. In: Proceedings of the 4th real numbers and computers conference, Dagstuhl, Germany, pp 23–29
Laurent O, Michel P, Wiels V (2001) Using formal verification techniques to reduce simulation and test effort. In: Proceedings of the international symposium of formal methods Europe, Berlin, Germany, pp 465–477. Available at: http://link.springer.de/link/service/series/0558/papers/2021/20210465.pdf
Li RC, Boldo S, Daumas M (2003) Theorems on efficient argument reductions. In: Bajard JC, Schulte M (eds) Proceedings of the 16th symposium on computer arithmetic, Santiago de Compostela, Spain, pp 129–136.
Markstein P (2000) IA-64 and elementary functions: speed and precision. Prentice Hall, Upper Saddle River, NJ. Available at: http://www.markstein.org/
Miner PS, Leathrum JF (1996) Verification of IEEE compliant subtractive division algorithms. In: Proceedings of the 1st international conference on formal methods in computer-aided design, pp 64–78. Available at: http://www.ece.odu.edu/∼leathrum/Formal_Methods/computer_arithmetic/fmcad.ps
O’Leary J, Zhao X, Gerth R, Seger CJH (1999) Formally verifying IEEE compliance of floating point hardware. Intel Technol J, vol 3. Available at: http://developer.intel.com/technology/itj/q11999/pdf/floating_point.pdf
Overton MJ (2001) Numerical computing with IEEE floating point arithmetic. SIAM, Philadelphia. Available at: http://www.siam.org/catalog/mcc07/ot76.htm
Priest DM (1992) On properties of floating point arithmetics: numerical stability and the cost of accurate computations. PhD thesis, University of California at Berkeley, Berkeley, CA. Available at: ftp://ftp.icsi.berkeley.edu/pub/theory/priest-thesis.ps.Z
Rushby J, von Henke F (1991) Formal verification of algorithms for critical systems. In: Proceedings of the conference on software for critical systems, New Orleans, pp 1–15. Available at: http://www.acm.org/pubs/articles/proceedings/soft/125083/p1-rushby/p1-rushby.pdf
Russinoff DM (1998) A mechanically checked proof of IEEE compliance of the floating point multiplication, division and square root algorithms of the AMD-K7 processor. LMS J Comput Math 1:148–200. http://www.onr.com/user/russ/david/k7-div-sqrt.ps
Schryer NL (1981) A test of computer’s floating-point arithmetic unit. Technical report 89, AT&T Bell Laboratories. Available at: http://cm.bell-labs.com/cm/cs/cstr/89.ps.gz
Schwarz EM, Smith RM, Krygowski CA (1999) The S/390 G5 floating point unit supporting hex and binary architectures. In: Koren I, Kornerup P (eds) Proceedings of the 14th symposium on computer arithmetic, Adelaide, Australia, pp 258–265 . Available at: http://computer.org/proceedings/arith/0116/0116toc.htm
Sterbenz PH (1974) Floating point computation. Prentice-Hall, Upper Saddle River, NJ
Stevenson D et al (1987) An American national standard: IEEE standard for binary floating point arithmetic. ACM SIGPLAN Notices 22:9–25
Texas Instruments (1997) TMS320C3x User’s guide. Available at: http://www-s.ti.com/sc/psheets/spru031e/spru031e.pdf
Author information
Authors and Affiliations
Corresponding authors
Rights and permissions
About this article
Cite this article
Boldo, S., Daumas, M. Properties of two’s complement floating point notations. STTT 5, 237–246 (2004). https://doi.org/10.1007/s10009-003-0120-y
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10009-003-0120-y