  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.
