摘要
快速傅里叶变换(FFT)的应用领域非常广泛,其硬件实现方法多种多样。传统的电路正确性验证的方法是模拟,这种方法的主要缺点是不能穷尽模拟全部输入情况,而形式化方法使用纯数学手段证明电路具有某些属性,从而证明其正确性。所以用形式化方法验证FFT电路的正确性具有极强的实用价值。形式化验证的第一步工作是对要验证的电路进行建模,因此本文首先介绍了国内外FFT形式化建模的主要方法和优缺点,然后用重写系统给出了任意N=2M点的基2的流水式快速傅里叶变换处理机的形式化模型,显示了重写系统用于复杂硬件电路建模的优越性,为进一步的电路正确性验证奠定基础。
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 Radix-2 FFT processor using rewrite systems. It shows that rewrite systems can well specify complex hardware circuits.
出处
《华东理工大学学报（自然科学版）》
EI
CAS
CSCD
北大核心
2007年第2期227-232,共6页
Journal of East China University of Science and Technology
基金
国家自然科学基金(60373075)
关键词
重写
形式化
描述
验证
归纳
快速傅里叶变换处理机
rewriting
formal method
specification
verification
induction
FFT processor
