Deriving approximation tolerance constraints from verification runs

TL;DR

This paper introduces a novel method to derive hardware tolerance constraints from standard verification runs, ensuring correctness in approximate computing systems using abstract interpretation techniques.

Contribution

It presents a new approach to determine tolerance constraints for approximate hardware from verification results, bridging verification and hardware design verification.

Findings

Constraints guarantee verification results on approximate hardware

Method successfully applied to example C programs

Effective extraction of tolerance constraints from predicate abstraction

Abstract

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.