nach oben

Erschienen in:

2020 | OriginalPaper | Buchkapitel

Satisfiability Solving Meets Evolutionary Optimisation in Designing Approximate Circuits

verfasst von : Milan Češka, Jiří Matyáš, Vojtech Mrazek, Tomáš Vojnar

Erschienen in: Theory and Applications of Satisfiability Testing – SAT 2020

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

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.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Vorheriges Kapitel Matrix Multiplication: Verifying Strong Uniquely Solvable Puzzles

Nächstes Kapitel SAT Solving with Fragmented Hamiltonian Path Constraints for Wire Arc Additive Manufacturing

Audemard, G., Simon, L.: On the glucose SAT solver. Int. J. Artif. Intell. Tools 27, 1840001 (2018)CrossRef

Bruttomesso, R., Cimatti, A., Franzén, A., Griggio, A., Sebastiani, R.: The MathSAT 4 SMT Solver. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 299–303. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-70545-1_28CrossRef

Češka, M., Matyáš, J., et al.: Approximating complex arithmetic circuits with formal error guarantees: 32-bit multipliers accomplished. In: International Conference on Computer Aided Design (ICCAD’2017), pp. 416–423. IEEE (2017)

Češka, M., Matyáš, J., Mrazek, V., Sekanina, L., Vasicek, Zdenek, Vojnar, Tomáš: ADAC: Automated design of approximate circuits. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10981, pp. 612–620. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-96145-3_35CrossRef

Chandrasekharan, A., Soeken, M., et al.: Precise error determination of approximated components in sequential circuits with model checking. In: Design Automation Conference (DAC’2016), pp. 129:1–129:6. ACM (2016)

de Moura, L., Bjørner, N.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-78800-3_24CrossRef

Eén, N., Sörensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502–518. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-24605-3_37CrossRef

Froehlich, S., Große, D., Drechsler, R.: One method - all error-metrics: a three-stage approach for error-metric evaluation in approximate computing. In: Design, Automation Test in Europe Conference Exhibition (2019)

Froehlich, S., Grosse, D., Drechsler, R.: Approximate hardware generation using symbolic computer algebra employing grobner basis. In: Design, Automation Test in Europe Conference Exhibition (DATE’2018), pp. 889–892. IEEE (2018)

10.

Gupta, V., Mohapatra, D., et al.: Low-power digital signal processing using approximate adders. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 32(1), 124–137 (2013)CrossRef

11.

Haaswijk, W., Soeken, M., et al.: SAT based exact synthesis using DAG topology families. In: Design Automation Conference (DAC’2018), pp. 1–6 (2018)

12.

Heule, M.J.H., Kiesl, B., Biere, A.: Encoding redundancy for satisfaction-driven clause learning. In: Vojnar, T., Zhang, L. (eds.) TACAS 2019. LNCS, vol. 11427, pp. 41–58. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-17462-0_3CrossRef

13.

Lotfi, A., Rahimi, A., et al.: Grater: an approximation workflow for exploiting data-level parallelism in FPGA acceleration. In: Design, Automation Test in Europe Conference Exhibition (DATE’2016), pp. 1279–1284. EDA Consortium (2016)

14.

Mahdiani, H.R., Ahmadi, A., et al.: Bio-inspired imprecise computational blocks for efficient VLSI implementation of soft-computing applications. IEEE Trans. Circuits Syst. I Regul. Pap. 57(4), 850–862 (2010)MathSciNetCrossRef

15.

Miller, J.F., Thomson, P.: Cartesian genetic programming. In: Poli, R., Banzhaf, W., Langdon, W.B., Miller, J., Nordin, P., Fogarty, T.C. (eds.) EuroGP 2000. LNCS, vol. 1802, pp. 121–132. Springer, Heidelberg (2000). https://doi.org/10.1007/978-3-540-46239-2_9CrossRef

16.

Mrazek, V., Hrbacek, R., et al.: EvoApprox8b: library of approximate adders and multipliers for circuit design and benchmarking of approximation methods. In: Design, Automation Test in Europe Conference Exhibition (DATE’2017) (2017)

17.

Mrazek, V., Sarwar, S.S., et al.: Design of power-efficient approximate multipliers for approximate artificial neural networks. In: International Conference on Computer Aided Design (ICCAD’2016), pp. 811–817. ACM (2016)

18.

Nepal, K., Hashemi, S., et al.: Automated high-level generation of low-power approximate computing circuits. IEEE Trans. Emerg. Top. Comput. 7, 18–30 (2018)

19.

Reda, S., Shafique, M. (eds.): Approximate Circuits. Springer, Cham (2019). https://doi.org/10.1007/978-3-319-99322-5CrossRef

20.

Riazanov, A., Voronkov, A.: The design and implementation of vampire. AI Commun. 15, 91–110 (2002)MATH

21.

Soeken, M.: Cirkit (version 3). https://github.com/msoeken/cirkit (2019)

22.

Soeken, M., Amarù, L.G., et al.: Exact synthesis of majority-inverter graphs and its applications. IEEE Trans. Comput. -Aided Des. Integr. Circuits Syst. 36(11), 1842–1855 (2017)CrossRef

23.

Soeken, M., De Micheli, G., Mishchenko, A.: Busy man’s synthesis: combinational delay optimization with sat. In: Design, Automation Test in Europe Conference Exhibition (DATE’2017), pp. 830–835 (2017)

24.

Soeken, M., Haaswijk, W., et al.: Practical exact synthesis. In: Design, Automation Test in Europe Conference Exhibition (DATE’2018), pp. 309–314 (2018)

25.

Vasicek, Z., Mrazek, V.: Towards low power approximate DCT architecture for HEVC standard. In: Design, Automation Test in Europe Conference Exhibition (DATE’2017) (2017)

26.

Vasicek, Z., Sekanina, L.: Evolutionary approach to approximate digital circuits design. IEEE Trans. Evol. Comput. 19(3), 432–444 (2015)CrossRef

27.

Vašíček, Z., Slaný, K.: Efficient phenotype evaluation in cartesian genetic programming. In: Moraglio, A., Silva, S., Krawiec, K., Machado, P., Cotta, Carlos (eds.) EuroGP 2012. LNCS, vol. 7244, pp. 266–278. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-29139-5_23CrossRef

28.

Venkatesan, R., Agarwal, A., et al.: MACACO: Modeling and analysis of circuits for approximate computing. In: International Conference on Computer Aided Design (ICCAD’2011), pp. 667–673. ACM(2011)

Titel: Satisfiability Solving Meets Evolutionary Optimisation in Designing Approximate Circuits
verfasst von: Milan Češka
Jiří Matyáš
Vojtech Mrazek
Tomáš Vojnar
Verlag: Springer International Publishing
Buch: Theory and Applications of Satisfiability Testing – SAT 2020
Print ISBN: 978-3-030-51824-0

Electronic ISBN: 978-3-030-51825-7

Copyright-Jahr: 2020
DOI: https://doi.org/10.1007/978-3-030-51825-7_33

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"