Detail publikace

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.
Název česky
Formální verifikace kandidátních řešení pro evoluční optimalizaci v evolvable hardware
Typ
článek v časopise
Jazyk
anglicky
Autoři
Vašíček Zdeněk, doc. Ing., Ph.D. (UPSY)
Sekanina Lukáš, prof. Ing., Ph.D. (UPSY)
URL
Klíčová slova

genetic programming, circuit optimization, SAT solver, evolvable hardware

Abstrakt

V této práci je využita formální verifikace pro zkrácení doby evaluace kandidátních řešení při evolučním návrhu a optimalizaci číslicových obvodů. Navržená metoda předpokládá, že existuje plně funkční řešení, u kterého se snažíme redukovat počet hradel. Evoluce probíhá pomocí kartézského genetického programování, které využívá SAT solver pro rozhodnutí, zda je kandidátní řešení plně funkční. Navržená metoda umožňuje optimalizovat obvody, které mají desítky vstupů a sestávají z tisíců hradel. Pro testovací obvody ze sady LGSynth93 došlo v průměru ke snížení počtu hradel o 37,8% v porovnání s konvenční metodou SIS.  

Rok
2011
Strany
305–327
Časopis
Genetic Programming and Evolvable Machines, roč. 12, č. 3, ISSN 1389-2576
DOI
10.1007/s10710-011-9132-7
UT WoS
000292814000007
EID Scopus
2-s2.0-80055089068
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/"
}
Nahoru