关键词: 重写, 形式化, 描述, 验证, 归纳, 快速傅里叶变换处理机

Abstract: Fast Fourier Transform (FFT) has a wide range of usage; it also has many various ways of hardware implements. Simulation is a traditional way for hardware verifying, the main weakness of this method is that it is a hard work (sometimes it is impossible) 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. This paper presents a formal model of Radix-2 FFT processor using Rewriting System and verifies that it can process complex data properly. These explore a new way to verify complex circuit.

Key words: rewriting, formal method, specification, verify, induction, FFT processor