Title :
Formalization of a Parameterized Parallel Adder Within the Coq Theorem Prover
Abstract :
This paper describes a new advancement in theorem proving based formal verification: a formalization of a parameterized parallel prefix adder developed in the proof assistant Coq.
Keywords :
Adders; Books; Digital arithmetic; Equations; Formal verification; Hardware; Logic circuits; Logic design; Prototypes; Switches; Adder circuits; computer arithmetic; formal method;
Journal_Title :
Computer-Aided Design of Integrated Circuits and Systems, IEEE Transactions on
DOI :
10.1109/TCAD.2009.2034346
