Anwendung normalisierter Eigenschaften zur Verbesserung von Qualitätsaussagen in der funktionalen Hardware-Verifikation

Eine möglichst fehlerfreie Elektronik ist heutzutage in vielen Bereichen äußerst wichtig. Digitale Hardware wird wie z. B. in der Medizin, in der Automobilindustrie oder in der Luft- und Raumfahrt in vielen sicherheitskritischen Systemen eingesetzt, die bei Fehlern unmittelbar Leben in Gefahr bringen können. Auch im Finanzwesen können Fehler in der Hardware sehr schnell sehr teuer werden. Aus diesem Grund wird bei deren Entwicklung bis zu 70% der Zeit für die Verifikation, die Qualitätssicherung des Produktes, aufgewendet. Nur wer schnell ein fehlerfreies Produkt auf den Markt bringt und Kosten für ein Re-Design vermeidet, kann seine Stellung festigen. Es gilt, first-to-market zu sein. Durch Werkzeuge für die Entwurfsautomatisierung kann Fehlern im immer wiederkehrenden Entwurfsablauf vorgebeugt werden. Menschliche Fehler werden weitestgehend durch rechnergestützte Prozesse wie die Synthese von Schaltungen aus Hardwarebeschreibungssprachen vermieden. Weiterhin stellen Modellprüfungen die Konsistenz zwischen Spezifikation und Implementierung des Systems sicher. Die vorgelegte Dissertation soll hierbei die Erstellung und Nutzung von formalen (funktionalen) Spezifikationen unterstützen. Formale Spezifikationen stellen eine eindeutige Beschreibung eines Systems dar im Gegensatz zu Spezifikationen in gesprochener Sprache. Sie sind Voraussetzung für eine maschinelle Verarbeitung, wie es z. B. bei der formalen Eigenschaftsprüfung notwendig ist. Zur Beurteilung der Qualität solcher Spezifikationen wurde ein Verfahren entwickelt, mit dem der Determiniertheitsgrad der Ausgänge eines Systems bestimmt werden kann. Dieses quantitative Maß erlaubt Aussagen über die Vollständigkeit einer Spezifikation. Neben der Vollständigkeit können auch Widersprüche innerhalb einer Spezifikation gefunden werden. Beide Analysen sind bei praxisrelevanten Spezifikationen von Hand nicht möglich, sie können jedoch rechnergestützt durchgeführt werden. Neben dem Einsatz bei der Eigenschaftsprüfung können formale Spezifikationen auch die Simulation von Hardwaremodellen unterstützen. Simulation ist das häufigste Verifikationsverfahren, gerade bei der Systemverifikation. Zur Beurteilung der Simulation in Bezug auf die formale Spezifikation wurde ein Normalisierungsalgorithmus entwickelt, der formale Spezifikationen in so genannte Microproperties zerlegt, eine atomare Beschreibung der Funktionalität. Als Assertions simuliert können diese die formale Spezifikation mit den Simulationsergebnissen wie Überdeckungsmaßen in Zusammenhang bringen. Alle entwickelten Verfahren wurden an verschiedenen Spezifikationen überprüft.