Functional verification of high performance adders in \textsc{Coq} (Q2336214)

From MaRDI portal
scientific article
Language Label Description Also known as
English
Functional verification of high performance adders in \textsc{Coq}
scientific article

    Statements

    Functional verification of high performance adders in \textsc{Coq} (English)
    0 references
    0 references
    19 November 2019
    0 references
    Summary: 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 \textsc{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.
    0 references
    0 references
    0 references
    0 references
    0 references

    Identifiers

    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references