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.