文献类型：期刊文献

中文题名：FFT处理机的形式化模型及正确性验证

英文题名：Formal model of FFT processor and its verification

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

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

年份：2007

卷号：43

期号：2

起止页码：10

中文期刊名：计算机工程与应用

外文期刊名：Computer Engineering and Applications

收录：CSTPCD;;北大核心:【北大核心2004】；CSCD:【CSCD2011_2012】；

基金：国家自然科学基金资助项目(60373075)。

语种：中文

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

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

摘要：快速傅立叶变换的应用领域非常广泛,其硬件实现方法多种多样,验证这些电路的正确性具有很强的实用价值。传统的电路正确性验证的方法是模拟,这种方法的主要缺点是随着参与运算的点数的增加,穷尽模拟全部输入情况所耗费的时间越来越长,甚至难以实现。而形式化方法使用纯数学手段证明电路的正确性,克服了传统方法的缺点。首先用重写系统给出了任意N=2M点的基2的流水式快速傅里叶变换处理机的形式化模型,然后给出它的正确性验证,探索了验证处理复数的复杂电路正确性的方法。
Fast Fourier Transform（FFr） 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.