Functional verification of high performance adders in C OQ

Addition arithmetic design plays a crucial role in high performance digital systems. the paper proposes a systematic method to formalize and verify adders in a formal proof assistant coq. the proposed approach succeeds in formalizing the gate-level implementations and verifying the functional correctness of the most important adders of interest in industry,in a faithful,scalable,and modularized way. the methodology can be extended to other adder architectures as well. © 2014 qian wang et al.