2005b). Functional equivalence checking for verification of algebraic transformations on array-intensive source code

Development of energy and performance-efficient embed-ded software is increasingly relying on application of com-plex transformations on the critical parts of the source code. Designers applying such nontrivial source code transforma-tions are often faced with the problem of ensuring functional equivalence of the original and transformed programs. Cur-rently they have to rely on incomplete and time-consuming simulation. Formal automatic verification of the transformed program against the original is instead desirable. This calls for equivalence checking tools similar to the ones available for comparing digital circuits. We present such a tool to com-pare array-intensive programs related through a combination of important global transformations like expression propaga-tions, loop and algebraic transformations. When the trans-formed program fails to pass the equivalence check, the tool provides specific feedback on the possible locations of errors.