Formal Verification of Multiplier Circuits using Computer Algebra

Digitale Schaltungen modellieren digitale Komponenten und arithmetische Operationen und sind daher ein essenzieller Bestandteil in Computern und digitalen Systemen. Arithmetische Schaltungen sind ein Spezialfall von digitalen Schaltungen und werden in Computern genutzt um Boole'sche Algebra zu implementieren. Es ist äußerst wichtig, dass diese Schaltungen korrekt sind, um Fehler wie zum Beispiel den berühmten Pentium-FDIV-Bug zu vermeiden. Mithilfe von formaler Verifikation kann man feststellen, ob eine gegebene Schaltung ihrer Spezifikation entspricht. Jedoch sind arithmetische Schaltungen, insbesondere Multiplizierer auf Gatterebene, eine Herausforderung für bestehende Verfikationstechniken. Techniken basierend auf dem Entscheidungsproblem der Aussagenlogik (SAT) oder auf Entscheidungsdiagrammen sind nicht der Lage Multiplizerer effizient zu verifizieren. Theorem Prover in Kombination mit SAT können die Korrektheit komplexer Multiplizerer beweisen, allerdings ist diese Methode nicht vollautomatisch anwendbar. Die zurzeit erfolgreichste Beweistechnik basiert auf Computeralgebra. In dieser Methode wird die Schaltung mithilfe von Polynomen als eine Gröbner Basis modelliert. Die Spezifikation, ebenfalls als Polynom kodiert, wird mittels der Gröbner Basis reduziert. Diese Reduktion liefert das Ergebnis null genau dann, wenn die Schaltung ihrer Spezifikation entspricht. In dieser Thesis wird dieses Problem einfach, aber präzise formalisiert und Korrektheit und Vollständigkeit wird zuerst für Polynomringe über Körper und nachfolgend für allgemeinere Ringe bewiesen. Dadurch sind wir in der Lage nicht nur vorzeichenlose und -behaftete Integer-Multiplizierer, sondern auch abgeschnittene Multiplizierer zu verifizieren. Wir verbessern diese algebraische Beweistechnik und präsentieren einen neuen inkrementellen Algorithmus, der es erlaubt, das Verifikationsproblem in kleinere Teilprobleme aufzuspalten. Weiters präsentieren wir Vorbearbeitungstechniken, welche Variablen von der Gröbner Basis eliminieren und daher die Polynomdarstellung der Schaltung vereinfachen. Jedoch können gewisse Bestandteile von Multiplizierern, genauer gesagt Addierer, nicht sehr effizient mit Computeralgebra verifiziert werden. Wir nutzen SAT, um diese komplexen Addierer mit einfachen äquivalenten Addierern zu ersetzen. Wir implementieren ein dediziertes Verifikationstool und können Multiplizierer mit Bitbreite 2048 vollautomatisch verifizieren. Nichtsdestotrotz kann das Verifikationsprogramm Fehler enthalten. Daher werden Beweiszertifikate generiert, welche von eigenständigen Beweischeckern auf Richtigkeit überprüft werden. Wir instanziieren den abstrakten ``Polynomial Calculus'' und formalisieren das Beweiskalkül PAC. PAC Beweise können in unserem Verifikationstool erzeugt und mit unseren eigenständigen Beweischeckern überprüft werden.Digital circuits are extensively used in computers and digital systems because they are able to represent models for various digital components and arithmetic operations. A subclass of digital circuits are arithmetic circuits, which are used in computer circuits to perform Boolean algebra. 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 and in practice still require substantial manual effort. Approaches based on satisfiability checking (SAT) or on decision diagrams seem to be unable to solve this problem in a reasonable amount of time. In principle, theorem provers in combination with SAT are able to verify industrial multipliers, but this approach cannot be applied fully automated. Currently, the most effective automated reasoning technique relies on computer algebra. In this approach the word-level specification, modeled as a polynomial, is reduced by a Gröbner basis, which is implied by the gate-level representation of the circuit. The reduction returns zero if and only if the circuit is correct. In this thesis we give a rigorous formalization of this reasoning method including soundness and completeness arguments, first for polynomial rings, where the coefficient domain is a field and later for more general polynomial rings. As a consequence we are able to verify not only large unsigned and signed integer multipliers very efficiently, but are also able to verify truncated multipliers. We further improve the algebraic verification approach and present a new incremental column-wise verification algorithm, which splits the verification problem into smaller more manageable sub-problems and thus does not require to consider a full word-level specification. We present preprocessing approaches based on variable elimination in order to rewrite and hence simplify the implied Gröbner basis. However, certain parts of a multiplier, namely final-stage adders, are hard to verify using computer algebra. In our approach we use SAT to replace complex adders by equivalent adders, which can be verified using computer algebra. We develop a dedicated reduction engine, which is able to apply adder substitution and verifies large multipliers of input bit-width 2048 fully automated. Nonetheless, the verification process might not be error-free. Generating and automatically checking proofs independently increases confidence in the results of automated reasoning tools. We show how the polynomial calculus can be instantiated to yield a practical algebraic calculus (PAC). Proofs in this format can be obtained as a by-product of verifying multiplier circuits in our reduction engine and can be checked with our independent proof checking tools.eingereicht von Dipl.-Ing. Daniela Kaufmann, BscUniversität Linz, Dissertation, 2020(VLID)494987