Technical Report

Verification of the Fast Fourier Transform using HOL Theorem Proving

Behzad Akbarpour and Sofiène Tahar

ABSTRACT


The fast Fourier transform (FFT) is an algorithm to compute the discrete Fourier transform (DFT) with a substantial time saving over conventional methods. Two basic classes of FFT algorithms are the decimation-in-time (DIT) and decimation-in-frequency (DIF). In this report we describe the formal verification of the FFT algorithms at different abstraction levels based on the HOL theorem prover. We make use of existing theories in HOL on real and complex real, IEEE standard based floating-point, and fixed-point arithmetic to model the FFT algorithms in HOL. Then, we establish fundamental analysis lemmas as our models to derive expressions for the accumulation of roundoff error in floating- and fixed-point FFT algorithms implementation in comparison to the corresponding ideal real specification. Based on the extensively studied related work on computing the errors due to finite precision effects in the realization of FFT algorithms with floating- and fixed-point arithmetics using theoretical paper-and-pencil proofs and simulation techniques since the late sixties, we performed a similar error analysis using the HOL theorem proving environment. The HOL formalization and proofs are found to be in good agreement with the theoretical counterparts. Finally, we use a classical hierarchical proof approach in HOL to prove that the FFT implementation at behavioral, register transfer (RT), and netlist gate levels implies the high level fixed-point algorithmic specification.

 
Download Postscript  file (PS File) 
Download PDF file (PDF File) 
Send comments and suggestions to: behzad@ece.concordia.ca