Download Volltext

3.6 Vollständigkeitsprüfung
führt. Es gibt zwei Formen der Determinierung. Zum einen kann ein Signal
vollständig determiniert sein, was bedeutet, dass der Wert zu jeden Zeitpunkt
bestimmt ist. Dies wird durch die Zeile
determined ( Signalname ) , end_offset=Verz ö gerung ;
ausgedrückt. Die Angabe end_offset kennzeichnet eine verschobene Determinierung, gegenüber den Grenzen der Eigenschaft. Bei der Modellierung von
Pipelines vereinfacht diese Angabe die Durchführung des Determinierungstests.
Die zweite Form der Determinierung kommt zum Einsatz, wenn der Wert
eines Ausgangssignals nur von Bedeutung ist, wenn eine bestimmte Bedingung eintritt. So hängt beispielsweise die Determiniertheit des Datenausgangs
eines Speichers evtl. von der Aktivierung eines Lesesignals ab. Die Syntax
dieser Form wird mit dem Schlüsselwort if eingeleitet und sieht wie folgt
aus:
i f ( Bedingung ) then
determined ( Signalname ) ;
end i f , end_offset=Verz ö gerung ;
3.6.5 Resettests
Zusätzlich zu diesen drei Tests müssen für den Resetfall abgewandelte Formen
der anderen Tests genutzt werden. Diese als Resettests bezeichneten Prüfungen beweisen somit die entsprechenden Fragestellungen vor dem Hintergrund
der speziellen Gegebenheiten der Reseteigenschaft.
3.6.6 Trivialdesign
Die Beweisführung der Tests hängt nicht von einem tatsächlichen Hardwareentwurf ab. Sie werden vielmehr auf einem ”trivialen” Design durchgeführt,
welches zwar alle Signale und deren Datentypen kennt, jedoch kein weiteres Verhalten implementiert. Die Ausgänge und internen Signale besitzen im
Trivialdesign keinen Treiber, d.h. sie können zu jedem Zeitpunkt einen der
Werte ihres Wertebereichs frei auswählen.
Demnach kann eine Menge von Eigenschaften auf Vollständigkeit geprüft
werden kann, ohne dass bereits eine Implementierung vorliegt. Dies hilft dabei Fehler zu vermeiden und ermöglicht ein schnelleres Auffinden von noch
nicht beschriebener Funktionalität während des Entwurfs der Eigenschaften.
Bei der formalen Verifikation der Eigenschaften vor Erstellung oder automatisierten Generierung einer Implementierung muss jedoch das Trivialdesign
69