Abstraktionsverfahren zur Eigenschaftsprüfung mit Bounded Model Checking

Der Entwurf höchstintegrierter digitaler Hardwaresysteme ist von einem immensen Aufwand zur Sicherstellung korrekten Verhaltens geprägt. Durch die fortschreitende Komplexität der entworfenen Schaltungen ist es sehr schwierig, die Einhaltung geforderter Eigenschaften zu beurteilen.

Neben der Simulation, mit der das Verhalten von Hardwareentwürfen in bestimmten Situationen untersucht werden kann, mit der es in der Regel aber unmöglich ist, das Verhalten in allen möglichen Situationen zu untersuchen, wurden formale Verifikationstechniken entwickelt. Verfahren zur formalen Modellprüfung ermöglichen, durch Rechnerhilfe einen Beweis für das Einhalten beziehungsweise Verletzen einer Eigenschaft durch einen Hardwareentwurf zu erhalten. Die historisch zuerst genutzten Verfahren basierten dabei auf der Repräsentation und Manipulation von Modellen und Eigenschaften als Entscheidungsbäume. Für viele Anwendungen haben sich Erfüllbarkeitsprüfer mittlerweile als mächtiger als OBDDs herausgestellt. In der industriellen Praxis kommt deshalb vermehrt das auf Erfüllbarkeitsprüfern beruhende "Bounded Model Checking" zur Anwendung. In der Vergangenheit wurden außerdem Abstraktionsverfahren entwickelt, die bei der Modellprüfung mit Hilfe von Entscheidungsbäumen die Nutzung vereinfachter Modelle erlauben und so die Wirkung der Zustandsraumexplosion verringern.

In der Arbeit wurde die Entwicklung eines Abstraktionsverfahrens zur Modellprüfung mittels Erfüllbarkeitsprüfer dokumentiert. Dieses Verfahren, welches eines der ersten Verfahren zum abstrahierenden Bounded Model Checking ist, zeichnet sich im Gegensatz zu bisherigen abstrahierenden Modellprüfungsverfahren dadurch aus, dass rechenintensive Algorithmen lediglich auf abstrakte Modelle angewendet werden, das Gesamtmodell jedoch ausschließlich durch Algorithmen geringer Komplexität untersucht wird.

Eine der Grundlagen des entwickelten Verfahrens ist die effiziente Vereinfachung von Belegungen boolescher Funktionen. Im Rahmen der Arbeit wurden deswegen nicht nur verschiedene Verfahren dazu untersucht, sondern auch Begriffe zur qualitativen Unterscheidung von Belegungen entwickelt. Mit diesen können die unterschiedlichen Leistungen der verschiedenen Vereinfachungsverfahren erklärt werden, sowohl bezüglich des erzielten Grads der Vereinfachung als auch des dazu erforderlichen Rechenaufwands.

Zur Untersuchung der entwickelten Verfahren und zum Vergleich mit herkömmlichen Techniken wurde eine experimentelle Modellprüfungsumgebung implementiert. Mit dieser ist es möglich, die entwickelten Verfahren auf industrierelevanten Modellen und Eigenschaften anzuwenden. Die mit dieser Implementierung durchgeführten Experimente zur Prüfung akademischer und industrieller Modelle und Eigenschaften belegen, dass die Kapazität durch die entwickelte Abstraktionstechnik deutlich gesteigert wird. Insbesondere werden bei den untersuchten Problemen im Durchschnitt sowohl die Rechenzeit als auch der Speicherbedarf deutlich gesenkt, abhängig von dem konkreten Modell um bis zu mehrere Größenordnungen. Der Speicherbedarf kann sogar bei nahezu jedem der untersuchten Probleme gesenkt werden.

Nebenprodukte der Arbeit sind zum einen durch die formale Beschreibung einer Untermenge der verbreitet eingesetzten Eigenschaftssprache ITL und zum anderen durch den für Forschung und Lehre zur Verfügung stehenden leistungsfähigen Modellprüfer gegeben.