| |
|
|
Formal Verification of DSP Software
AbstractSoftware 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 work-in-progress in 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 are building 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). This is joint work with David Currie at UBC, and Sreeranga Rajan and Masahiro Fujita at Fujitsu Labs of America. |