Digitale Hardware/ Software-Systeme- P12:Getrieben durch neue Technologien und Anwendungen wird der Entwurf eingebetteter Systeme zunehmend komplexer. Dabei ist eine Umsetzung als Hardware/Software- System heutzutage der Stand der Technik. Die Minimierung von Fehlern im Entwurf dieser Systeme ist aufgrund deren Komplexit¨at eine der zentralen Herausforderungen unserer heutigen Zeit. Bereits heute wird mehr Aufwand in die Verifikation, also in die U¨ berpru¨fung der Korrektheit, eines eingebetteten Systems gesteckt als in den eigentlichen Entwurf | Funktionale Eigenschaftsprüfung 323 Funktionale Eigenschaftsprüfung Für die funktionale Eigenschaftsprüfung von Hardware-Komponenten werden heutzutage im Wesentlichen zusicherungsbasierte oder SAT-basierte Verfahren eingesetzt. Beide Ansätze werden im Folgenden naher betrachtet. Zusicherungsbasierte Eigenschaftsprüfung Für die zusicherungsbasierte simulative Eigenschaftsprüfung werden Zusicherungen engl. assertions zunachst in Monitore übersetzt siehe Abschnitt . Für die funktionale Eigenschaftsprüfung von Hardware-Komponenten werden diese Monitore in Schaltungen synthetisiert. Die resultierenden Monitorschaltungen können anschließend zusammen mit dem Modell der Schaltung simuliert werden oder zur Überprüfung der Schaltung im spateren Betrieb auch mit gefertigt werden. Im Folgenden wird gezeigt wie Monitore für PSL-Zusicherungen generiert werden konnen. Synthese von Monitoren Üm Monitore zur simulativen Prüfung von Zusicherungen im Hardware-Entwurf einsetzen zu konnen müssen Monitore synthetisiert werden. Somit werden Monitore als Komponenten implementiert die als Eingang das Taktsignal das Rücksetzsignal weitere Synchronisationssignale und Signale des SÜV engl. System Under Verification welche für die Überprüfung der Zusicherung beobachtet werden müssen erhalten. Die Ausgabe der Monitorkomponente zeigt dann an inwieweit die zu überprüfende Zusicherung momentan erfüllt ist. Eine Zusicherung kann in einer Simulation entweder 1. stark erfüllt sein wenn die Zusicherung bereits erfüllt ist und unter jedem erdenklichen Ausführungspfad auch bei Beendigung der Simulation weiter erfüllt sein wird 2. erfüllt sein wenn die Zusicherung bereits erfüllt wurde aber Ausführungspfade denkbar sind welche die Zusicherung widerlegen 3. ausstehend sein wenn die Zusicherung bisher weder erfüllt wurde noch widerlegt wurde aber Ausführungspfade moglich sind welche die Zusicherung erfüllen oder widerlegen oder 4. nicht erfüllt sein wenn die Zusicherung bereits .
