| Title: | Automatic Verification of DSP Software |
| Authors: | David W. Currie
Alan J. Hu
Sreeranga Rajan
Masahiro Fujita |
| Organizations: | Mentor Graphics
Dept of Computer Science, University of British Columbia
Fujitsu Laboratories of America
Fujitsu Laboratories of America |
| Print Information: | Proceedings of the 37th Conference on Design Automation
Pages 130 - 135
ACM SIGDA, EDAC, IEEE-CAS: DAC'00 Conference
Los Angeles, CA, 2000 |
| Online: | 1.
ACM Digital Library copy |
The paper presents a technique to verify the equivalence of
small, assembly-language routines for DSPs. The verification
method uses control-flow analysis, symbolic simulation, and
cooperating decision procedures for memory, linear arithmetic,
and uninterpreted functions with equality.
The verification task is to take two assembly-language routines
and verify that they are equivalent. This process is used to
verify the correctness of highly optmized code in relation to
the original, non-optimized version. The user specifies what
inputs are initially equal and what outputs should be equal on
termination.
The overall verification approach is to traverse the CFG in a
depth-first fashion, symbolically simulating along the
way. Branch conditions are checked for compatibility. At the end
of the trace, the outputs are checked for equivalence. On a
mismatch, the tool produces an error trace. SVC is used to
compare the results while traversing the CFG and at the end of
the verification procedure. SVC handles propositional logic,
linear arithmetic, memory read/write, and uninterpreted
functions with equality.
Assumptions:
- Single CFG
- The two CFGs to compare are "very similar"
- No program counter arithmetic or self-modifying code
- No while-loops or recursion. Fixed-count loops are
OK.
- User-defined axioms for comparison of
structurally-different code fragment.
Highlights:
- Loops are unrolled according to the decision procedure: if
the loop is proven to be taken, it is unrolled one more time;
if the loop is proven not to be taken, the loop is no longer
unrolled; otherwise, the loop code cannot be handled.
- Forward branches are handled by case-splitting (not yet
implemented).
- The simulator handles parallel execution by serializing
operation and performing a state commit only after all the
instructions executing in parallel have obtained their
operands.
- Delay slots are simulated using queues to delay the
results of an instruction.
|