An Entry for THE 8th ANNUAL (2011) "HUMIES" AWARDS FOR HUMAN-COMPETITIVE RESULTS PRODUCED BY GENETIC AND EVOLUTIONARY COMPUTATION HELD AT THE GENETIC AND EVOLUTIONARY COMPUTATION CONFERENCE GECCO 2011

(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: 

Paper 1: Vasicek Z., Sekanina L.: Formal Verification of Candidate Solutions for Post-Synthesis Evolutionary Optimization in Evolvable Hardware. Genetic Programming and Evolvable Machines, Vol. 12, 2011, in press, accepted on Feb 21, 2011, see Online First Articles, http://www.springerlink.com/content/h7q3322n202p0744/

Paper 2: Vasicek Z., Sekanina L.: A Global Postsynthesis Optimization Method for Combinational Circuits. In: Proc. of the Design, Automation and Test in Europe Conference -- DATE 2011, Grenoble, EDAA, 2011, p. 1525-1528 (928 submissions, 34% acceptance rate)

(2) the name, complete physical mailing address, e-mail address, and phone number of EACH author of EACH paper: 

Paper 1 and 2:
Zdenek Vasicek, Faculty of Information Technology, Brno University of Technology, Bozetechova 2, 612 66 Brno, Czech Republic, e-mail: vasicek@fit.vutbr.cz, phone: +420541141354

Lukas Sekanina, Faculty of Information Technology, Brno University of Technology, Bozetechova 2, 612 66 Brno, Czech Republic, e-mail: sekanina@fit.vutbr.cz, phone: +420541141215

(3) the name of the corresponding author (i.e., the author to whom notices will be sent concerning the competition):

Lukas Sekanina

(4) the abstract of the paper(s):

Paper 1:
We propose to utilize a formal verification algorithm to reduce the fitness evaluation time for evolutionary post-synthesis optimization in evolvable hardware. The proposed method assumes that a fully functional digital circuit is available. A post-synthesis optimization is then conducted using Cartesian Genetic Programming (CGP) which utilizes a satisfiability problem solver to decide whether a candidate solution is functionally correct or not. It is demonstrated that the method can optimize digital circuits of tens of inputs and thousands of gates. Furthermore, the number of gates was reduced for the LGSynth93 benchmark circuits by 37.8% on average with respect to results of the conventional SIS tool.

Paper 2:
A genetic programming-based circuit synthesis method is proposed that enables to globally optimize the number of gates in circuits that have already been synthesized using common methods such as ABC and SIS. The main contribution is a proposal for a new fitness function that enables to significantly reduce the fitness evaluation time in comparison to the state of the art. The fitness function performs optimized equivalence checking using a SAT solver. It is shown that the equivalence checking time can significantly be reduced when knowledge of the parent circuit and its mutated offspring is taken into account. For a cost of a runtime, results of conventional synthesis conducted using SIS and ABC were improved by 20-40\% for the LGSynth93 benchmarks.

(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:

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): 

Efficient logic synthesis and optimization have been crucial for computer theory as well as computer industry for more than 50 years. Nowadays, many companies provide commercial tools that allow producing reasonable logic synthesis and optimization in a reasonable time. However, the recent work in the area of conventional synthesis has shown that these tools produce solutions that are far from optimum for many circuit classes (e.g. Cong, J., Minkovich, K.: IEEE Trans. on CAD 26(2), 230-239, 2007). Evolvable hardware community has demonstrated that very efficient implementations of digital circuits can be obtained using evolutionary computation, particularly by means of Cartesian Genetic Programming, CGP (e.g. Vassilev, V., Job, D., Miller, J.F.: Proc. of the 2nd NASA/DoDWorkshop on Evolvable Hardware, 2000). Unfortunately, the evolutionary circuit design is able to discover innovate designs only for small circuit instances (approx. up to 20 inputs and 100 gates). One of the key problems is a very time consuming fitness calculation which typically grows exponentially with increasing circuit complexity (number of inputs).

We have shown in papers 1 and 2 that it is possible to significantly reduce the number of gates for complex circuits, too. Very compact implementations can be obtained if the fitness calculation utilizes a formal verification algorithm (a SAT solver in our case) to check whether a candidate circuit is functionally correct or not. For the cost of runtime, the best-obtained results of conventional synthesis conducted using academia tools (SIS and ABC) and 3 commercial tools were improved by the proposed method in 20-40% for the standard LGSynth93 benchmarks (over 100 inputs and 1000 gates). Smaller logic designs clearly lead to smaller area on a chip, and potentially to reducing power consumption and shortening the test application time. 

To summarize:
D: The result of our method is an optimized implementation of a digital circuit (e.g. ALU4) which is typically much smaller than the best result obtained from a conventional synthesis tool. Such solution is publishable in its own right as a new scientific result - independent of the fact that the result was mechanically created - because a clear improvement in the area on a chip can be demonstrated with respect to the state-of-the-art.

E: Because (i) the results of our method are better than the results obtained using the state-of the-art academia as well as commercial tools for a standard circuit benchmark set and (ii) the state-of-the-art tools are based on the best implementations proposed so far, we claim that our solution 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. 

G: Despite the fact that various logic synthesis and optimization tools have been proposed in the last 50 years, the logic synthesis/optimization problem is considered as very difficult. We claim that the proposed method solves a problem of indisputable difficulty in its field.

(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):

Paper 1: Vasicek Z., Sekanina L.: Formal Verification of Candidate Solutions for Post-Synthesis Evolutionary Optimization in Evolvable Hardware. Genetic Programming and Evolvable Machines,  Spec. Issue on Evolvable Hardware Challenges, Vol. 12, 2011, in press 

Paper 2: Vasicek Z., Sekanina L.: A Global Postsynthesis Optimization Method for Combinational Circuits. In: Proc. of the Design, Automation and Test in Europe Conference -- DATE 2011, Grenoble, EDAA, 2011, p. 1525-1528

(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 judges should consider the entry as "best" in comparison to other entries that may also be "human-competitive": 

(a) We demonstrated a notable contribution to the evolutionary circuit design and evolvable hardware theory: We significantly eliminated the scalability problem of the fitness function evaluation which has been known from the very beginning of digital evolvable hardware. We believe that the approaches based on formal verification techniques could lead to many new applications of evolvable hardware, genetic programming and evolutionary design/optimization. Our contribution was accepted by a leading journal in the field of genetic programming and evolvable hardware - Genetic Programming and Evolvable Machines - in its special issue on Evolvable hardware challenges. 

(b) We demonstrated a significant contribution which has a great impact to applications: The proposed method - which benefits from the use of evolutionary computing - is capable of discovering logic circuit transformations that are unreachable by conventional minimization algorithms. Therefore, more compact circuits can be discovered. The result was presented on one of the leading conferences in the field of circuit design automation, DATE 2011. The community of circuit designers is conservative and pragmatic with respect to completely new approaches and methodologies. Many well-performing conventional approaches/tools have been proposed for this particular problem (Karnaugh map, Quine-McCluskey algorithm, Espresso, ABC, SIS) and many commercial companies have been active in this area in last 50 years. In summary, achieving a new contribution using evolutionary computation is very difficult in this particular problem domain.