Skip to main content Skip to main navigation


Polynomial Formal Verification of Adder Circuits Using Answer Set Programming

Mohamed Nadeem; Jan Kleinekathöfer; Rolf Drechsler
In: Reed-Muller Workshop (RM2023). Reed-Muller Workshop (RM-2023), May 24, Matsue City, Japan, 2023.


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. In this paper, we present our approach for PFV of arithmetic circuits. A divide and conquer approach is used to split the circuit into subgraphs. Each subgraph is verified using Answer Set Programming (ASP), a model based reasoning technique. For circuits with limited cutwidth, the verification process can be executed efficiently. Exemplarily, we use adder circuits to demonstrate the applicability of the method. Furthermore, the time complexity of the approach is analyzed and it is proven that the verification of several adder architectures is executable in linear time. Those theoretical findings are backed by experiments including different adder architectures with up to 10k bit wide inputs.