Multi-Metric SMT-Based Evaluation of Worst-Case-Error for Approximate Circuits.

Approximate computing has become a popular technique for leveraging the error resilience of applications that do not require full accuracy. By allowing for small and controlled errors, it is possible to reduce the area and power consumption of circuits. However, one of the main challenges in approximate computing is validating the design to ensure that it adheres to the error constraints. To address this issue, SMT/SAT solvers have been employed to evaluate errors, as their efficiency enables them to produce valid results, unlike statistical methods like Monte Carlo sampling. In this paper, we introduce a novel SMT-based algorithm for error evaluation that can be utilized for any approximate circuit and for any worst-case error metric. The algorithm leverages the solver's output to improve error evaluation efficiency and explore the error space monotonically. We demonstrate how this approach outperforms other error-evaluation techniques used in current research.