Cargando…
Incremental column-wise verification of arithmetic circuits using computer algebra
Verifying arithmetic circuits and most prominently multiplier circuits is an important problem which in practice still requires substantial manual effort. The currently most effective approach uses polynomial reasoning over pseudo boolean polynomials. In this approach a word-level specification is r...
Autores principales: | , , |
---|---|
Formato: | Online Artículo Texto |
Lenguaje: | English |
Publicado: |
Springer US
2019
|
Materias: | |
Acceso en línea: | https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7691315/ https://www.ncbi.nlm.nih.gov/pubmed/33281299 http://dx.doi.org/10.1007/s10703-018-00329-2 |
_version_ | 1783614262492528640 |
---|---|
author | Kaufmann, Daniela Biere, Armin Kauers, Manuel |
author_facet | Kaufmann, Daniela Biere, Armin Kauers, Manuel |
author_sort | Kaufmann, Daniela |
collection | PubMed |
description | Verifying arithmetic circuits and most prominently multiplier circuits is an important problem which in practice still requires substantial manual effort. The currently most effective approach uses polynomial reasoning over pseudo boolean polynomials. In this approach a word-level specification is reduced by a Gröbner basis which is implied by the gate-level representation of the circuit. This reduction returns zero if and only if the circuit is correct. We give a rigorous formalization of this approach including soundness and completeness arguments. Furthermore we present a novel incremental column-wise technique to verify gate-level multipliers. This approach is further improved by extracting full- and half-adder constraints in the circuit which allows to rewrite and reduce the Gröbner basis. We also present a new technical theorem which allows to rewrite local parts of the Gröbner basis. Optimizing the Gröbner basis reduces computation time substantially. In addition we extend these algebraic techniques to verify the equivalence of bit-level multipliers without using a word-level specification. Our experiments show that regular multipliers can be verified efficiently by using off-the-shelf computer algebra tools, while more complex and optimized multipliers require more sophisticated techniques. We discuss in detail our complete verification approach including all optimizations. |
format | Online Article Text |
id | pubmed-7691315 |
institution | National Center for Biotechnology Information |
language | English |
publishDate | 2019 |
publisher | Springer US |
record_format | MEDLINE/PubMed |
spelling | pubmed-76913152020-12-02 Incremental column-wise verification of arithmetic circuits using computer algebra Kaufmann, Daniela Biere, Armin Kauers, Manuel Form Methods Syst Des Article Verifying arithmetic circuits and most prominently multiplier circuits is an important problem which in practice still requires substantial manual effort. The currently most effective approach uses polynomial reasoning over pseudo boolean polynomials. In this approach a word-level specification is reduced by a Gröbner basis which is implied by the gate-level representation of the circuit. This reduction returns zero if and only if the circuit is correct. We give a rigorous formalization of this approach including soundness and completeness arguments. Furthermore we present a novel incremental column-wise technique to verify gate-level multipliers. This approach is further improved by extracting full- and half-adder constraints in the circuit which allows to rewrite and reduce the Gröbner basis. We also present a new technical theorem which allows to rewrite local parts of the Gröbner basis. Optimizing the Gröbner basis reduces computation time substantially. In addition we extend these algebraic techniques to verify the equivalence of bit-level multipliers without using a word-level specification. Our experiments show that regular multipliers can be verified efficiently by using off-the-shelf computer algebra tools, while more complex and optimized multipliers require more sophisticated techniques. We discuss in detail our complete verification approach including all optimizations. Springer US 2019-02-26 2020 /pmc/articles/PMC7691315/ /pubmed/33281299 http://dx.doi.org/10.1007/s10703-018-00329-2 Text en © The Author(s) 2019 OpenAccessThis article is distributed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits unrestricted use, distribution, and reproduction in any medium, provided you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license, and indicate if changes were made. |
spellingShingle | Article Kaufmann, Daniela Biere, Armin Kauers, Manuel Incremental column-wise verification of arithmetic circuits using computer algebra |
title | Incremental column-wise verification of arithmetic circuits using computer algebra |
title_full | Incremental column-wise verification of arithmetic circuits using computer algebra |
title_fullStr | Incremental column-wise verification of arithmetic circuits using computer algebra |
title_full_unstemmed | Incremental column-wise verification of arithmetic circuits using computer algebra |
title_short | Incremental column-wise verification of arithmetic circuits using computer algebra |
title_sort | incremental column-wise verification of arithmetic circuits using computer algebra |
topic | Article |
url | https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7691315/ https://www.ncbi.nlm.nih.gov/pubmed/33281299 http://dx.doi.org/10.1007/s10703-018-00329-2 |
work_keys_str_mv | AT kaufmanndaniela incrementalcolumnwiseverificationofarithmeticcircuitsusingcomputeralgebra AT bierearmin incrementalcolumnwiseverificationofarithmeticcircuitsusingcomputeralgebra AT kauersmanuel incrementalcolumnwiseverificationofarithmeticcircuitsusingcomputeralgebra |