A Formal Model of Radix-2 Fast Fourier Transform Processor

Fast fourier transform(FFT) has a wide range of applications and many various ways of hardware implementations.Simulation is a traditional way for hardware verification,the main weakness of this method is to give all kinds of input that the circuit may have.On the contrast,formal methods can use pure mathematical methods to verify a circuit's properties.That is why exploring new ways to verify the correctness of FFT hardware circuits using formal method is important.Because a formal model should be given in advance of verification,this paper introduces some formal models of FFT.Then it presents a(formal) model of Radix2 FFT processor using rewrite systems.It shows that rewrite systems can well specify complex hardware circuits.