Skip to main content
SpringerLink
Log in

A Methodology for the Formal Verification of FFT Algorithms in HOL

  • Conference paper
Formal Methods in Computer-Aided Design (FMCAD 2004)

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

Included in the following conference series:

Abstract

This paper addresses the formal specification and verification of fast Fourier transform (FFT) algorithms at different abstraction levels based on the HOL theorem prover. We make use of existing theories in HOL on real and complex numbers, IEEE standard floating-point, and fixed-point arithmetics to model the FFT algorithms. Then, we derive, by proving theorems in HOL, expressions for the accumulation of roundoff error in floating- and fixed-point FFT designs with respect to the corresponding ideal real and complex numbers specification. The HOL formalization and proofs are found to be in good agreement with the theoretical paper-and-pencil counterparts. Finally, we use a classical hierarchical proof approach in HOL to prove that the FFT implementations at the register transfer level (RTL) implies the corresponding high level fixed-point algorithmic specification.

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 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.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.

Similar content being viewed by others

References

  1. Akbarpour, B., Tahar, S., Dekdouk, A.: Formalization of Cadence SPW Fixed-Point Arithmetic in HOL. In: Butler, M., Petre, L., Sere, K. (eds.) IFM 2002. LNCS, vol. 2335, pp. 185–204. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  2. Akbarpour, B., Tahar, S.: Modeling SystemC Fixed-Point Arithmetic in HOL. In: Dong, J.S., Woodcock, J. (eds.) ICFEM 2003. LNCS, vol. 2885, pp. 206–225. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  3. Akbarpour, B., Tahar, S.: Error Analysis of Digital Filters using Theorem Proving. In: Slind, K., Bunker, A., Gopalakrishnan, G.C. (eds.) TPHOLs 2004. LNCS, vol. 3223, pp. 1–16. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  4. Bjesse, P.: Automatic Verification of Combinational and Pipelined FFT Circuits. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 380–393. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  5. Boulton, R., Gordon, A., Gordon, M., Harrison, J., Herbert, J., Van-Tassel, J.: Experience with Embedding Hardware Description Languages in HOL. In: Theorem Provers in Circuit Design, pp. 129–156. North-Holland, Amsterdam (1992)

    Google Scholar 

  6. Brigham, E.O.: The Fast Fourier Transform. Prentice Hall, Englewood Cliffs (1974)

    MATH  Google Scholar 

  7. Capretta, V.: Certifying the Fast Fourier Transform with Coq. In: Boulton, R.J., Jackson, P.B. (eds.) TPHOLs 2001. LNCS, vol. 2152, pp. 154–168. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  8. Synopsys, Inc. CoCentric TM System Studio User’s Guide, USA (August 2001)

    Google Scholar 

  9. Cochran, W.T., et al.: What is the Fast Fourier Transform. IEEE Transactions on Audio and Electroacoustics AU-15, 45–55 (1967)

    Article  Google Scholar 

  10. Cooley, J.W., Tukey, J.W.: An Algorithm for Machine Calculation of Complex Fourier Series. Mathematics of Computation 19, 297–301 (1965)

    Article  MATH  MathSciNet  Google Scholar 

  11. Forsythe, G., Moler, C.B.: Computer Solution of Linear Algebraic Systems. Prentice-Hall, Englewood Cliffs (1967)

    MATH  Google Scholar 

  12. Gamboa, R.A.: The Correctness of the Fast Fourier Transform: A Structural Proof in ACL2. Formal Methods in System Design, Special Issue on UNITY (January 2002)

    Google Scholar 

  13. Gentleman, W.M., Sande, G.: Fast Fourier Transforms - For Fun and Profit. In: AFIPS Fall Joint Computer Conference, vol. 29, pp. 563–578. Spartan Books, Washington (1966)

    Google Scholar 

  14. Gordon, M.J.C., Melham, T.F.: Introduction to HOL: A Theorem Proving Environment for Higher-Order Logic. Cambridge University Press, Cambridge (1993)

    MATH  Google Scholar 

  15. Harrison, J.R.: Constructing the Real Numbers in HOL. Formal Methods in System Design 5(1/2), 35–59 (1994)

    Article  MATH  Google Scholar 

  16. Harrison, J.R.: A Machine-Checked Theory of Floating-Point Arithmetic. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin, C., Théry, L. (eds.) TPHOLs 1999. LNCS, vol. 1690, pp. 113–130. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  17. Harrison, J.R.: Floating-Point Verification in HOL Light: The Exponential Function. Formal Methods in System Design 16(3), 271–305 (2000)

    Article  Google Scholar 

  18. Harrison, J.R.: Complex Quantifier Elimination in HOL. In: Supplemental Proceedings of the International Conference on Theorem Proving in Higher Order Logics, Edinburgh, Scotland, pp. 159–174 (September 2001)

    Google Scholar 

  19. Kaneko, T., Liu, B.: Accumulation of Round-Off Error in Fast Fourier Transforms. Journal of Association for Computing Machinery 17(4), 637–654 (1970)

    MATH  MathSciNet  Google Scholar 

  20. Keding, H., Willems, M., Coors, M., Meyr, H.: FRIDGE: A Fixed-Point Design and Simulation Environment. In: Proceedings Design Automation and Test in Europe Conference, Paris, France, pp. 429–435 (February 1998)

    Google Scholar 

  21. Liu, B., Kaneko, T.: Roundoff Error in Fast Fourier Transforms (Decimation in Time). In: Proceedings of the IEEE (Proceedings Letters), pp. 991–992 (June 1975)

    Google Scholar 

  22. Mathworks, Inc. Fixed-Point Blockset User’s Guide (ver. 2.0) (1999)

    Google Scholar 

  23. Melham, T.: Higher Order Logic and Hardware Verification. Cambridge Tracts in Theoretical Computer Science, vol. 31. Cambridge University Press, Cambridge (1993)

    Book  MATH  Google Scholar 

  24. Misra, J.: Powerlists: A Structure for Parallel Recursion. ACM Transactions on Programming Languages and Systems 16(6), 1737–1767 (1994)

    Article  Google Scholar 

  25. Oppenheim, A.V., Schafer, R.W.: Discrete-Time Signal Processing. Prentice-Hall, Englewood Cliffs (1989)

    MATH  Google Scholar 

  26. Oppenheim, A.V., Weinstein, C.J.: Effects of Finite Register Length in Digital Filtering and the Fast Fourier Transform. Proceedings of the IEEE 60(8), 957–976 (1972)

    Article  Google Scholar 

  27. Cadence Design Systems, Inc. Signal Processing WorkSystem (SPW) User’s Guide, USA (July 1999)

    Google Scholar 

  28. Thong, T., Liu, B.: Fixed-Point Fast Fourier Transform Error Analysis. IEEE Transactions on Acoustics, Speech, and Signal Processing, ASSP 24(6), 563–573 (1976)

    Article  Google Scholar 

  29. Weinstein, C.J.: Roundoff Noise in Floating Point Fast Fourier Transform Computation. IEEE Transactions on Audio and Electroacoustics AU-17(3), 209–215 (1969)

    Article  Google Scholar 

  30. Welch, P.D.: A Fixed-Point Fast Fourier Transform Error Analysis. IEEE Transactions on Audio and Electroacoustics AU-17(2), 151–157 (1969)

    Article  Google Scholar 

  31. Wilkinson, J.H.: Rounding Errors in Algebraic Processes. Prentice-Hall, Englewood Cliffs (1963)

    MATH  Google Scholar 

  32. Xilinx, Inc. High-Performance 16-Point Complex FFT/IFFT V1.0.5, Product Specification, USA (July 2000), http://xilinx.com/ipcenter

Download references

Author information

Authors and Affiliations

  1. Dept. of Electrical & Computer Engineering, Concordia University, 1455 de Maisonneuve W., Montreal, Quebec, H3G 1M8, Canada

    Behzad Akbarpour & Sofiène Tahar

Authors
  1. Behzad Akbarpour
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Sofiène Tahar
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Computer Science Department, University of British Columbia,  

    Alan J. Hu

  2. IBM Austin Research Laboratory, 11400 Burnet Rd, MS 904-6H004, TX 78758-3493, Austin, USA

    Andrew K. Martin

Rights and permissions

Reprints and permissions

Copyright information

© 2004 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Akbarpour, B., Tahar, S. (2004). A Methodology for the Formal Verification of FFT Algorithms in HOL. In: Hu, A.J., Martin, A.K. (eds) Formal Methods in Computer-Aided Design. FMCAD 2004. Lecture Notes in Computer Science, vol 3312. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-30494-4_4

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-30494-4_4

  • Publisher Name: Springer, Berlin, Heidelberg

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

  • Online ISBN: 978-3-540-30494-4

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation