Login | Register

An approach for the formal verification of DSP designs using Theorem proving

Title:

An approach for the formal verification of DSP designs using Theorem proving

Akbarpour, B. and Tahar, Sofiène (2006) An approach for the formal verification of DSP designs using Theorem proving. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 25 (8). pp. 1441-1457. ISSN 0278-0070

[img]
Preview
Text (application/pdf)
TCAD-2006.pdf - Accepted Version
311kB

Official URL: http://dx.doi.org/10.1109/TCAD.2005.857314

Abstract

This paper proposes a framework for the incorporation of formal methods in the design flow of digital signal processing (DSP) systems in a rigorous way. In the proposed approach, DSP descriptions were modeled and verified at different abstraction levels using higher order logic based on the higher order logic (HOL) theorem prover. This framework enables the formal verification of DSP designs that in the past could only be done partially using conventional simulation techniques. To this end, a shallow embedding of DSP descriptions in HOL at the floating-point (FP), fixed-point (FXP), behavioral, register transfer level (RTL), and netlist gate levels is provided. The paper made use of existing formalization of FP theory in HOL and a parallel one developed for FXP arithmetic. The high ability of abstraction in HOL allows a seamless hierarchical verification encompassing the whole DSP design path, starting from top-level FP and FXP algorithmic descriptions down to RTL, and gate level implementations. The paper illustrates the new verification framework on the fast Fourier transform (FFT) algorithm as a case study.

Divisions:Concordia University > Gina Cody School of Engineering and Computer Science > Electrical and Computer Engineering
Item Type:Article
Refereed:Yes
Authors:Akbarpour, B. and Tahar, Sofiène
Journal or Publication:IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems
Date:2006
Digital Object Identifier (DOI):10.1109/TCAD.2005.857314
Keywords:Design automation digital signal processors error analysis fast Fourier transforms finite wordlength effects formal verification higher order logic theorem proving
ID Code:977378
Deposited By: DANIELLE DENNIE
Deposited On:14 Jun 2013 15:32
Last Modified:18 Jan 2018 17:44

References:

B. Akbarpour, Modeling and verification of DSP designs in HOL, 2005 :Dept. Elect. Comput. Eng., Concordia Univ.

B. Akbarpour and S. Tahar, "A methodology for the formal verification of FFT algorithms in HOL", Formal Methods in Computer-Aided Design, vol. 3312, pp.37 -51 2004 :Springer-Verlag

B. Akbarpour and S. Tahar, "Error analysis of digital filters using theorem proving", Theorem Proving in Higher Order Logics, vol. 3223, pp.1 -16 2004 :Springer-Verlag

B. Akbarpour and S. Tahar, "The application of formal verification to SPW designs", Proc. Euromicro Symp. Digital System Design, pp.325 -332 2003

B. Akbarpour, S. Tahar, and A. Dekdouk, "Formalization of fixed-point arithmetic in HOL", Form. Methods Syst. Des., vol. 27, no. 1/2, pp.173 -200 2005

R. Boulton, A. Gordon, M. Gordon, J. Harrison, J. Herbert, and J. Van-Tassel, "Experience with embedding hardware description languages in HOL", Theorem Provers in Circuit Design, pp.129 -156 1992 :North Holland

P. Bjesse, "Automatic verification of combinational and pipelined FFT circuits", Computer Aided Verification, vol. 1633, pp.380 -393 1999 :Springer-Verlag

E. O. Brigham, The Fast Fourier Transform, 1974 :Prentice-Hall

V. Capretta, "Certifying the fast Fourier transform with Coq", Theorem Proving in Higher Order Logics, vol. 2152, pp.154 -168 2001 :Springer-Verlag

Signal Processing WorkSystem (SPW) User',s Guide, 1999

CoCentric System Studio User',s Guide, 2001

W. T. Cochran, et al., "What is the fast Fourier transform", IEEE Trans. Audio Electroacoust., vol. AU-15, no. 2, pp.45 -55 1967

J. W. Cooley and J. W. Tukey, "An algorithm for machine calculation of complex Fourier series", Math. Comput., vol. 19, no. 90, pp.297 -301 1965

