|
|
Functional verification of high performance adders in C OQ
|
|
|
|
|
نویسنده
|
wang q. ,song x. ,gu m. ,sun j.
|
منبع
|
journal of applied mathematics - 2014 - دوره : 2014 - شماره : 0
|
چکیده
|
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.
|
|
|
آدرس
|
school of software,tsinghua university, China, department of ece,portland state university,portland, United States, school of software,tsinghua university, China, school of software,tsinghua university, China
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Authors
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|