Late Breaking Results: Polynomial Formal Verification of Fast Adders

Despite the recent success of formal verification methods, the computational complexity of most of them is still unknown. It raises serious questions regarding the scalability of the approaches. One of the most successful formal methods to prove the correctness of adders is Binary Decision Diagram (BDD)-based verification. It reports very good results for verification of different adder architectures. However, the computational complexity of BDD-based verification has not been yet fully investigated. In this paper, we calculate the complexity of verifying one of the fastest available adders, i.e., conditional sum adder. Then, we show that the verification of this architecture is possible in polynomial time. Finally, we confirm our theoretical calculations by experimental results.