Functional Equivalence Checking for Verification of Algebraic Transformations on Array-Intensive Source Code

TL;DR

This paper introduces an automated formal verification tool for checking the functional equivalence of array-intensive programs after complex source code transformations, improving reliability over traditional simulation methods.

Contribution

It presents a novel equivalence checking tool specifically designed for array-intensive source code transformations, with detailed error localization capabilities.

Findings

Successfully verifies transformed array-intensive programs

Provides specific feedback on potential error locations

Enhances confidence in code transformations for embedded software

Abstract

Development of energy and performance-efficient embedded software is increasingly relying on application of complex transformations on the critical parts of the source code. Designers applying such nontrivial source code transformations are often faced with the problem of ensuring functional equivalence of the original and transformed programs. Currently 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 compare array-intensive programs related through a combination of important global transformations like expression propagations, loop and algebraic transformations. When the transformed program fails to pass the equivalence check, the tool provides specific feedback on the possible locations of errors.