Polynomial formal verification parameterized by cutwidth properties of a circuit using Boolean satisfiability

Verification is an essential step in the design process of microprocessors. A complete coverage can only be ensured by formal methods, which tend to have exponential runtimes in the general case. Polynomial Formal Verification addresses this issue, opening a research field focused on providing formal methods which can ensure 100% correctness along with predictable and manageable time and space complexity. In this work, two SAT-based verification approaches in the field of PFV are presented. For both the verification of the cutwidth decomposition on the Circuit-CNF and the verification of the cutwidth decomposition on the Circuit-AIG, it is proven that their time complexity is parameterized by their respective cutwidth. This enables the definition of a class of circuits with constant cutwidth, for which verification can be ensured in linear time. After the theoretical considerations, both approaches are experimentally evaluated on the case study of adder circuits, underlining the established theoretical bounds. Finally, both approaches are compared and their significance in the research filed of PFV are stated. • We present two formal verification approaches for which parameterized time complexity bounds can be established. • We identify a class of circuits for which a linear-time verification can be ensured. • We experimentally evaluate our approaches to show the viability for formal verification in practice.