Publication Details

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

VAŠÍČEK, Z.; SEKANINA, L. Formal verification of candidate solutions for post-synthesis evolutionary optimization in evolvable hardware. Genetic Programming and Evolvable Machines, 2011, vol. 12, no. 3, p. 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
DOI
UT WoS
000292814000007
EID Scopus
BibTeX
@article{BUT76412,
  author="Zdeněk {Vašíček} and Lukáš {Sekanina}",
  title="Formal verification of candidate solutions for post-synthesis evolutionary optimization in evolvable hardware",
  journal="Genetic Programming and Evolvable Machines",
  year="2011",
  volume="12",
  number="3",
  pages="305--327",
  doi="10.1007/s10710-011-9132-7",
  issn="1389-2576",
  url="https://www.fit.vut.cz/research/publication/9712/"
}
Back to top