Highly Automated Formal Verification of Arithmetic Circuits
Veröffentlichungsdatum
2017-02-07
Autoren
Betreuer
Gutachter
Zusammenfassung
This dissertation investigates the problems of two distinctive formal verification techniques for verifying large scale multiplier circuits and proposes two approaches to overcome some of these problems. The first technique is equivalence checking based on recurrence relations, while the second one is the symbolic computation technique which is based on the theory of Gröbner bases. This investigation demonstrates that approaches based on symbolic computation have better scalability and more robustness than state-of-the-art equivalence checking techniques for verification of arithmetic circuits. According to this conclusion, the thesis leverages the symbolic computation technique to verify floating-point designs. It proposes a new algebraic equivalence checking, in contrast to classical combinational equivalence checking, the proposed technique is capable of checking the equivalence of two circuits which have different architectures of arithmetic units as well as control logic parts, e.g., floating-point multipliers.
Schlagwörter
Formal verification
;
Arithmetic Circuits
;
Symbolic Computation
;
Equivalence Checking
Institution
Fachbereich
Dokumenttyp
Dissertation
Zweitveröffentlichung
Nein
Sprache
Englisch
Dateien![Vorschaubild]()
Lade...
Name
00105740-1.pdf
Size
1.05 MB
Format
Adobe PDF
Checksum
(MD5):82444180b0da1eaf3ebb030bb7f42bbf