Incremental column-wise verification of arithmetic circuits using computer algebra

DOI10.1007/S10703-018-00329-2MaRDI QIDQ2225473zbMATH OpenOpenAlexDBLPWikidataFDO

Authors Daniela Kaufmann, Armin Biere, M. Kauers

Publication date 8 February 2021

Published in Formal Methods in System Design (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/s10703-018-00329-2

zbMATH Keywords

computer algebraarithmetic circuit verificationGröbner basis

Mathematics Subject Classification ID

Symbolic computation and algebraic computation (68W30) Specification and verification (program logics, model checking, etc.) (68Q60) Networks and circuits as models of computation; circuit complexity (68Q06)

Recommendations

• Rewriting environment for arithmetic circuit verification
• Polynomial formal verification of multipliers
• Automated and scalable verification of integer multipliers
• Using an induction prover for verifying arithmetic circuits

Cites work

• scientific article; zbMATH DE number 3930347 (Why is no real title available?)
• An Algebraic Approach for Proving Data Correctness in Arithmetic Data Paths
• An algorithm for finding the basis elements of the residue class ring of a zero dimensional polynomial ideal
• Computer arithmetic algorithms.
• Graph-Based Algorithms for Boolean Function Manipulation
• Simulating circuit-level simplifications on CNF
• Theory and Applications of Satisfiability Testing
• Verification of arithmetic circuits using binary moment diagrams

Cited in

(6)

• Polynomial formal verification of multipliers
• An Algebraic Approach for Proving Data Correctness in Arithmetic Data Paths
• Formal Verification of Integer Multiplier Circuits Using Algebraic Reasoning: A Survey
• Verification of Galois field based circuits by formal reasoning based on computational algebraic geometry
• Practical algebraic calculus and Nullstellensatz with the checkers Pacheck and Pastèque and Nuss-Checker
• Rewriting environment for arithmetic circuit verification

Describes a project that uses

Uses Software

• YalSAT
• AIGER
• Lingeling
• Splatz
• Treengeling
• ABC
• Plingeling
• SINGULAR
• MiniSat
• Mathematica

This page was built for publication: Incremental column-wise verification of arithmetic circuits using computer algebra

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