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.