Faculty of Information Technology, BUT

Publication Details

Formal verification of candidate solutions for post-synthesis evolutionary optimization in evolvable hardware

VAŠÍČEK Zdeněk and SEKANINA Lukáš. Formal verification of candidate solutions for post-synthesis evolutionary optimization in evolvable hardware. Genetic Programming and Evolvable Machines, vol. 12, no. 3, pp. 305-327. ISSN 1389-2576.
Czech title
Formální verifikace kandidátních řešení pro evoluční optimalizaci v evolvable hardware
Type
journal article
Language
english
Authors
URL
Keywords
genetic programming, circuit optimization, SAT solver, evolvable hardware
Abstract

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.
Published
2011
Pages
305-327
Journal
Genetic Programming and Evolvable Machines, vol. 12, no. 3, ISSN 1389-2576
Publisher
Springer Verlag
DOI
BibTeX
@ARTICLE{FITPUB9712,
   author = "Zden\v{e}k Va\v{s}\'{i}\v{c}ek and Luk\'{a}\v{s} 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",
   doi = "10.1007/s10710-011-9132-7",
   language = "english",
   url = "https://www.fit.vut.cz/research/publication/9712"
}
Files
Back to top