abstract = "We present a novel method allowing one to approximate
complex arithmetic circuits with formal guarantees on
the approximation error. The method integrates in a
unique way formal techniques for approximate
equivalence checking into a search-based circuit
optimisation algorithm. The key idea of our approach is
to employ a novel search strategy that drives the
search towards promptly verifiable approximate
circuits. The method was implemented within the ABC
tool and extensively evaluated on functional
approximation of multipliers (with up to 32-bit
operands) and adders (with up to 128-bit operands).
Within a few hours, we constructed a high-quality
Pareto set of 32-bit multipliers providing trade-offs
between the circuit error and size. This is for the
first time when such complex approximate circuits with
formal error guarantees have been derived, which
demonstrates an outstanding performance and scalability
of our approach compared with existing methods that
have either been applied to the approximation of
multipliers limited to 8-bit operands or statistical
testing has been used only. Our approach thus
significantly improves capabilities of the existing
methods and paves a way towards an automated design
process of provably correct circuit approximations.",