Deriving approximation tolerance constraints from verification runs
This addresses the problem of software verification for approximate computing, enabling energy-efficient hardware while maintaining correctness guarantees, though it is incremental as it builds on existing abstract interpretation methods.
The paper tackles the challenge of verifying program correctness on approximate hardware by deriving tolerance constraints from standard verification runs, ensuring that verification results remain valid when hardware meets these constraints, and demonstrates the approach on C programs and approximate adders.
Approximate computing (AC) is an emerging paradigm for energy-efficient computation. The basic idea of AC is to sacrifice high precision for low energy by allowing for hardware which only carries out "approximately correct" calculations. For software verification, this challenges the validity of verification results for programs run on approximate hardware. In this paper, we present a novel approach to examine program correctness in the context of approximate computing. In contrast to all existing approaches, we start with a standard program verification and compute the allowed tolerances for AC hardware from that verification run. More precisely, we derive a set of constraints which - when met by the AC hardware - guarantees the verification result to carry over to AC. Our approach is based on the framework of abstract interpretation. On the practical side, we furthermore (1) show how to extract tolerance constraints from verification runs employing predicate abstraction as an instance of abstract interpretation, and (2) show how to check such constraints on hardware designs. We exemplify our technique on example C programs and a number of recently proposed approximate adders.