Automatic formal verification of dsp software
Automatic formal verification of dsp software
复制标题
DSP软件的自动形式验证
DOI：
--
复制
发表时间：
2000
期刊：
影响因子：
--
通讯作者：
S. Rajan
中科院分区：
文献类型：
--
作者：
David W. Currie;Alan J. Hu;S. Rajan
本文介绍了一种新型的形式验证方法，用于对数字信号处理器（DSP）的小型组装程序进行等效检查。通过结合控制流分析，符号模拟，自动决策过程和某些特定领域的优化，我们构建了一个自动验证工具，该工具可以比较结构相似的DSP汇编语言例程。我们对从真实的应用程序中获取的代码样本进行了测试，并自动发现了几个以前未知的错误。在所有示例中，运行时和内存要求都是合理的。我们的方法应轻松地概括为多个DSP体系结构，最终允许对两个不同DSP的代码进行比较（例如，从一个DSP验证一个端口到另一个DSP），并处理更复杂的DSP（例如静态固定的，VLIW）。
This paper describes a novel formal verification approach for equivalence checking of small, assembly-language routines for digital signal processors (DSP). By combining control-flow analysis, symbolic simulation, automatic decision procedures, and some domain-specific optimizations, we have built an automatic verification tool that compares structurally similar DSP assembly language routines. We tested our tool on code samples taken from a real application program and discovered several previously unknown bugs automatically. Runtime and memory requirements were reasonable on all examples. Our approach should generalize easily for multiple DSP architectures, eventually allowing comparison of code for two different DSPs (e.g., to verify a port from one DSP to another) and handling more complex DSPs (e.g. statically-scheduled, VLIW).