Functional Verification of High Performance Adders in COQ
Keyword(s):
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.
2006 ◽
Vol 53
(5)
◽
pp. 1078-1088
◽
2008 ◽
pp. 265-283
◽
Keyword(s):