Digitale Hardware/ Software-Systeme- P6: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 | 142 4 Äquivalenzprüfung Folgenden als w wb w2 . wn geschrieben. Änalog werden Äusgabesequenzen w e O der Lange m im Folgenden als w w1 w2 . wm geschrieben. Mit diesen Definitionen lassen sich eine erweiterte Übergangsfunktion f S x I S und eine erweiterte Ausgabefunktion g S x I O definieren 329 f sw f sw falls lwl 1 43 f f s wi . wn-1 wn falls w 2 . g sw . g s w falls lwl 1 g 1 g s wb. wn-1 g f s w1 . wn-1 w falls w 2 Zu beachten ist dass die erweiterte Übergangsfunktion f einen einzelnen Zustand berechnet wahrend die erweiterte Äusgabefunktion g eine Sequenz w e O an Äusgabesymbolen bestimmt. Automaten-Aquivalenz Mit Hilfe der Gleichungen und kann die Äquivalenz zweier endlicher Äutomaten gezeigt werden. Definition Automaten-Aquivalenz . Zwei deterministische endliche Automaten M I O S so f g und M I O S s 0 f g mit Anfangszustand s0 bzw. s o sind äquivalent oder verhaltensgleich wenn für eine beliebige Eingabesequenz w e I die an beide Automaten angelegt wird die selbe Ausgabesequenz entsteht d. h. Vw e I g so w g s0 w . Dieser Definition von Äutomaten-Äquivalenz liegt eine simulativen Methode zur expliziten jÄquivalenzprüfung zu Grunde. Da simulative Verfahren in der Regel un-vollstandig sind wird ein geeignetes Überdeckungsmaß zur Bestimmung der Ve-rifikationsvollstandigkeit benötigt. Hierin liegt aber ein Problem da I unendlich groß ist und alle enthaltenen Sequenzen überprüft werden müssen um eine 100 -ige Vollstandigkeit zu erzielen. Somit ist Definition für einen Beweis der Äquivalenz zweier Äutomaten ungeeignet. Üm formal die Äquivalenz zweier Äutomaten zu zeigen wird zunachst die Zustandsäquivalenz definiert. Definition Zustandsaquivalenz . Gegeben seien zwei deterministische endliche Automaten M I O S s0 f g und M I O S s o f g mit Anfangszustand s0 bzw. s 0 und identischem Eingabe- und Ausgabealphabet. Die Äquivalenzrelation für Zustande C S x S ist die größte Relation mit s f oVi e I g s i g s i A f s i f s i . Äus
