Detail publikace
Formal verification of candidate solutions for post-synthesis evolutionary optimization in evolvable hardware
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
Jazyk
en
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.
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",
annote="
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.",
address="NEUVEDEN",
chapter="76412",
doi="10.1007/s10710-011-9132-7",
edition="NEUVEDEN",
howpublished="online",
institution="NEUVEDEN",
number="3",
volume="12",
year="2011",
month="july",
pages="305--327",
publisher="NEUVEDEN",
type="journal article in Web of Science"
}