Armin Biere, Manuel Kauers, Daniela Ritirc,
"Challenges in Verifying Arithmetic Circuits Using Computer Algebra"
: Proc. 19th International Symposium on Symbolic and Numeric Algorithms for Scienti?c Computing, 2017
Original Titel:
Challenges in Verifying Arithmetic Circuits Using Computer Algebra
Sprache des Titels:
Englisch
Original Buchtitel:
Proc. 19th International Symposium on Symbolic and Numeric Algorithms for Scienti?c Computing
Original Kurzfassung:
Verifying arithmetic circuits is an important problem which still requires considerable manual effort. For instance multipliers are considered dif?cult to verify. The currently most effective approach for arithmetic circuit veri?cation uses computer algebra. In this approach the circuit is modeled as a set of pseudo-boolean polynomials and it is checked if the given word-level speci?cation is implied by the circuit polynomials. For this purpose the theory of Gr¨obner bases is used. In this paper we givea summary oftwo recent paperson this work.We reword the theory and illustrate the results of these papers by examples. We also present a new technical theorem which allows to rewrite local parts of the Gr¨obner basis. Rewriting the Gr¨obner basis has tremendous effect on computation time.
Forschungs-