Daniela Kaufmann,
"Formal Verification of Multiplier Circuits using Computer Algebra"
, in Fachbereich Informatik, Johannes Kepler University, Linz, 3-2020
Original Titel:
Formal Verification of Multiplier Circuits using Computer Algebra
Sprache des Titels:
Englisch
Original Kurzfassung:
Digital circuits are extensively used in computers and digital systems because they areable to represent models for various digital components and arithmetic operations. Asubclass of digital circuits are arithmetic circuits, which are used in computer circuits toperform Boolean algebra. It is of high importance to guarantee that these circuits arecorrect 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 respectto a certain specification. However, arithmetic circuits, and most prominently gate-levelmultipliers, impose a challenge for existing verification techniques and in practice stillrequire substantial manual effort. Approaches based on satisfiability checking (SAT) oron decision diagrams seem to be unable to solve this problem in a reasonable amount oftime. In principle, theorem provers in combination with SAT are able to verify industrialmultipliers, but this approach cannot be applied fully automated. Currently, the mosteffective automated reasoning technique relies on computer algebra. In this approachthe 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 returnszero if and only if the circuit is correct.In this thesis we give a rigorous formalization of this reasoning method includingsoundness and completeness arguments, first for polynomial rings, where the coefficientdomain is a field and later for more general polynomial rings. As a consequence we areable to verify not only large unsigned and signed integer multipliers very efficiently, butare also able to verify truncated multipliers. We further improve the algebraic verificationapproach and present a new incremental column-wise verification algorithm, whichsplits the verification problem into smaller more manageable sub-problems and thusdoes not require to consider a full word-level specification. We present preprocessingapproaches based on variable elimination in order to rewrite and hence simplify theimplied 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 replacecomplex adders by equivalent adders, which can be verified using computer algebra.We develop a dedicated reduction engine, which is able to apply adder substitution andverifies large multipliers of input bit-width 2048 fully automated.Nonetheless, the verification process might not be error-free. Generating and automat-ically checking proofs independently increases confidence in the results of automatedreasoning tools. We show how the polynomial calculus can be instantiated to yield apractical algebraic calculus (PAC). Proofs in this format can be obtained as a by-productof verifying multiplier circuits in our reduction engine and can be checked with ourindependent proof checking tools.
Forschungs-