Detail publikace

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

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

Originální název

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

Typ

článek v časopise ve Web of Science, Jimp

Jazyk

angličtina

Originální abstrakt

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.

Klíčová slova

genetic programming, circuit optimization, SAT solver, evolvable hardware

Autoři

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

Rok RIV

2011

Vydáno

15. 7. 2011

ISSN

1389-2576

Periodikum

Genetic Programming and Evolvable Machines

Ročník

12

Číslo

3

Stát

Spojené státy americké

Strany od

305

Strany do

327

Strany počet

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