Publikation
Polynomial formal verification parameterized by cutwidth properties of a circuit using Boolean satisfiability
Luca Müller; Rolf Drechsler
In: Microprocessors and Microsystems (MICPRO), Vol. 118, Elsevier, 2025.
Zusammenfassung
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.