Modellgenerierung für die SAT-basierte Eigenschaftsprüfung

Modelgeneration for SAT-based property checking

  • Mit zunehmender Integration von immermehr Funktionalität in zukünftigen SoC-Designs erhöht sich die Bedeutung der funktionalen Verifikation auf der Blockebene. Nur Blockentwürfe mit extrem niedriger Fehlerrate erlauben eine schnelle Integration in einen SoC-Entwurf. Diese hohen Qualitätsansprüche können durch simulationsbasierte Verifikation nicht erreicht werden. Aus diesem Grund rücken Methoden zur formalen Entwurfsverifikation in den Fokus. Auf der Blockebene hat sich die Eigenschaftsprüfung basierend auf dem iterativen Schaltungsmodell als erfolgreiche Technologie herausgestellt. Trotzdem gibt es immer noch einige Design-Klassen, die für BIMC schwer zu handhaben sind. Hierzu gehören Schaltungen mit hoher sequentieller Tiefe sowie arithmetische Blöcke. Die fortlaufende Verbesserung der verwendeten Beweismethoden, z.B. der verwendeten SAT-Solver, wird der zunehmenden Komplexität immer größer werdender Blöcke alleine nicht gewachsen sein. Aus diesem Grund zeigt diese Arbeit auf, wie bereits in der Problemaufbereitung des Front-Ends eines Werkzeugs zur formalen Verifikation Maßnahmen zur Vereinfachung der entstehenden Beweisprobleme ergriffen werden können. In den beiden angesprochenen Problemfeldern werden dazu exemplarisch geeignete Freiheitsgrade bei der Modellgenerierung im Front-End identifiziert und zur Vereinfachung der Beweisaufgaben für das Back-End ausgenutzt.

Volltext Dateien herunterladen

Metadaten exportieren

  • Export nach Bibtex
  • Export nach RIS

Weitere Dienste

Teilen auf Twitter Suche bei Google Scholar
Metadaten
Verfasserangaben:Markus Wedler
URN (Permalink):urn:nbn:de:hbz:386-kluedo-19794
Betreuer:Wolfgang Kunz
Dokumentart:Dissertation
Sprache der Veröffentlichung:Deutsch
Jahr der Fertigstellung:2006
Jahr der Veröffentlichung:2006
Veröffentlichende Institution:Technische Universität Kaiserslautern
Titel verleihende Institution:Technische Universität Kaiserslautern
Datum der Annahme der Abschlussarbeit:08.08.2006
Datum der Publikation (Server):22.08.2006
Freies Schlagwort / Tag:Eigenschaftsprüfung; Modellgenerierung
front end ; model generation; property checking
GND-Schlagwort:Arithmetik; Bounded Model Checking ; Erfüllbarkeitsproblem ; Model checking ; System-on-Chip ; Verifikation
Fachbereiche / Organisatorische Einheiten:Fachbereich Elektrotechnik und Informationstechnik
CCS-Klassifikation (Informatik):B. Hardware / B.2 ARITHMETIC AND LOGIC STRUCTURES / B.2.3 Reliability, Testing, and Fault-Tolerance** (B.8)
DDC-Sachgruppen:6 Technik, Medizin, angewandte Wissenschaften / 62 Ingenieurwissenschaften / 620 Ingenieurwissenschaften und zugeordnete Tätigkeiten
Lizenz (Deutsch):Standard gemäß KLUEDO-Leitlinien vor dem 27.05.2011

$Rev: 13581 $