Publication Details
Satisfiability Solving Meets Evolutionary Optimisation in Designing Approximate Circuits
Matyáš Jiří, Ing., Ph.D. (RG VERIFIT)
Mrázek Vojtěch, Ing., Ph.D. (DCSY)
Vojnar Tomáš, prof. Ing., Ph.D. (DITS)
approximate computing, genetic programming, satisfiability solving
Approximate circuits that trade the chip area or power consumption for the
precision of the computation play a key role in development of energy-aware
systems. Designing complex approximate circuits is, however, very difficult,
especially, when a given approximation error has to be guaranteed. Evolutionary
search algorithms together with SAT-based error evaluation currently represent
one of the most successful approaches for automated circuit approximation. In
this paper, we apply satisfiability solving not only for circuit evaluation but
also for its minimisation. We consider and evaluate several approaches to this
task, both inspired by existing works as well as novel ones. Our experiments show
that a combined strategy, integrating evolutionary search and SMT-based
sub-circuit minimisation (using quantified theory of arrays) that we propose, is
able to find complex approximate circuits (e.g. 16-bit multipliers) with
considerably better trade-offs between the circuit precision and size than
existing~approaches.
@inproceedings{BUT168143,
author="Milan {Češka} and Jiří {Matyáš} and Vojtěch {Mrázek} and Tomáš {Vojnar}",
title="Satisfiability Solving Meets Evolutionary Optimisation in Designing Approximate Circuits",
booktitle="Theory and Applications of Satisfiability Testing - SAT 2020",
year="2020",
series="Lecture Notes in Computer Science",
volume="12178",
pages="481--491",
publisher="Springer International Publishing",
address="Alghero",
doi="10.1007/978-3-030-51825-7\{_}33",
isbn="978-3-030-51824-0"
}