Journal article

 
Vašíček, Z., Sekanina, L.: Formal verification of candidate solutions for post-synthesis evolutionary optimization in evolvable hardware, In: Genetic Programming and Evolvable Machines, Vol. 12, No. 3, 2011, Berlin, DE, p. 305-327, ISSN 1389-2576
Publication language:english
Original title:Formal verification of candidate solutions for post-synthesis evolutionary optimization in evolvable hardware
Title (cs):Formální verifikace kandidátních řešení pro evoluční optimalizaci v evolvable hardware
Pages:305-327
Place:DE
Year:2011
Journal:Genetic Programming and Evolvable Machines, Vol. 12, No. 3, Berlin, DE
ISSN:1389-2576
URL:http://www.springerlink.com/content/h7q3322n202p0744/ [HTML]
Files: 
+Type Name Title Size Modified
iconvasicek_sekanina_genp2011.pdf520 KB2011-07-18 16:12:29
^ Select all
With selected:
Keywords
genetic programming, circuit optimization, SAT solver, evolvable hardware
Annotation
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.
BibTeX:
@ARTICLE{
   author = {Zdeněk Vašíček and Lukáš Sekanina},
   title = {Formal verification of candidate solutions for
	post-synthesis evolutionary optimization in evolvable
	hardware},
   pages = {305--327},
   journal = {Genetic Programming and Evolvable Machines},
   volume = {12},
   number = {3},
   year = {2011},
   ISSN = {1389-2576},
   language = {english},
   url = {http://www.fit.vutbr.cz/research/view_pub.php?id=9712}
}