Summary for
Automatic Verification for Scheduled VLIW Code

The paper extends previous work on verifying assembly code at the ISA level by applying to moderm VLIW. Aggressive VLIW designs currently expose architectural features (parallelism, pipelining, resource conflicts, lack of interlocks), which makes code generation and optimization very challenging. The verification process deals mostly with discovering resource conflicts and proving the correctness of the scheduled code.

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 technique assumes the two routines have "very similar" control flow.

The verification procedure uses a model of the processor to symbolically simulate the two routines. The simulator summarizes statements as functions of the initial inputs and states. Most machine operations are treated as "uninterpreted functions". This abstraction is safe, but restrictive (does not support functional equivalence of sequences of instructions). The logic used is the theory of uninterpreted functions, with equality, linear arithmetic, and memory read and write. They employ SVC for checking this logic used for expressions.

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.