MUSCAT: MUS-based Circuit Approximation Technique
Linus Witschena, Tobias Wiersemab, Matthias Artmannc and Marco Platznerd
Paderborn University, Germany
awitschen@mail.upb.de
bwiersema@mail.upb.de
cmartmann@mail.upb.de
dplatzner@mail.upb.de
ABSTRACT
Many applications show an inherent resiliency against inaccuracies and errors in their computations. The design paradigm approximate computing exploits this fact by trading off the application’s accuracy against a target metric, e.g., hardware area. This work focuses on approximate computing on the hardware level, where approximate logic synthesis seeks to generate approximate circuits under user-defined quality constraints.
We propose the novel approximate logic synthesis method MUSCAT to generate approximate circuits which are valid-byconstruction. MUSCAT inserts cutpoints into the netlist to employ the commonly-used concept of substituting connections between gates by constant values, which offers potential for subsequent logic minimization. MUSCAT’s novelty lies in utilizing formal verification engines to identify minimal unsatisfiable subsets. These subsets determine a maximal number of cutpoints that can be activated together without resulting in a violation against the userdefined quality constraints. As a result, MUSCAT determines an optimal solution w.r.t. the number of activated cutpoints while providing a guarantee on the quality constraints.
We present the method and experimentally compare MUSCAT’s open-source implementation to AIG rewriting and components from the EvoApproxLib.We show that our method improves upon these state-of-the-art methods by achieving up to 80% higher savings in circuit area at typically much lower computation times.
Keywords: Approximate Computing, Formal Verification, Approximate Logic Synthesis, Approximate Circuit Synthesis, Minimal Unsatisfiable Subsets.