G. Forsythe and C. B. Moler, Computer Solution of Linear Algebraic Systems, 1967 :Prentice-Hall

R. A. Gamboa, "The correctness of the fast Fourier transform: A structural proof in ACL2", Form. Methods Syst. Des., Special Issue on UNITY, vol. 20, no. 1, pp.91 -106 2002

W. M. Gentleman and G. Sande, "Fast Fourier transforms&mdash,For fun and profit", AFIPS Fall Joint Computer Conf., San Francisco, CA, vol. 29, pp.563 -578 1966

M. J. C. Gordon and T. F. Melham, Introduction to HOL: A Theorem Proving Environment for Higher Order Logic, 1993 :Cambridge Univ. Press

J. R. Harrison, "Constructing the real numbers in HOL", Form. Methods Syst. Des., vol. 5, no. 1/2, pp.35 -59 1994

J. R. Harrison, "A machine-checked theory of floating-point arithmetic", Theorem Proving in Higher Order Logics, vol. 1690, pp.113 -130 1999 :Springer-Verlag

J. R. Harrison, "Floating-point verification in HOL light: The exponential function", Form. Methods Syst. Des., vol. 16, no. 3, pp.271 -305 2000

J. R. Harrison, "Complex quantifier elimination in HOL", Supplemental Proc. Int. Conf. Theorem Proving Higher Order Logics, pp.159 -174 2001

J. R. Harrison and L. Th&eacute,ry, "A skeptic',s approach to combining HOL and Maple", J. Autom. Reason., vol. 21, no. 3, pp.279 -294 1998

M. Huhn, K. Schneider, T. Kropf, and G. Logothetis, "Verifying imprecisely working arithmetic circuits", Proc. Design Automation and Test Eur. Conf., pp.65 -69 1999

IEEE Standard for Binary Floating-Point Arithmetic, 1985

T. Kaneko and B. Liu, "Accumulation of round-off error in fast Fourier transforms", J. Assoc. Comput. Mach., vol. 17, no. 4, pp.637 -654 1970

H. Keding, M. Willems, M. Coors, and H. Meyr, "FRIDGE: A fixed-point design and simulation environment", Proc. Design Automation and Test Eur. Conf., pp.429 -435 1998

B. Liu and T. Kaneko, "Roundoff error in fast Fourier transforms (decimation in time)", Proc. IEEE, vol. 63, no. 6, pp.991 -992 1975

Simulink Reference Manual, 1996

T. Melham, "Higher order logic and hardware verification", Cambridge Tracts in Theoretical Computer Science, vol. 31, 1993 :Cambridge Univ. Press

J. Misra, "Powerlists: A structure for parallel recursion", ACM Trans. Program. Lang. Syst., vol. 16, no. 6, pp.1737 -1767 1994

A. V. Oppenheim and R. W. Schafer, Discrete-Time Signal Processing, 1989 :Prentice-Hall

A. V. Oppenheim and C. J. Weinstein, "Effects of finite register length in digital filtering and the fast Fourier transform", Proc. IEEE, vol. 60, no. 8, pp.957 -976 1972

T. Thong and B. Liu, "Fixed-point fast Fourier transform error analysis", IEEE Trans. Acoust., Speech, Signal Process., vol. ASSP-24, no. 6, pp.563 -573 1976

C. J. Weinstein, "Roundoff noise in floating point fast Fourier transform computation", IEEE Trans. Audio Electroacoust., vol. AU-17, no. 3, pp.209 -215 1969

P. D. Welch, "A fixed-point fast Fourier transform error analysis", IEEE Trans. Audio Electroacoust., vol. AU-17, no. 2, pp.151 -157 1969

J. H. Wilkinson, Rounding Errors in Algebraic Processes, 1963 :Prentice-Hall

High-Performance 64-Point Complex FFT/IFFT V2.0, Product Specification, 2000 [online] Available:
http://xilinx.com/ipcenter
All items in Spectrum are protected by copyright, with all rights reserved. The use of items is governed by Spectrum's terms of access.

Repository Staff Only: item control page

Downloads per month over past year

Back to top Back to top