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.
| Identifer | oai:union.ndltd.org:nusl.cz/oai:invenio.nusl.cz:363841 |
| Date | January 2017 |
| Creators | Matyáš, Jiří |
| Contributors | Lengál, Ondřej, Češka, Milan |
| Publisher | Vysoké učení technické v Brně. Fakulta informačních technologií |
| Source Sets | Czech ETDs |
| Language | Czech |
| Detected Language | English |
| Type | info:eu-repo/semantics/masterThesis |
| Rights | info:eu-repo/semantics/restrictedAccess |
Page generated in 0.0019 seconds