Publication
Cutwidth Decomposition on Circuit-AIGs: Taming Verification Complexity of Arithmetic Circuits
Luca Müller; Mohamed Nadeem; Rolf Drechsler
In: 27th International Symposium on Quality Electronic Design. International Symposium on Quality Electronic Design (ISQED-2026), April 8-10, San Francisco, USA, 2026.
Abstract
erification is an essential step in modern Very
Large Scale Integration (VLSI) Computer-Aided Design (CAD) to
avoid errors in circuits with ever-increasing complexity. Formal
verification methods are gaining traction in both academia and
industry, as they can ensure the complete correctness of a design.
However, they come with the tradeoff of potentially exponential
time and space complexity.
This work aims to tame this complexity, establishing a formal
verification approach based on the cutwidth decomposition on
Circuit-And-Inverter Graphs (AIGs), which can make use of
different verification techniques like Boolean Satisfiability (SAT)
and Answer Set Programming (ASP). For circuits with a constant
cutwidth, a linear verification time is formally proven. The
practical applicability of this approach to arithmetic circuits
is demonstrated by experimental evaluation of three Arithmetic
Logic Units (ALUs), showing that the theoretical bounds hold
in practice and that our approach can outperform other formal
verification approaches found in open-source software