Formal Verification of Integer Multiplier Circuits using Computer Algebra
Sprache des Vortragstitels:
Englisch
Original Tagungtitel:
14th International Workshop on Boolean Problems, Bremen - online
Sprache des Tagungstitel:
Englisch
Original Kurzfassung:
Digital circuits are extensively used in computers and digital systems and it is of high importance to guarantee that these circuits are correct in order to prevent issues like the famous Pentium FDIV bug. Formal verification can be used to derive the correctness of a given circuit with respect to a certain specification. However arithmetic circuits, and most prominently gate-level multipliers, impose a challenge for existing verification techniques. Approaches which purely rely on SAT solving or on decision diagrams seem to be unable to solve this problem in a reasonable amount of time. Currently one of the most effective techniques is based on algebraic reasoning. In this approach the circuit is modeled as a set of pseudo-Boolean polynomials and the word-level specification is reduced by a Gröbner basis which is implied by the polynomial representation of the circuit. However parts of the multiplier, i.e., final stage adders, are hard to verify using computer algebra. In our approach we combine SAT and computer algebra to substantially improve automated verification of integer multipliers. Complex final stage adders are detected and replaced by simple adders. The correctness of the replacement is verified by SAT solvers and the simplified multiplier is verified by computer algebra techniques. Nonetheless the verification process might not be error-free. Generating and automatically checking proofs independently increases confidence in the results of automated reasoning tools. In order to validate verification results we show how proof certificates can be obtained as a by-product of verifying multiplier circuits in our reduction engine, which can be checked with our independent proof checker tool.
Sprache der Kurzfassung:
Englisch
Vortragstyp:
Hauptvortrag / Eingeladener Vortrag auf einer Tagung
Forschungs-