Late Breaking Results: Polynomial Formal Verification of Fast Adders

Alireza Mahzoon, Rolf Drechsler

In: Design Automation Conference (DAC). Design Automation Conference (DAC-2021) December 5-9 San Francisco CA United States 2021.


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.

Deutsches Forschungszentrum für Künstliche Intelligenz
German Research Center for Artificial Intelligence