Skip to main content
SpringerLink
Log in

Verification of IEEE compliant subtractive division algorithms

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

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

Included in the following conference series:

Abstract

A parameterized definition of subtractive floating point division algorithms is presented and verified using PVS. The general algorithm is proven to satisfy a formal definition of an IEEE standard for floating point arithmetic. The utility of the general specification is illustrated using a number of different instances of the general algorithm.

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

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Mark D. Aagaard and Carl-Johan H. Seger. The formal verification of a pipelined double-precision IEEE floating-point multiplier. In Proceedings 1995 IEEE/ACM International Conference on Computer-Aided Design, pages 7–10, San Jose, CA, November 1995.

    Google Scholar 

  2. Geoff Barrett. A formal approach to rounding. In Proceedings 8th Symposium on Computer Arithmetic, pages 247–254, 1987.

    Google Scholar 

  3. Geoff Barrett. Formal methods applied to a floating-point number system. IEEE Transactions on Software Engineering, 15(5):611–621, May 1989.

    Google Scholar 

  4. Bhaskar Bose. DRS — derivational reasoning system: A digital design derivation system for hardware synthesis. In T. Hilburn, G. Suski, and J. Zalewski, editors, Safety and Reliability in Emerging Control Technologies. Elsevier Science Publishers, Oxford, UK, 1996. ISBN 0 08 042610 7, to be published.

    Google Scholar 

  5. E. M. Clarke, S. M. German, and X. Zhao. Verifying the SRT division algorithm using theorem proving techniques. In Rajeev Alur and Thomas A. Henzinger, editors, Computer-Aided Verification, CAV '96, number 1102 in Lecture Notes in Computer Science, New Brunswick, NJ, July/August 1996. Springer-Verlag.

    Google Scholar 

  6. Milos D. Ercegovac and Tomás Lang. Division and Square Root: Digit-Recurrence Algorithms and Implementations. Kluwer Academic Publishers, 1994.

    Google Scholar 

  7. IEEE-754. Standard for Binary Floating-Point Arithmetic, 1985. ANSI/IEEE Std 754-1985.

    Google Scholar 

  8. IEEE-854. Standard for Radix-Independent Floating-Point Arithmetic, 1987. ANSI/IEEE Std 854-1987.

    Google Scholar 

  9. J. Harrison. Floating point verification in HOL. In E.T. Schubert, P.J. Windley, and J. Alves-Foss, editors, Proceedings 8th International Workshop on Higher Order Logic Theorem Proving and its Applications, volume 971 of Lecture Notes in Computer Science, pages 186–199, Aspen Grove, UT, USA, September 1995. Springer Verlag.

    Google Scholar 

  10. J. O'Leary, M. Leeser, J. Hickey, and M. Aagaard. Non-restoring integer square root: A case study in design by principled optimization. In T. Kropf and R. Kumar, editors, Proc. 2nd International Conference on Theorem Provers in Circuit Design (TPCD94), volume 901 of Lecture Notes in Computer Science, pages 52–71, Bad Herrenalb, Germany, September 1994. Springer Verlag, published 1995.

    Google Scholar 

  11. Steven D. Johnson. Synthesis of Digital Design from Recursion Equations. The MIT Press, Cambridge, MA, 1984. ACM Distinguished Dissertation 1984.

    Google Scholar 

  12. Israel Koren. Computer Arithmetic Algorithms. Prentice Hall, 1993.

    Google Scholar 

  13. M. Leeser and J. O'Leary. Verification of a subtractive radix-2 square root algorithm and implementation. In Proceedings International Conference on Computer Design 1995 (ICCD '95), pages 526–531, October 1995.

    Google Scholar 

  14. Irwin Meisels and Mark Saaltink. The Z/EVES reference manual (draft). Technical Report TR-95-5493-03, ORA Canada, December 1995.

    Google Scholar 

  15. Paul S. Miner. Defining the IEEE-854 floating-point standard in PVS. Technical Memorandum 110167, NASA, Langley Research Center, Hampton, VA, June 1995.

    Google Scholar 

  16. J Strother Moore, Tom Lynch, and Matt Kaufmann. A mechanically checked proof of the correctness of the kernel of the AMD5k86 floating point division algorithm. (Submitted), URL:http://devil.ece.utexas.edu:80/∼lynch/divide/-divide.html, March 1996.

    Google Scholar 

  17. Sam Owre, John Rushby, Natarajan Shankar, and Friedrich von Henke. Formal verification for fault-tolerant architectures: Prolegomena to the design of PVS. IEEE Transactions on Software Engineering, 21(2):107–125, February 1995.

    Google Scholar 

  18. H. Rueß, N. Shankar, and M. K. Srivas. Modular verification of SRT division. In Rajeev Alur and Thomas A. Henzinger, editors, Computer-Aided Verification, CAV '96, number 1102 in Lecture Notes in Computer Science, pages 123–134, New Brunswick, NJ, July/August 1996. Springer-Verlag.

    Google Scholar 

  19. David M. Russinoff. A mechanically checked proof of correctness of the AMD K5 floating-point square root algorithm, unpublished manuscript, July 1996.

    Google Scholar 

  20. George S. Taylor. Compatible hardware for division and square root. In Proceedings 5th Symposium on Computer Arithmetic, pages 127–134, 1981.

    Google Scholar 

  21. V. Pratt. Anatomy of the Pentium bug. In P.D. Mosses, M. Nielsen, and M.I. Schwartzbach, editors, TAPSOFT '95: Theory and Practice of Software Development, volume 915 of Lecture Notes in Computer Science, pages 97–107, Aarhus, Denmark, May 1995. Springer Verlag.

    Google Scholar 

  22. D. Verkest, L. Claesen, and H. De Man. A proof of the nonrestoring division algorithm and its implementation on an ALU. Formal Methods in System Design, 4:5–31, January 1994.

    Google Scholar 

  23. J. S. Walther. A unified algorithm for elementary functions. In Proceedings of Spring Joint Computer Conference, pages 379–385, 1971.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. NASA Langley Research Center, 23681-0001, Hampton, VA, USA

    Paul S. Miner

  2. Department of Electrical and Computer Engineering, Old Dominion University, 23529, Norfolk, VA, USA

    James F. Leathrum Jr.

Authors
  1. Paul S. Miner
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. James F. Leathrum Jr.
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Mandayam Srivas Albert Camilleri

Rights and permissions

Reprints and permissions

Copyright information

© 1996 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Miner, P.S., Leathrum, J.F. (1996). Verification of IEEE compliant subtractive division algorithms. In: Srivas, M., Camilleri, A. (eds) Formal Methods in Computer-Aided Design. FMCAD 1996. Lecture Notes in Computer Science, vol 1166. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0031800

Download citation

  • DOI: https://doi.org/10.1007/BFb0031800

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-61937-6

  • Online ISBN: 978-3-540-49567-3

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation