|
Formal Verification of DSP Software
Abstract
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 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.
|