Automatic formal verification of DSP software

被引：35

作者：

Currie, DW ^{[1
]}

Hu, AJ ^{[1
]}

Rajan, S ^{[1
]}

Fujita, M ^{[1
]}

机构：

[1] Mentor Graph Corp, Billerica, MA USA

来源：

37TH DESIGN AUTOMATION CONFERENCE, PROCEEDINGS 2000 | 2000年

关键词：

D O I：

10.1145/337292.337339

中图分类号：

TP [自动化技术、计算机技术];

学科分类号：

0812 ;

摘要：

This paper describes a novel formal verification approach for equivalence checking of small, assembly-language routines for digital signal processors (DSP). By combining control-8ow 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).

引用

页码：130 / 135

页数：6

共 10 条

[1]

Aho A., 1988, Compilers - Principles, Techniques and Tools

[2]

BALAKRISHNAN S, 1997, TR402 CONC U

[3] Formally specifying and mechanically verifying programs for the Motorola complex arithmetic processor DSP [J].

Brock, BC ;

Hunt, WA .

INTERNATIONAL CONFERENCE ON COMPUTER DESIGN - VLSI IN COMPUTERS AND PROCESSORS, PROCEEDINGS, 1997, :31-36

[4] A METHODOLOGY FOR HARDWARE VERIFICATION BASED ON LOGIC SIMULATION [J].

BRYANT, RE .

JOURNAL OF THE ACM, 1991, 38 (02) :299-328

[5]

Carter W. C., 1979, 16th design automation conference proceedings, P280, DOI 10.1109/DAC.1979.1600119

[6]

DILL DL, 1999, SVC HOME PAGE

[7]

JAIN J, 1997, INT C VLSI DESIGN

[8]

MINATO S, 1996, INT C COMP AID DES I

[9]

Rajan SP, 1999, HARDW SOFTW CODES, P2, DOI 10.1109/HSC.1999.777381

[10] A formal verification technique for embedded software. [J].

Thiry, O ;

Claesen, L .

INTERNATIONAL CONFERENCE ON COMPUTER DESIGN - VLSI IN COMPUTERS AND PROCESSORS, PROCEEDINGS, 1996, :352-357

← 1 →