@phdthesis{Kaufmann-PhdThesis20,
title = {Formal Verification of Multiplier Circuits using Computer Algebra},
author = {Daniela Kaufmann},
url = {https://danielakaufmann.at/wp-content/uploads/2020/11/Kaufmann-PhD-Thesis-2020.pdf, Thesis},
year = {2020},
date = {2020-06-03},
address = {Linz, Austria},
school = {Johannes Kepler University},
abstract = {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.},
keywords = {},
pubstate = {published},
tppubtype = {phdthesis}
}