Skip to main content
SpringerLink
Log in

Formal Verification of Floating Point Trigonometric Functions

  • Conference paper
  • First Online:
Formal Methods in Computer-Aided Design (FMCAD 2000)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 1954))

Included in the following conference series:

Abstract

We have formal verified a number of algorithms for evaluat-ing transcendental functions in double-extended precision floating point arithmetic in the Intel® IA-64 architecture. These algorithms are used in the ItaniumTM processor to provide compatibility with IA-32 (x86) hardware transcendentals, and similar ones are used in mathematical software libraries. In this paper we describe in some depth the formal verification of the sin and cos functions, including the initial range reduction step. This illustrates the diferent facets of verification in this field, covering both pure mathematics and the detailed analysis of floating point rounding.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. D. Bailey, P. Borwein, and S. Plouffe. On the rapid computation of various polylogarithmic constants. Mathematics of Computation, 66:903–913, 1997.

    Article  MATH  MathSciNet  Google Scholar 

  2. A. Baker. A Consise Introduction to the Theory of Numbers. Cambridge University Press, 1985.

    Google Scholar 

  3. G. Cousineau and M. Mauny. The Functional Approach to Programming. Cam-bridge University Press, 1998.

    Google Scholar 

  4. T. J. Dekker. A floating-point technique for extending the available precision. Numerical Mathematics, 18:224–242, 1971.

    Article  MATH  MathSciNet  Google Scholar 

  5. M. J. C. Gordon, R. Milner, and C. P. Wadsworth. Edinburgh LCF: A Mechanised Logic of Computation, volume 78 of Lecture Notes in Computer Science. Springer-Verlag, 1979.

    Google Scholar 

  6. R. L. Graham, D. E. Knuth, and O. Patashnik. Concrete Mathematics: A Foun-dation for Computer Science. Addison-Wesley, 2nd edition, 1994.

    Google Scholar 

  7. J. Harrison. HOL Light: A tutorial introduction. In M. Srivas and A. Camilleri, editors, Proceedings of the First International Conference on Formal Methods in Computer-Aided Design (FMCAD’96), volume 1166 of Lecture Notes in mputerScience, pages 265–269. Springer-Verlag, 1996.

    Google Scholar 

  8. J. Harrison. Verifying the accuracy of polynomial approximations in HOL. In E. L. Gunter and A. Felty, editors, Theorem Proving in Higher Order Logics: 10th International Conference, TPHOLs’97, volume 1275 of Lecture Notes in Computer Science, pages 137–152, Murray Hill, NJ, 1997. Springer-Verlag.

    Google Scholar 

  9. J. Harrison. Theorem Proving with the Real Numbers. Springer-Verlag, 1998. Revised version of author’s PhD thesis.

    Google Scholar 

  10. J. Harrison. A machine-checked theory of floating point arithmetic. In Y. Bertot, G. Dowek, A. Hirschowitz, C. Paulin, and L. Théry, editors, Theorem Proving in Higher Order Logics: 12th International Conference, TPHOLs’99, volume 1690 of Lecture Notes in Computer Science, pages 113–130, Nice, France, 1999. Springer-Verlag.

    Google Scholar 

  11. J. Harrison, T. Kubaska, S. Story, and P. Tang. The computation of transcendental functions on the IA-64 architecture. Intel Technology Journal, 1999-2Q4:1–7, 1999. This paper is available on the Web as http://developer.intel.com/technology/itj/q41999/articles/art_5.htm

    Google Scholar 

  12. O. Møller. Quasi double-precision in floating-point addition. BIT, 5:37–50, 1965.

    Article  MATH  Google Scholar 

  13. M. E. Remes. Sur le calcul effectif des polynomes d'approximation de Tchebichef. Comptes Rendus Hebdomadaires des Séances de l'Académie des Sciences, 199:337–340, 1934.

    MATH  Google Scholar 

  14. P. H. Sterbenz. Floating-Point Computation. Prentice-Hall, 1974.

    Google Scholar 

  15. S. Story and P. T. P. Tang. New algorithms for improved transcendental functions on IA-64. In I. Koren and P. Kornerup, editors, Proceedings, 14th IEEE symposium on on computer arithmetic, pages 4–11, Adelaide, Australia, 1999. IEEE Computer Society.

    Google Scholar 

  16. P. T. P. Tang. Table-lookup algorithms for elementary functions and their error analysis. In Proceedings of the 10th Symposium on Computer Arithemtic, pages 232–236, 1991.

    Google Scholar 

  17. P. Weis and X. Leroy. Le langage Caml. InterEditions, 1993. See also the CAML Web page: http://pauillac.inria.fr/caml/

Download references

Author information

Authors and Affiliations

  1. Intel Corporation, EY2-035200 NE Elam Young Parkway, OR 97124, Hillsboro, USA

    John Harrison

Authors
  1. John Harrison
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Austin Research Laboratories, IBM Corporation, Mail Stop 9460, Building 904 11501 Burnet Road, 78758, Austin, Texas, USA

    Warren A. Hunt Jr.

  2. Computer Science Department, Indiana University, Lindley Hall, 150 W. Woodlawn Avenue, 47405-7104, Bloomington, Indiana, USA

    Steven D. Johnson

Rights and permissions

Reprints and permissions

Copyright information

© 2000 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Harrison, J. (2000). Formal Verification of Floating Point Trigonometric Functions. In: Hunt, W.A., Johnson, S.D. (eds) Formal Methods in Computer-Aided Design. FMCAD 2000. Lecture Notes in Computer Science, vol 1954. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-40922-X_14

Download citation

  • DOI: https://doi.org/10.1007/3-540-40922-X_14

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-41219-9

  • Online ISBN: 978-3-540-40922-9

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation