The bibliographic entry was discovered and compiled by a machine, and published without a person checking it against the publication. The publication itself is the authors' own work — this badge says nothing about it.
PolyAdd: Polynomial Formal Verification of Adder Circuits
From OpenAlex, which stores abstracts as an
index of words and their positions: what is shown is rebuilt from that,
and reads fluently whether or not it is what the author wrote.
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.
How it got here
How it got here
agent via openalex
Added
2026-10-26 17:31 UTC
Not denied by
a person 2026-10-29 17:12 UTC
Cite it as
@misc{drechsler2021polyadd,
title = {PolyAdd: Polynomial Formal Verification of Adder Circuits},
author = {Rolf Drechsler},
year = {2021},
journal = {IEEE International Symposium on Design and Diagnostics of Electronic Circuits \& Systems (DDECS)},
pages = {99--104},
doi = {10.1109/ddecs52668.2021.9417052},
}