Verification 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.