Formal Verification of Integer Multiplier Circuits using Algebraic Reasoning - A Survey
Sprache des Vortragstitels:
14th International Workshop on Boolean Problems, Bremen - online
Sprache des Tagungstitel:
Digital circuits are extensively used in computers and digital systems andit is of high importance to guarantee that these circuits are correct in order to preventissues like the famous Pentium FDIV bug. Formal verification can be used to derivethe correctness of a given circuit with respect to a certain specification. Howeverarithmetic circuits, and most prominently multipliers, impose a challenge for existingverification techniques. Currently one of the most effective techniques is based onalgebraic reasoning. In this approach the circuit is modeled as a set of pseudo-Booleanpolynomials and the word-level specification is reduced by a Gröbner basis, whichis implied by the polynomial representation of the circuit. The circuit is correct ifand only if the final result is zero. Nonetheless the verification process might not beerror-free. Generating and automatically checking proofs independently increasesconfidence in the results of automated reasoning tools. In this paper we surveythe current state of the art of this work. We give an overview over recent solvingtechniques, available benchmarks, and include a comprehensive evaluation.
Sprache der Kurzfassung:
Hauptvortrag / Eingeladener Vortrag auf einer Tagung