Đang chuẩn bị liên kết để tải về tài liệu:
Digitale Hardware/ Software-Systeme- Part 6

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 4.4 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. 4.3.1 Automaten-Aquivalenz Mit Hilfe der Gleichungen 4.3 und 4.4 kann die Äquivalenz zweier endlicher Äutomaten gezeigt werden. Definition 4.3.1 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 4.3.1 für einen Beweis der Äquivalenz zweier Äutomaten ungeeignet. Üm formal die Äquivalenz zweier Äutomaten zu zeigen wird zunachst die Zustandsäquivalenz definiert. Definition 4.3.2 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