Approximate Computing via Effective SMT-Based Logic Synthesis

You are cordially invited to attend the PhD Dissertation Defence of Morteza Rezaalipour on Friday 6 June 2025 at 12:45 in room D1.15

Abstract:
The relentless progress of semiconductor technology, historically governed by Moore's Law and Dennard scaling, is now facing fundamental physical and economic limitations. As transistor densities approach atomic scales, power dissipation, manufacturing variability, and diminishing returns in performance gains have made energy efficiency a critical challenge in Very-Large-Scale Integration (VLSI) design. This is particularly evident in resource-constrained domains such as mobile IoT devices, embedded systems, and edge computing, where applications like digital signal processing (DSP), multimedia encoding, and machine learning dominate. These applications exhibit a key property: they are inherently error-resilient, either due to noise in input data, redundancy in computations, or the limitations of human perception. This resilience has motivated the emergence of Approximate Computing (AC) as a disruptive design paradigm, where controlled reductions in computational accuracy are traded for significant improvements in power consumption, silicon area, and latency, with minimal impact on perceived output quality. Despite its potential, the widespread adoption of AC faces two major bottlenecks. First, existing methods for Worst-Case Error (WCE) analysis -- a critical metric for quantifying approximation bounds -- are either computationally intractable (exhaustive simulation) or unreliable (statistical sampling). Second, Approximate Logic Synthesis (ALS) techniques for generating approximate circuits often rely on heuristic-driven transformations, leading to suboptimal area-precision trade-offs. This dissertation addresses the challenges arising from these bottlenecks through three synergistic contributions, each advancing the state-of-the-art in AC design and analysis. Our first contribution, ErrorEval, is a novel framework for exact WCE computation in combinational circuits. Unlike prior approaches -- such as the naive exhaustive search (infeasible beyond 16-bit inputs) and Monte Carlo sampling (which cannot guarantee error bounds) -- ErrorEval formulates WCE computation as a constrained optimization problem suitable for Satisfiability Modulo Theories (SMT) solving. By strategically pruning the search space and prioritizing Satisfiable (SAT) solver calls over costly Unsatisfiable (UNSAT) queries, ErrorEval achieves two to three orders of magnitude speedup over state-of-the-art tools. To bridge the gap between error analysis and synthesis, we next introduce XPAT, an SMT-based Boolean rewriting methodology for the generation of area-optimized approximate circuits. XPAT's innovation lies in its parametrical template, which guides the SMT solver to systematically explore the design space. By tuning template parameters, e.g., maximum literals per product term, XPAT generates approximate circuits that strictly adhere to user-defined error constraints while minimizing area. Compared to state-of-the-art ALS tools, XPAT reduces area occupation by 15-40% for the same error tolerance, as demonstrated on many arithmetic circuits. Our final contribution, Shared XPAT (XPAT-S), rethinks the template structure to explicitly optimize product-term sharing across outputs. Traditional SOP templates treat each output independently, leading to redundant exploration of structurally similar (and area-inefficient) solutions. XPAT-S introduces shared-product parameters that steer the SMT solver toward globally optimal approximations that maximize circuit reuse. Experiments show that XPAT-S outperforms both non-shared XPAT and the state-of-the-art work by 12-30% in area savings for arithmetic circuits, without compromising precision. Together, these contributions provide a cohesive framework for scalable, rigorous, and automation-friendly AC. ErrorEval ensures reliability by certifying error bounds; XPAT and its variants enable area-efficient synthesis with formal guarantees; and the notion of the shared-template opens new directions for template-driven optimization. By integrating these contributions into Electronic Design Automation (EDA) flows, this work paves the way for AC's adoption in safety-critical yet resilient domains, from energy-efficient AI accelerators to real-time embedded vision systems.

Dissertation Committee:
- Prof. Laura Pozzi, Università della Svizzera italiana, Switzerland (Research Advisor)
- Prof. Rodrigo Benedito Otoni, Università della Svizzera italiana, Switzerland (Research co-Advisor)
- Prof. Cesare Alippi, Università della Svizzera italiana, Switzerland (Internal Member)
- Prof. Carlo Alberto Furia, Università della Svizzera italiana, Switzerland (Internal Member)
- Prof. Akash Kumar, Ruhr University Bochum, Germany (External Member)
- Prof. Marco Platzner, Paderborn University, Germany (External Member)