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
Preview |
Text (application/pdf)
311kBTCAD-2006.pdf - Accepted Version |
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é,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
Repository Staff Only: item control page
Download Statistics
Download Statistics