Back
2025INF007
Doctoral thesis

Approximate computing via effective SMT-based logic synthesis

  • 2025

PhD: Università della Svizzera italiana

Approximate computing
Approximate logic synthesis
SMT solver
Worst-case error
English 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-LargeScale 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 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 four synergistic contributions, each advancing the state-of-the-art in their own way. 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 SMTbased 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 shown on many arithmetic circuits. To enable XPAT to be applicable to larger circuits, we develop SubXPAT, an iterative variant that decomposes the circuit into smaller submodules, applies XPAT locally, and recomposes the results. SubXPAT retains XPAT’s guarantees while enabling approximation of larger designs. Our final contribution, Shared XPAT (XPAT-S), rethinks the template structure to explicitly optimize product-term sharing across outputs. Our original template treats 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.
Collections
Language
  • English
Classification
Computer science and technology
License
License undefined
Open access status
green
Identifiers
Persistent URL
https://n2t.net/ark:/12658/srd1332334
Statistics
Document views: 14 File downloads:
  • 2025INF007.pdf: 33