Thesis Details
Využití přibližné ekvivalence při návrhu přibližných obvodů
This thesis is concerned with the utilization of formal verification techniques in the design of the functional approximations of combinational circuits. We thoroughly study the existing formal approaches for the approximate equivalence checking and their utilization in the approximate circuit development. We present a new method that integrates the formal techniques into the Cartesian Genetic Programming. The key idea of our approach is to employ a new search strategy that drives the evolution towards promptly verifiable candidate solutions. The proposed method was implemented within ABC synthesis tool. Various parameters of the search strategy were examined and the algorithm's performance was evaluated on the functional approximations of multipliers and adders with operand widths up to 32 and 128 bits respectively. Achieved results show an unprecedented scalability of our approach.
Approximate circuits, relaxed equivalence, evolutionary circuit design, Cartesian genetic programming, ABC.
Čadík Martin, doc. Ing., Ph.D. (DCGM FIT BUT), člen
Češka Milan, doc. RNDr., Ph.D. (DITS FIT BUT), člen
Janoušek Jan, doc. Ing., Ph.D. (FIT CTU), člen
Orság Filip, Ing., Ph.D. (DITS FIT BUT), člen
Zachariášová Marcela, Ing., Ph.D. (DCSY FIT BUT), člen
@mastersthesis{FITMT19459,
author = "Ji\v{r}\'{i} Maty\'{a}\v{s}",
type = "Master's thesis",
title = "Vyu\v{z}it\'{i} p\v{r}ibli\v{z}n\'{e} ekvivalence p\v{r}i n\'{a}vrhu p\v{r}ibli\v{z}n\'{y}ch obvod\r{u}",
school = "Brno University of Technology, Faculty of Information Technology",
year = 2017,
location = "Brno, CZ",
language = "czech",
url = "https://www.fit.vut.cz/study/thesis/19459/"
}