文献类型：期刊文献

中文题名：基2的流水式快速傅里叶变换处理机的形式化模型

英文题名：A Formal Model of Radix-2 Fast Fourier Transform Processor

作者：张欢欢[1];宋国新[1];邵志清[1]

机构：[1]华东理工大学计算机科学与工程系,上海200237

年份：2007

卷号：33

期号：2

起止页码：227

中文期刊名：华东理工大学学报（自然科学版）

外文期刊名：Journal of East China University of Science and Technology

收录：CSTPCD;;EI(收录号：20072210628432);Scopus;北大核心:【北大核心2004】；CSCD:【CSCD2011_2012】；

基金：国家自然科学基金(60373075)

语种：中文

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

外文关键词：rewriting; formal method; specification; verification; induction; FFT processor

摘要：快速傅里叶变换(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.