Publication detail

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

VAŠÍČEK, Z. SEKANINA, L.

Original Title

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

Type

journal article in Web of Science

Language

English

Original 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.

Keywords

genetic programming, circuit optimization, SAT solver, evolvable hardware

Authors

VAŠÍČEK, Z.; SEKANINA, L.

RIV year

2011

Released

15. 7. 2011

ISBN

1389-2576

Periodical

Genetic Programming and Evolvable Machines

Year of study

12

Number

3

State

United States of America

Pages from

305

Pages to

327

Pages count

23

URL

https://www.fit.vut.cz/research/publication/9712/

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/"
}

Documents

vasicek_sekanina_genp2011.pdf