An Entry for t15th Annual (2018) "Humies" Awards For Human-Competitive Results – Produced by Genetic and Evolutionary Computation ========================================================================================================================================== 1. the complete title of one (or more) paper(s) published in the open literature describing the work that the author claims describes a human-competitive result; "Approximating Complex Arithmetic Circuits with Formal Error Guarantees: 32-bit Multipliers Accomplished" 2. the name, complete physical mailing address, e-mail address, and phone number of EACH author of EACH paper(s); Milan Ceska Faculty of Information Technology Brno University of Technology Bozetechova 2 612 66 Brno, Czech Republic e-mail: ceskam@fit.vutbr.cz tel: +420541141178 Jiri Matyas Faculty of Information Technology Brno University of Technology Bozetechova 2 612 66 Brno, Czech Republic e-mail: imatyas@fit.vutbr.cz tel: +420541141331 Vojtech Mrazek Faculty of Information Technology Brno University of Technology Bozetechova 2 612 66 Brno, Czech Republic e-mail: imrazek@fit.vutbr.cz tel: +420541141348 Lukas Sekanina Faculty of Information Technology Brno University of Technology Bozetechova 2 612 66 Brno, Czech Republic e-mail: sekanina@fit.vutbr.cz tel: +420541141215 Zdenek Vasicek Faculty of Information Technology Brno University of Technology Bozetechova 2 612 66 Brno, Czech Republic e-mail: vasicek@fit.vutbr.cz tel: +420541141354 Tomas Vojnar Faculty of Information Technology Brno University of Technology Bozetechova 2 612 66 Brno, Czech Republic e-mail: vojnar@fit.vutbr.cz tel: +420541141202 3. the name of the corresponding author (i.e., the author to whom notices will be sent concerning the competition); Zdenek Vasicek 4. the abstract of the paper(s); We present a novel method allowing one to approximate complex arithmetic circuits with formal guarantees on the approximation error. The method integrates in a unique way formal techniques for approximate equivalence checking into a search-based circuit optimisation algorithm. The key idea of our approach is to employ a novel search strategy that drives the search towards promptly verifiable approximate circuits. The method was implemented within the ABC tool and extensively evaluated on functional approximation of multipliers (with up to 32-bit operands) and adders (with up to 128-bit operands). Within a few hours, we constructed a high-quality Pareto set of 32-bit multipliers providing trade-offs between the circuit error and size. This is for the first time when such complex approximate circuits with formal error guarantees have been derived, which demonstrates an outstanding performance and scalability of our approach compared with existing methods that have either been applied to the approximation of multipliers limited to 8-bit operands or statistical testing has been used only. Our approach thus significantly improves capabilities of the existing methods and paves a way towards an automated design process of provably-correct circuit approximations. 5. a list containing one or more of the eight letters (A, B, C, D, E, F, G, or H) that correspond to the criteria (see above) that the author claims that the work satisfies; B, D, E, G 6. a statement stating why the result satisfies the criteria that the contestant claims (see examples of statements of human-competitiveness as a guide to aid in constructing this part of the submission); Approximate arithmetic circuits (particularly adders and multipliers) have been intensively studied, designed, evaluated and applied since 2010. Contrasted to common (exact) arithmetic circuits, they are optimized for one additional criterion – the error – evaluated via one or more error metrics. The goal of the approximate circuit design is to find a circuit showing the best tradeoffs among (typically four) conflicting design objectives - power consumption, area, delay and error. Approximate arithmetic circuits exhibit significantly lower power consumption than common arithmetic circuits which is crucial for the current “hot” application domains such as energy efficient deep neural networks, signal processing and data mining. A comprehensive survey of approximate arithmetic circuits is available in [Jiang17]. An open problem is how to automatically create complex approximate circuits with provable properties in terms of the error. The mainstream approaches are based on applying the divide and conquer principle - a simple approximate component is developed and then used as a building block in complex approximate circuits. The error of the resulting circuit is evaluated by means of a simulation. In our paper, we used Cartesian Genetic Programming (CGP) to approximate complex arithmetic circuits without introducing any decomposition. Moreover, the error of each candidate circuit is formally analyzed in the fitness function. In order to obtain the worst case error (WCE) of a candidate circuit, the problem is formulated as a satisfiability problem and solved with a SAT solver. However, the approach based on a common SAT solver does not scale well for multipliers (analysis of 16-bit multipliers may take hundred seconds for some instances). Hence, we introduced a verifiability driven CGP in which the SAT solver can use only a very short time to prove or disprove the submitted formula representing a candidate solution. Our method enables to generate and evaluate substantially more candidate designs in a single evolutionary run than if there is no time limit for the SAT solver. This strategy drives CGP to complex approximate circuits showing desired WCE and, at the same time, their WCE can quickly be verified. B: Literature (such as journal papers [Jiang17, Vasicek15, Kulkarni11]) shows tens of approximate 16 bit multipliers created by means of various techniques including evolutionary design (paper [Vasicek15]). By means of the proposed method, we evolved multipliers showing better tradeoffs than existing multipliers as clearly demonstrated in Fig. 6 (in the attached paper) which compares properties of selected 16 bit approximate multipliers. Moreover, as the error of 16 bit approximate multipliers presented in the literature is evaluated by means of simulation, i.e. there are no formal guarantees in terms of the error. Our approach naturally provides these formal guarantees. Hence, we can claim that our “result is equal to or better than a result that was accepted as a new scientific result at the time when it was published in a peer-reviewed scientific journal”. D: We evolved (up to) 32 bit approximate multipliers and (up to) 128 bit approximate adders with formally guaranteed WCE. In the case of multipliers, no approximate designs of this complexity are available in the literature for comparison. The evolved approximate multipliers presented in the paper are publishable in their own right as a new scientific result - independent of the fact that they were mechanically created - because no comparable designs exist in the literature. This is confirmed by the fact that our paper was accepted and presented at the ICCAD conference, which is a flagship conference in the circuit design automation field. ICCAD is an A ranked conference according to CORE database and shows ~25% acceptance ratio. E: Our result is equal to or better than the most recent human-created solution to a long-standing problem for which there has been a succession of increasingly better human-created solutions. This can be documented by a detailed comparison of the properties of evolved 16 bit approximate multipliers with the state of the art 16 bit approximate multipliers developed in recent years, which was conducted in the paper (Fig. 6). G: Despite the fact that various design principles and methods for approximate arithmetic circuits were proposed in the last 8 year, the approximate circuit design problem is not solved and it is still considered as very hard. In particular, finding good compromises between key parameters of complex circuits such as 16 or 32 bit multipliers is very difficult. We presented better solutions than the state of the art. We claim that the proposed method solves a problem of indisputable difficulty in its field. References: [Jiang17] H. Jiang, C. Liu et al.: “A review, classification, and comparative evaluation of approximate arithmetic circuits,” J. Emerg. Technol. Comput. Syst., vol. 13, no. 4, pp. 60:1–60:34, Aug. 2017 [Kulkarni11] P. Kulkarni, P. Gupta, M. D. Ercegovac: Trading accuracy for power in a multiplier architecture. Journal of Low Power Electronics, vol. 7, no. 4, pp. 490–501, 2011. ISSN 1546-1998 [Vasicek15] Z. Vasicek, L. Sekanina: Evolutionary Approach to Approximate Digital Circuits Design. IEEE Transactions on Evolutionary Computation. 2015, vol. 19, no. 3, pp. 432-444 7. a full citation of the paper (that is, author names; publication date; name of journal, conference, technical report, thesis, book, or book chapter; name of editors, if applicable, of the journal or edited book; publisher name; publisher city; page numbers, if applicable); Milan Ceska, Jiri Matyas, Vojtech Mrazek, Lukas Sekanina, Zdenek Vasicek and Tomas Vojnar: Approximating Complex Arithmetic Circuits with Formal Error Guarantees: 32-bit Multipliers Accomplished. In: Proceedings of 36th IEEE/ACM International Conference on Computer Aided Design (ICCAD). Irvine, CA, IEEE, 2017, pp. 416-423. ISBN 978-1-5386-3093-8, DOI: 10.1109/ICCAD.2017.8203807 8. a statement either that "any prize money, if any, is to be divided equally among the co-authors" OR a specific percentage breakdown as to how the prize money, if any, is to be divided among the co-authors; Any prize money is to be divided equally among the co-authors. 9. a statement stating why the authors expect that their entry would be the "best,"; (i) By means of CGP we created much better approximate multipliers (in terms of Pareto fronts showing key parameters such as power consumption and error) than the state of the art can provide. Moreover, formal guarantees in terms of error are provided by our method. (ii) We invented a new and highly efficient evolutionary circuit design method that drives the search towards promptly verifiable approximate circuits. This new search principle was later presented as a key idea behind a tool paper [Ceska18] accepted on the flagship formal verification conference (CAV – Computer Aided Verification 2018, A* according to CORE database). In addition to evolutionary computation and circuit design, our work thus also contributed to a completely different field – formal verification. (iii) Evolved approximate arithmetic circuits are now available online, in the EvoApprox8b library (http://www.fit.vutbr.cz/research/groups/ehw/approxlib/). Our statistic shows that 134 unique users from 23 countries visited the library website and spent there approximately 4 minutes on average in last 3 months. [Ceska18] Milan Ceska, Jiri Matyas, Vojtech Mrazek, Lukas Sekanina, Zdenek Vasicek and Tomas Vojnar: ADAC: Automated Design of Approximate Circuits. In: Proceedings of 30th International Conference on Computer Aided Verification (CAV'18). To appear in LNCS., 2018, pp. 1-9 10. An indication of the general type of genetic or evolutionary computation used, such as GA (genetic algorithms), GP (genetic programming), ES (evolution strategies), EP (evolutionary programming), LCS (learning classifier systems), GE (grammatical evolution), GEP (gene expression programming), DE (differential evolution), etc. CGP (Cartesian GP) 11. The date of publication of each paper. Nov 13, 2017