Automatic functional verification of memory oriented global source code transformations

In this paper, we present a fully automatic technique to verify an important class of optimizing program transformations applied to reduce accesses to the data memory. These are prevalent while developing software for power and performance-efficient embedded multimedia systems. The verification of the transformations relies on an automatic proof of functional equivalence of the initial and the transformed program functions. It is based on extracting and reasoning on the polyhedral models representing the dependencies between the elements of the output and the input variables, which are preserved under the transformations considered. If the verification reports failure, the technique also identifies the errors and their location in the function, hence providing an effective means to debug the transformed program function.