Logo des Repositoriums

Auflistung nach Autor:in "Kaufmann, Daniela"

1 - 2 von 2
  • Zeitschriftenartikel
    Formal verification of multiplier circuits using computer algebra
    (it - Information Technology: Vol. 64, No. 6, 2022) Kaufmann, Daniela
    Digital circuits are widely utilized in computers, because they provide models for various digital components and arithmetic operations. Arithmetic circuits are a subclass of digital circuits that are used to execute Boolean algebra. To avoid problems like the infamous Pentium FDIV bug, it is critical to ensure that arithmetic circuits are correct. Formal verification can be used to determine the correctness of a circuit with respect to a certain specification. However, arithmetic circuits, particularly integer multipliers, represent a challenge to current verification methodologies and, in reality, still necessitate a significant amount of manual labor. In my dissertation we examine and develop automated reasoning approaches based on computer algebra, where the word-level specification, modeled as a polynomial, is reduced by a Gröbner basis inferred by the gate-level representation of the circuit. We provide a precise formalization of this reasoning process, which includes soundness and completeness arguments and adds to the mathematical background in this field. On the practical side we present an unique incremental column-wise verification algorithm and preprocessing approaches based on variable elimination that simplify the inferred Gröbner basis. Furthermore, we provide an algebraic proof calculus in this thesis that allows obtaining certificates as a by-product of circuit verification in order to boost confidence in the outcomes of automated reasoning tools. These certificates can be efficiently verified with independent proof checking tools.
  • Konferenzbeitrag
    Formale Verifikation von Multiplizierern mit Computeralgebra
    (Ausgezeichnete Informatikdissertationen 2020, 2021) Kaufmann, Daniela
    Arithmetische Schaltungen werden in Prozessoren zur Implementierung von Boolescher Algebra genutzt. Aufgrund des weitreichenden Einsatzes von Prozessoren ist es äußerst wichtig, die Korrektheit dieser Schaltungen garantieren zu können, um Fehler wie den beru ̈hmten Pentium FDIV- Bug zu vermeiden. Mithilfe formaler Verifikation kann festgestellt werden, ob eine Schaltung ihrer gewünschten Spezifikation entspricht. Allerdings stellen arithmetische Schaltungen, insbesondere Integer-Multiplizierer auf Gatterebene, eine Herausforderung für bestehende Verifikationstechniken dar. In dieser Dissertation [Ka20] werden aktuelle Verifikationsmethoden basierend auf Computeral- gebra verbessert. Wir zeigen eine rigorose präzise mathematische Formulierung, welche auch die Anwendung der Mathematik in diesem Gebiet erweitert. Außerdem haben wir neue Methoden zur vollautomatischen Verifikation von Integer-Multiplizierern entworfen und implementiert, sowie ein kompaktes Beweisformat entwickelt, um das Ergebnis der Verifikation zertifizieren zu können.