Využití formálních metod v přibližném počítání

Applications of Formal Methods in Approximate Computing

As the Moore's Law ceases to hold, the ever increasing demand for high performance and lower power computer systems leads to the emergence of novel alternative computing paradigms. One of these paradigms is the so called approximate computing - a technique aiming to increase the efficiency of computations by introducing some errors into the computed results. This paradigm is mainly applicable in the error resilient applications - a class of applications where the absolute precision of the result is not critical, the most prominent of which include neural networks, multimedia and signal processing, or data mining. Naturally, techniques for approximate computing developed at various levels of the computing system architectures - the hardware, memory, operating system and software levels.This thesis aims at the search-based design techniques for approximate arithmetic circuits. Circuit approximation is a crucial domain of approximate computing, as the approximate circuits can serve as the basic building blocks for larger systems and applications. We focus on the automated search-based approaches, which often work iteratively: in each iteration they 1) create the approximate candidates (synthesizer component), 2) evaluate their error with respect to the correct solution (analyser component). To successfully approximate complex circuits, the search based approaches usually need to perform a high number of iterations. Therefore, efficient synthesizer and analyser components are essential.In order to improve the performance of the approximation process, we employ formal verification methods in both the synthesizer and analyser components of a circuit design loop implemented using Cartesian Genetic Programming. The evaluator component is accelerated with the utilisation of a novel construction of the specialised intermediate circuits called the approximation miters. The miters allow us to translate the error quantification procedure to a decision problem that can be evaluated using a SAT solver. We further enhance the performance of the search algorithm by integrating it with a verifiability driven strategy that guides the search towards promptly verifiable circuits and thus performs a significantly higher number of iterations, leading to a better quality of the final approximate solutions. We also improve the performance of the synthesizer component using an integration of satisfiability based local sub-circuit optimisation with the search algorithm. This effectively allows the search strategy to escape local optima and to further  improve the quality of the solution. Finally, we propose a novel mutation operator tailored to circuit approximation that improves the overall performance of the approximation process.The research presented in this thesis fundamentally improves the capabilities of the current search-based circuit approximation techniques and thus allows us to design approximate circuits with large bit-widths and complex structure (e.g. 32-bit multipliers or 128-bit adders) with the best known trade-offs between the power consumption and approximation error.

Formal verification, approximate computing, approximate arithmetic circuits, Cartesian Genetic Programming, approximate equivalence checking.

MATYÁŠ, Jiří. Využití formálních metod v přibližném počítání. Brno, 2023. Ph.D. Thesis. Brno University of Technology, Faculty of Information Technology. 2024-02-14. Supervised by Češka Milan. Available from: https://www.fit.vut.cz/study/phd-thesis/1418/