Automatic formal verification of reconfigurable DSPs

Author

Velev, Miroslav N. ; Gao, Ping

Author_Institution

Aries Design Autom., Chicago, IL, USA

fYear

2011

fDate

25-28 Jan. 2011

Firstpage

293

Lastpage

296

Abstract

We present a method for automatic formal verification of Digital Signal Processors (DSPs) that have VLIW architecture and reconfigurable functional units optimized for accelerating Software Defined Radio (SDR) applications to be used for future space communications by NASA. The formal verification was done with the highly automatic method of Correspondence Checking by exploiting the property of Positive Equality that allows a dramatic simplification of the solution space and many orders of magnitude speedup. The formal verification of a complex reconfigurable DSP took approximately 10 minutes of CPU time on a single workstation, when using our industrial-strength tool flow.

Keywords

digital signal processing chips; electronic engineering computing; formal verification; software radio; SDR; VLIW architecture; automatic formal verification; correspondence checking; digital signal processor; positive equality; reconfigurable DSP; reconfigurable functional unit; software defined radio; Design automation; Digital signal processing; Equations; Formal verification; Mathematical model; Program processors; VLIW;

fLanguage

English

Publisher

ieee

Conference_Titel

Design Automation Conference (ASP-DAC), 2011 16th Asia and South Pacific

Conference_Location

Yokohama

ISSN

2153-6961

Print_ISBN

978-1-4244-7515-5

Type

conf

DOI

10.1109/ASPDAC.2011.5722201

Filename

5722201