Prof. Ing. Lukáš Sekanina, Ph.D.
ČEŠKA Milan, MATYÁŠ Jiří, MRÁZEK Vojtěch, SEKANINA Lukáš, VAŠÍČEK Zdeněk and VOJNAR Tomáš. ADAC: Automated Design of Approximate Circuits. In: Proceedings of 30th International Conference on Computer Aided Verification (CAV'18). Oxford, UK: Springer International Publishing, 2018, pp. 612-620. ISBN 978-3-319-96145-3. | Publication language: | english |
---|
Original title: | ADAC: Automated Design of Approximate Circuits |
---|
Title (cs): | ADAC: Nástroj pro automatizovaný vývoj aproximovaných obvodů |
---|
Pages: | 612-620 |
---|
Proceedings: | Proceedings of 30th International Conference on Computer Aided Verification (CAV'18) |
---|
Conference: | 30th International Conference on Computer Aided Verification |
---|
Place: | Oxford, UK, GB |
---|
Year: | 2018 |
---|
ISBN: | 978-3-319-96145-3 |
---|
DOI: | 10.1007/978-3-319-96145-3_35 |
---|
Publisher: | Springer International Publishing |
---|
Files: | |
---|
| Keywords |
---|
approximate circuits, energy-efficient computing, design automation, approximate equivalence checking, Cartesian Genetic Programming, SAT and BDD-based decision procedures |
Annotation |
---|
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. |
BibTeX: |
---|
@INPROCEEDINGS{
author = {Milan {\v{C}}e{\v{s}}ka and Ji{\v{r}}{\'{i}}
Maty{\'{a}}{\v{s}} and Vojt{\v{e}}ch Mr{\'{a}}zek
and Luk{\'{a}}{\v{s}} Sekanina and Zden{\v{e}}k
Va{\v{s}}{\'{i}}{\v{c}}ek and Tom{\'{a}}{\v{s}}
Vojnar},
title = {ADAC: Automated Design of Approximate Circuits},
pages = {612--620},
booktitle = {Proceedings of 30th International Conference on Computer
Aided Verification (CAV'18)},
year = {2018},
location = {Oxford, UK, GB},
publisher = {Springer International Publishing},
ISBN = {978-3-319-96145-3},
doi = {10.1007/978-3-319-96145-3_35},
language = {english},
url = {http://www.fit.vutbr.cz/research/view_pub.php?id=11731}
} |
|