Challenges in Verifying Arithmetic Circuits Using Computer Algebra

Description

Verifying arithmetic circuits is an important problem which still requires considerable manual effort. For instance multipliers are considered difficult to verify. The currently most effective approach for arithmetic circuit verification 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 specification 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.

Period	28 Sept 2017
Event title	19th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing
Event type	Conference
Location	RomaniaShow on map