Publication
Polynomial Formal Verification exploiting Constant Cutwidth
Mohamed Nadeem; Jan Kleinekathöfer; Rolf Drechsler
In: 34th International Workshop on Rapid System Prototyping (RSP). International Symposium on Rapid System Protoyping (RSP-2023), September 21, Hamburg, Germany, 2023.
Abstract
Only formal methods can guarantee the correctness of a circuit, but are usually very time and memory consuming. Therefore, efficient formal verification is a 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. As many different types of adders have a constant cutwidth, we can prove that those are verifiable in linear time. Those theoretical findings are backed by experiments including different adder architectures with up to 10k bit wide inputs