Detail publikačního výsledku

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

Anglický název

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

Druh

Článek WoS

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.

Anglický 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

Klíčová slova v angličtině

genetic programming, circuit optimization, SAT solver, evolvable hardware

Autoři

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

Rok RIV

2012

Vydáno

15.07.2011

ISSN

1389-2576

Periodikum

Genetic Programming and Evolvable Machines

Svazek

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

Dokumenty

vasicek_sekanina_genp2011