PolyAdd: Polynomial Formal Verification of Adder Circuits

TL;DR

This paper demonstrates that polynomial-time formal verification of certain adder circuits is possible using BDDs, providing a practical approach for circuits where traditional methods are inefficient due to NP-completeness.

Contribution

It proves that polynomial verification can be achieved for various adder circuits using BDDs, extending the scope of efficient formal verification methods.

Findings

Polynomial verification is feasible for Ripple Carry, Conditional Sum, and Carry Look Ahead Adders.

The entire construction process for these adders can be carried out in polynomial time.

Properties of adder functions are formally proven within this framework.

Abstract

Only by formal verification approaches functional correctness can be ensured. While for many circuits fast verification is possible, in other cases the approaches fail. In general no efficient algorithms can be given, since the underlying verification problem is NP-complete. In this paper we prove that for different types of adder circuits polynomial verification can be ensured based on BDDs. While it is known that the output functions for addition are polynomially bounded, we show in the following that the entire construction process can be carried out in polynomial time. This is shown for the simple Ripple Carry Adder, but also for fast adders like the Conditional Sum Adder and the Carry Look Ahead Adder. Properties about the adder function are proven and the core principle of polynomial verification is described that can also be extended to other classes of functions and circuit realizations.