Textdokument
Qualitätsorientierter Entwurfs- und Verifikationsablauf für digitale Systeme
Vorschaubild nicht verfügbar
Volltext URI
Dokumententyp
Dateien
Zusatzinformation
Datum
2009
Autor:innen
Zeitschriftentitel
ISSN der Zeitschrift
Bandtitel
Verlag
Gesellschaft für Informatik
Zusammenfassung
Auf Grund der technologischen Möglichkeiten bei der Fertigung integrierter Schaltkreise hat die Verbreitung elektronischer Systeme massiv zugenommen. Diese umgeben uns heutzutage oft unsichtbar in Form von sogenannten eingebetteten Systemen und übernehmen zentrale Steuerungsaufgaben, zunehmend auch in sicherheitskritischen Anwendungen. Deshalb steigen die Qualitätsanforderungen vor allem im Hinblick auf die Korrektheit beim Entwurf – eine große Herausforderung in Anbetracht der stark zunehmenden Komplexität solcher Systeme. In der hier zusammengefassten Dissertation [Gro08] wird nach Erläuterung des etablierten Entwurfablaufs von digitalen Systemen erstmals ein qualitätsorientierter Entwurfs- und Verifikationsablauf vorgestellt. Vor allem unter den folgenden beiden Gesichtspunkten werden durch den vorgestellten Ablauf wichtige Beiträge auf dem Gebiet des Systementwurfs geleistet: (1) Es werden auf den unterschiedlichen Abstraktionsebenen neue auf die jeweilige Aufgabe „zugeschnittene“ Verifikationstechniken integriert. (2) Die erreichte Verifikationsqualität wird messbar gemacht. Vorliegende Lücken bei der Verifikation werden automatisch identifiziert, so dass die Qualität gezielt verbessert werden kann. Im Zusammenhang mit der Qualitätssicherung auf der Blockebene, wo für die Verifikation die formale Eigenschaftsprüfung eingesetzt wird, konnte ein bisher offenes Problem aus dem Schaltkreisentwurf gelöst werden, indem nun die Frage beantwortet werden kann, ob genügend Eigenschaften spezifiziert wurden. Die Anwendung des in der vorgestellten Arbeit entwickelten Verfahrens zur Coverage-Analyse in der Eigenschaftsprüfung wurde erfolgreich für eine RISC CPU demonstriert. So konnten vollautomatisch alle Verifikationslücken aufgedeckt und schlussendlich auch geschlossen werden, so dass eine vollständige Coverage des Schaltkreisverhaltens durch den Eigenschaftssatz – also die bestmögliche Qualität – erzielt wurde.