Digitale Hardware/ Software-Systeme- P2: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 | 20 1 Einleitung Dabei ist das Zeitverhalten der Hardware stark durch die gewählte Technologie beeinflusst Die Gatterlaufzeiten bestimmen den kritischen Pfad in einem System und somit die Taktrate bzw. die Tiefe der Pipeline. Diese Effekte sind nicht auf die Logikebene beschrankt sondern sind auch auf Architekturebene und sogar Systemebene zu berücksichtigen. Im Bereich der Software-Verifikation trifft man auf ahnliche Aufgaben wie in der Hardware-Verifikation. Auf Blockebene liegt die Implementierung in Form eines Assemblerprogramms für den gewahlten Prozessor vor. Die Spezifikation ist in einer Hochsprache verfasst haufig in eingebetteten Systemen C C . Auch auf dieser Ebene kann es wichtig sein die Äquivalenz von Programmen zu zeigen da gerade eingebettete Software stark optimiert wird um den Speicher- und Geschwindigkeitsanforderungen zu genügen. Da eingebettete Systeme und deren Software auch haufig in sicherheitskritischen Bereichen eingesetzt werden ergibt sich aber auch als weitere Verifikationsaufgabe zu zeigen ob ein Programm gewisse funktionale Eigenschaften besitzt. So sollte eine Steuerungs-Software nicht verklemmen und korrekt auf Anfragen reagieren. Daneben hat die Mikroarchitektur des Prozessors einen großen Einfluss auf die Abärbeitungsgeschwindigkeit von Instruktionen d. h. unterschiedliche Mikroarchitekturen können die selbe Instruktionssatzarchitektur implementieren aber ein unterschiedliches zeitliches Verhalten besitzen. Dies hat Einfluss auf die Ausführungszeiten nicht nur einzelner Instruktionen sondern auf ganze Programme. Die Überprüfung der Einhaltung der Zeitanforderung ist somit eine Verifikationsaufgabe sowohl auf Block- als auch auf Modulebene. Auf Systemebene ist die Überprüfung von Eigenschaften der Implementierung noch vordergründiger. Aufgrund der Komplexitat von Spezifikation und Implementierung ist eine vollstandige Prüfung nicht mehr praktikabel. Das Verhalten auf Systemebene wird oftmals durch ein Modell kommunizierender .
