This work has been supported by the National Science Foundation of China Grant 61272002, the Tsinghua National Laboratory for Information Science and Technology (TNList) Cross-discipline Foundation 2011-9, the Major Research plan of the National Natural Science Foundation of China Grant 91218302, and the National Basic Research Program of China (973 Program) Grant 2010CB328003.
Journal of Applied Mathematics
Automatic theorem proving, calcul construction, COQ
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.
Qian Wang, Xiaoyu Song, Ming Gu, and Jiaguang Sun, “Functional Verification of High Performance Adders in COQ,” Journal of Applied Mathematics, vol. 2014, Article ID 197252, 9 pages, 2014.