TECHNION Formal Verification of VHDL-Based Real-Time Hardware Designs

Ziele

Dieses Kooperationsprojekt mit dem Technion (Haifa, Israel) hatte zum Ziel,Beweismethoden für die Hardwarebeschreibungssprache VHDL zu entwickeln. Die Methoden sollten auf zwei Weisen die Komplexitätsprobleme, die sich in der Praxis ergeben, angehen. Zum einen sollten Abstraktionstechniken entwickelt werden, die es erlauben, große Datenräume algebraisch zu behandeln und nicht jedes Datum separat betrachten zu müssen. Zum anderen waren neue Konzepte gefragt, um quantitative Aspekte der Zeit ähnlich abstrakt zu repräsentieren. So stellten die Arbeiten eine Ergänzung zu den Entwicklungen im Projekt FORMAT dar, wo der Schwerpunkt auf der werkzeugmäßigen Umsetzung von theoretisch fundierten Verifikationstechniken lag.

 

Überblick

Als ein Hauptergebins ist eine neue Methode zu nennen, die eine hochgradigautomatische Behandlung von Verifikationsproblemen ermöglicht, wo früher nur manuelle oder bestenfalls interaktive Techniken einsetzbar waren. Vornehmliches Anwendungsgebiet sind Systeme, wo neben dem Kontrollanteil auch nichttriviale Berechnungen auf Datenwerten anfallen, etwa Steuerungen komplexerer Systeme. Die Methode beruht auf einer unterschiedlichen Behandlung von Daten und Kontrolle. Während die verschiedenen Kontrollzustände separat behandelt werden, braucht auf den Daten nur das unterschieden zu werden, was auch auf die Kontrolle zurückschlägt. In logischen Charakterisierungen wird ausgedrückt, welche Daten zu welchen Reaktionen des Systems führen. Inwieweit dann das System seiner Spezifikation genügt, reduziert sich dabei auf einen Test, der die berechneten Charakterisierungen mit den geforderten vergleicht. Besonders hervorzuheben ist, daß auf diese Weise bekannte Spezialfälle, in denen die Komplexität des Datenraumes herausgerechnet werden kann, hier uniform und automatisch miterfaßt werden. Entwickelt worden sind die theoretischen Grundlagen des Verfahrens und die wesentlichen Algorithmen zu seiner praktischen Umsetzung. Eine Implementierung wird außerhalb des Projektes realisiert.

Bei den Methoden zur Behandlung der Realzeitproblematik sind die Arbeiten noch nicht zu einem Abschluß gebracht worden. Ebenso wie im Fall der Daten sind die bekannten Verfahren in der Praxis häufig aus Komplexitätsgründen nicht anwendbar. Hier war die Stoßrichtung, allgemeinere Verfahren bei Spezialisierung auf eingeschränktere, jedoch praxisrelevante Modellierungsklassen effizienter zu gestalten. Die bereits erreichten Zwischenresultate werden in das Projekt SACRES einfließen.

Personen

Laufzeit

Start: 01.01.1994
Ende: 31.12.1998