ADAC: Automated Design of Approximate Circuits

ADAC: Automated Design of Approximate Circuits

Paper in proceedings (conference paper)

Approximate circuits with relaxed requirements on functional correctness play an important role in the development of resource-efficient computer systems. Designing approximate circuits is a very complex and time-demanding process trying to find optimal trade-offs between the approximation error and resource savings. In this paper, we present ADAC - a novel framework for automated design of approximate arithmetic circuits. ADAC integrates in a unique way efficient simulation and formal methods for approximate equivalence checking into a search-based circuit optimisation. To make ADAC easily accessible, it is implemented as a module of the ABC tool: a~state-of-the-art system for circuit synthesis and verification. Within several hours, ADAC is able to construct high-quality Pareto sets of complex circuits (including even 32-bit multipliers), providing useful trade-offs between the resource consumption and the error that is formally guaranteed. This demonstrates outstanding performance and scalability compared with other existing approaches.

Approximate circuits with relaxed requirements on functional correctness play an important role in the development of resource-efficient computer systems. Designing approximate circuits is a very complex and time-demanding process trying to find optimal trade-offs between the approximation error and resource savings. In this paper, we present ADAC - a novel framework for automated design of approximate arithmetic circuits. ADAC integrates in a unique way efficient simulation and formal methods for approximate equivalence checking into a search-based circuit optimisation. To make ADAC easily accessible, it is implemented as a module of the ABC tool: a~state-of-the-art system for circuit synthesis and verification. Within several hours, ADAC is able to construct high-quality Pareto sets of complex circuits (including even 32-bit multipliers), providing useful trade-offs between the resource consumption and the error that is formally guaranteed. This demonstrates outstanding performance and scalability compared with other existing approaches.

approximate circuits, energy-efficient computing, design automation, approximate equivalence checking, Cartesian Genetic Programming, SAT and BDD-based decision procedures

approximate circuits, energy-efficient computing, design automation, approximate equivalence checking, Cartesian Genetic Programming, SAT and BDD-based decision procedures

ČEŠKA, M.; MATYÁŠ, J.; MRÁZEK, V.; VAŠÍČEK, Z.; SEKANINA, L.; VOJNAR, T.

2019

14.07.2018

Springer International Publishing

Oxford, UK

978-3-319-96145-3

Proceedings of 30th International Conference on Computer Aided Verification (CAV'18)

612

620

8

https://www.fit.vut.cz/research/publication/11731/

ADACAutomatedDesignOfApproxima