Logo des Repositoriums
Zur Startseite
  • English
  • Deutsch
Anmelden
  1. Startseite
  2. SuUB
  3. Dissertationen
  4. Highly Automated Formal Verification of Arithmetic Circuits
 
Zitierlink URN
https://nbn-resolving.de/urn:nbn:de:gbv:46-00105740-19

Highly Automated Formal Verification of Arithmetic Circuits

Veröffentlichungsdatum
2017-02-07
Autoren
Sayed-Ahmed, Amr  
Betreuer
Drechsler, Rolf  
Gutachter
Scholl, Christoph  
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
Universität Bremen  
Fachbereich
Fachbereich 03: Mathematik/Informatik (FB 03)  
Dokumenttyp
Dissertation
Zweitveröffentlichung
Nein
Sprache
Englisch
Dateien
Lade...
Vorschaubild
Name

00105740-1.pdf

Size

1.05 MB

Format

Adobe PDF

Checksum

(MD5):82444180b0da1eaf3ebb030bb7f42bbf

Built with DSpace-CRIS software - Extension maintained and optimized by 4Science

  • Datenschutzbestimmungen
  • Endnutzervereinbarung
  • Feedback schicken