Automated and scalable verification of integer multipliers

DOI10.1007/978-3-030-53288-8_23MaRDI QIDQ2225123zbMATH OpenOpenAlexFDO

Authors Mertcan Temel, Warren A. jun. Hunt, Anna Slobodová

Publication date 4 February 2021

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-030-53288-8_23

zbMATH Keywords

ACL2formal methodshardware verificationmultipliers

Mathematics Subject Classification ID

Mathematical problems of computer architecture (68M07) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Polynomial formal verification of multipliers
• Rewriting environment for arithmetic circuit verification
• scientific article; zbMATH DE number 1506311

Cited in

(13)

• Polynomial formal verification of multipliers
• Incremental column-wise verification of arithmetic circuits using computer algebra
• Functional verification of high performance adders in \textsc{Coq}
• Stability of the 7-3 compressor circuit for Wallace tree. I
• scientific article; zbMATH DE number 2102720 (Why is no real title available?)
• Formal Verification of Integer Multiplier Circuits Using Algebraic Reasoning: A Survey
• Scalable Techniques for Formal Verification
• Rewriting environment for arithmetic circuit verification
• Formal Verification of Structurally Complex Multipliers
• Formal verification of arithmetic RTL: translating Verilog to C++ to ACL2
• Verified implementation of an efficient term-rewriting algorithm for multiplier verification on ACL2
• Symbolic computer algebra for multipliers revisited - demonstrating the significance of order and phase optimization
• Divider verification using symbolic computer algebra and delayed don't care optimization: theory and practical implementation

Describes a project that uses

Uses Software

• GenMul
• RevSCA
• ACL2
• ABC
• Yosys
• multgen
• PolyCleaner

This page was built for publication: Automated and scalable verification of integer multipliers

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2225123)