Publication Details
ADAC: Automated Design of Approximate Circuits
Matyáš Jiří, Ing., Ph.D. (RG VERIFIT)
Mrázek Vojtěch, Ing., Ph.D. (DCSY)
Vašíček Zdeněk, doc. Ing., Ph.D. (DCSY)
Sekanina Lukáš, prof. Ing., Ph.D. (DCSY)
Vojnar Tomáš, prof. Ing., Ph.D. (DITS)
approximate circuits, energy-efficient computing, design automation, approximate equivalence checking, Cartesian Genetic Programming, SAT and BDD-based decision procedures
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.
@inproceedings{BUT155051,
author="Milan {Češka} and Jiří {Matyáš} and Vojtěch {Mrázek} and Zdeněk {Vašíček} and Lukáš {Sekanina} and Tomáš {Vojnar}",
title="ADAC: Automated Design of Approximate Circuits",
booktitle="Proceedings of 30th International Conference on Computer Aided Verification (CAV'18)",
year="2018",
pages="612--620",
publisher="Springer International Publishing",
address="Oxford, UK",
doi="10.1007/978-3-319-96145-3\{_}35",
isbn="978-3-319-96145-3",
url="https://www.fit.vut.cz/research/publication/11731/"
}