论文研究 FFT处理机的形式化模型及正确性验证.pdf

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