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