Title :
Automatic formal verification of reconfigurable DSPs
Author :
Velev, Miroslav N. ; Gao, Ping
Author_Institution :
Aries Design Autom., Chicago, IL, USA
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;
Conference_Titel :
Design Automation Conference (ASP-DAC), 2011 16th Asia and South Pacific
Conference_Location :
Yokohama
Print_ISBN :
978-1-4244-7515-5
DOI :
10.1109/ASPDAC.2011.5722201
