Advertisement

Verifying Relative Error Bounds Using Symbolic Simulation

  • Jesse Bingham
  • Joe Leslie-Hurd
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8559)

Abstract

In this paper we consider the problem of formally verifying hardware that is specified to compute reciprocal, reciprocal square root, and power-of-two functions on floating point numbers to within a given relative error. Such specifications differ from the common case in which any given input is specified to have exactly one correct output. Our approach is based on symbolic simulation with binary decision diagrams, and involves two distinct steps. First, we prove a lemma that reduces the relative error specification to several inequalities that involve reasoning about natural numbers only. The most complex of these inequalities asserts that the product of several naturals is less-than/greater-than another natural. Second, we invoke one of several customized algorithms that decides the inequality, without performing the expensive symbolic multiplications directly. We demonstrate the effectiveness of our approach on a next-generation Intel® processor design and report encouraging time and space metrics for these proofs.

Keywords

Relative Error Boolean Function Point Number Binary Decision Diagram Single Precision 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

References

  1. 1.
    Aagaard, M.D., Jones, R.B., Seger, C.-J.H.: Formal verification using parametric representations of Boolean constraints. In: Design Automation Conference (DAC 1999) (July 1999)Google Scholar
  2. 2.
    Bryant, R.E.: Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers C-35(8), 677–691 (1986)CrossRefGoogle Scholar
  3. 3.
    Bryant, R.E.: On the complexity of VLSI implementations and graph representations of Boolean functions with application to integer multiplication. IEEE Trans. Comput. 40(2), 205–213 (1991)CrossRefzbMATHMathSciNetGoogle Scholar
  4. 4.
    Darringer, J.A.: The application of program verification techniques to hardware verification. In: Proceedings of the 16th Design Automation Conference, DAC 1979, Piscataway, NJ, USA, pp. 375–381. IEEE Press (1979)Google Scholar
  5. 5.
    Goldberg, D.: What every computer scientist should know about floating point arithmetic. ACM Computing Surveys 23(1), 5–48 (1991)CrossRefGoogle Scholar
  6. 6.
    Harrison, J.V.: Formal verification of floating point trigonometric functions. In: Johnson, S.D., Hunt Jr., W.A. (eds.) FMCAD 2000. LNCS, vol. 1954, pp. 217–233. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  7. 7.
    IEEE. Standard for binary floating-point arithmetic. ANSI/IEEE Standard 754-1985. The Institute of Electrical and Electronic Engineers, Inc., 345 East 47th Street, New York, NY 10017, USA (1985)Google Scholar
  8. 8.
    Kaivola, R., Ghughal, R., Narasimhan, N., Telfer, A., Whittemore, J., Pandav, S., Slobodová, A., Taylor, C., Frolov, V., Reeber, E., Naik, A.: Replacing testing with formal verification in intel\(^{\scriptsize\circledR}\) coreTM i7 processor execution engine validation. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 414–429. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  9. 9.
    Minato, S.-I., Somenzi, F.: Arithmetic Boolean expression manipulator using BDDs. Formal Methods in System Design 10(2-3), 221–242 (1997)CrossRefGoogle Scholar
  10. 10.
    O’Leary, J., Kaivola, R., Melham, T.: Relational STE and theorem proving for formal verification of industrial circuit designs. In: Jobstmann, B., Ray, S. (eds.) Formal Methods in Computer-Aided Design (FMCAD 2013), pp. 97–104. IEEE (October 2013)Google Scholar
  11. 11.
    Parks, M.: Number-theoretic test generation for directed rounding. IEEE Trans. Comput. 49(7), 651–658 (2000)CrossRefMathSciNetGoogle Scholar
  12. 12.
    Paruthi, V.: Large-scale application of formal verification: From fiction to fact. In: Formal Methods in Computer-Aided Design (FMCAD 2010), pp. 175–180 (2010)Google Scholar
  13. 13.
    Sawada, J.: Automatic verification of estimate functions with polynomials of bounded functions. In: Formal Methods in Computer-Aided Design (FMCAD 2010), pp. 151–158 (2010)Google Scholar
  14. 14.
    Seger, C.J., Jones, R.B., O’Leary, J.W., Melham, T., Aagaard, M.D., Barrett, C., Syme, D.: An industrially effective environment for formal hardware verification. Trans. Comp.-Aided Des. Integ. Cir. Sys. 24(9), 1381–1405 (2006)CrossRefGoogle Scholar
  15. 15.
    Seger, C.-J.H., Bryant, R.E.: Formal verification by symbolic evaluation of partially-ordered trajectories. Formal Methods in System Design 6(2), 147–189 (1995)CrossRefGoogle Scholar
  16. 16.
    Slobodová, A., Davis, J., Swords, S., Hunt, W.A.: A flexible formal verification framework for industrial scale validation. In: Singh, S., Jobstmann, B., Kishinevsky, M., Brandt, J. (eds.) MEMOCODE, pp. 89–97. IEEE (2011)Google Scholar
  17. 17.
    Stewart, D.: Formal for everyone - Challenges in achievable multicore design and verification. In: Cabodi, G., Singh, S. (eds.) Formal Methods in Computer-Aided Design (FMCAD 2012), p. 186. IEEE (October 2012), http://www.cs.utexas.edu/ hunt/FMCAD/FMCAD12/FormalForEveryone_DStewart _ARM.pdfGoogle Scholar
  18. 18.
    Thathachar, J.: On the limitations of ordered representations of functions. In: Vardi, M.Y. (ed.) CAV 1998. LNCS, vol. 1427, pp. 232–243. Springer, Heidelberg (1998)CrossRefGoogle Scholar

Copyright information

© Springer International Publishing Switzerland 2014

Authors and Affiliations

  • Jesse Bingham
    • 1
  • Joe Leslie-Hurd
    • 1
  1. 1.Intel CorporationHillsboroU.S.A

Personalised recommendations