IBM Logo
IBM Research Lab in Haifa
Hot Shots  
FV Research in HRL  

Download the presentation

Alan J. Hu

University of British Columbia


Formal Verification of DSP Software

Software for digital signal processors is a particularly promising area for automatic formal verification. Hand-written assembly code is still very common in this area. Even when compilers are used, the generated code is frequently hand-tuned for performance reasons.
Making programming difficult for both humans and compilers is the fact that typical DSP architectures are highly non-orthogonal, with many specialized instructions that perform multiple operations in parallel and sometimes even lacking pipeline interlocks. Even a very limited verification tool would be useful in practice.

In this talk, I describe our on-going work developing such a tool. By combining symbolic simulation with cooperating decision procedures for uninterpreted functions with equality, memory, and presburger arithmetic (the SVC system developed at Stanford), we have built a verification tool that compares small, structurally similar assembly language routines for a Fujitsu DSP. Preliminary results on some small examples are promising: we have found several bugs while comparing fragments of production assembly code handwritten by experts to compiled code that was allegedly equivalent. We have also encountered many difficulties, some of which I will discuss. We are working toward handling larger examples, and more accurately modeling the DSP state. The approach should generalize for other 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).
Other potential applications of this research include verification of compiler optimizations and verification of microcode.

This is joint work with David Currie at Mentor Graphics, and Sreeranga Rajan and Masahiro Fujita at Fujitsu Labs of America.