论文标题
Polyadd：加法电路的多项式正式验证
PolyAdd: Polynomial Formal Verification of Adder Circuits
论文作者
论文摘要
只有通过正式验证方法才能确保功能正确性。尽管对于许多电路，可以快速验证，但在其他情况下，方法失败了。通常，由于基础验证问题是NP核算，因此无法给出有效的算法。在本文中，我们证明，对于不同类型的加法电路，可以根据BDD确保多项式验证。虽然已知添加的输出函数是多项式界限的，但我们在以下显示可以在多项式时间内执行整个施工过程。对于简单的波纹携带加法器，也显示了这一点，但也适用于有条件的加法器和随身携带的快速外观加法器等快速加法器。证明了有关加法功能的属性，并且描述了多项式验证的核心原理，也可以将其扩展到其他类别的函数和电路实现。
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.
