Polynomial Formal Verification exploiting Constant Cutwidth
Mohamed Nadeem, Jan Kleinekathöfer, Rolf Drechsler · 2023
Only formal methods can guarantee the correctness of a circuit, but are usually very time and memory consuming. Therefore, efficient formal verification is key in the design of complex circuits. Many verification techniques have been introduced, which mostly fail to give bounds for the time complexity of the verification process. To overcome this issue, Polynomial Formal Verification (PFV) was introduced. This paper introduces a novel approach to PFV of circuits, by leveraging the concept of constant cutwidth. We divide the circuit into subgraphs, one for every output. This makes the verification of every subgraph only dependent on the cutwidth of the circuit and independent of the bitwidth. One main problem we solve is the passing of information between those subgraphs. The approach enables formal verification in linear time for circuits with constant cutwidth.