Digitale Hardware/ Software-Systeme- Part 6

Digitale Hardware/ Software-Systeme- P6:Getrieben durch neue Technologien und Anwendungen wird der Entwurf eingebetteterSysteme zunehmend komplexer. Dabei ist eine Umsetzung als Hardware/Software-System heutzutage der Stand der Technik. Die Minimierung von Fehlern imEntwurf dieser Systeme ist aufgrund deren Komplexit¨at eine der zentralen Herausforderungenunserer heutigen Zeit. Bereits heute wird mehr Aufwand in die Verifikation,also in die U¨ berpru¨fung der Korrektheit, eines eingebetteten Systems gestecktals in den eigentlichen Entwurf....
Nội dung trích xuất từ tài liệu:
Digitale Hardware/ Software-Systeme- Part 6142 ¨ 4 Aquivalenzpr¨ fung uFolgenden als w = w1 , w2 , . . . wn geschrieben. Analog werden Ausgabesequenzenw ∈ O+ der L¨ nge m im Folgenden als w = w1 , w2 , . . . wm geschrieben. Mit diesen aDefinitionen lassen sich eine erweiterte Ubergangsfunktion f + : S × I + → S und eine ¨erweiterte Ausgabefunktion g+ : S × I + → O+ definieren [329]: f (s, w) falls |w| = 1 f + (s, w) := (4.3) f ( f + (s, w1 , . . . , wn−1 ), wn ) falls |w| ≥ 2 g(s, w) falls |w| = 1 g+ (s, w) := g+ (s, w1 , . . . , wn−1 ), g( f + (s, w1 , . . . , wn−1 ), wn ) falls |w| ≥ 2 (4.4)Zu beachten ist, dass die erweiterte Ubergangsfunktion f + einen einzelnen Zustand ¨berechnet, w¨ hrend die erweiterte Ausgabefunktion g+ eine Sequenz w ∈ O+ an aAusgabesymbolen bestimmt. ¨4.3.1 Automaten-Aquivalenz ¨Mit Hilfe der Gleichungen (4.3) und (4.4) kann die Aquivalenz zweier endlicherAutomaten gezeigt werden. ¨Definition 4.3.1 (Automaten-Aquivalenz). Zwei deterministische endliche Auto-maten M := (I, O, S, s0 , f , g) und M := (I , O , S , s0 , f , g ) mit Anfangszustand s0 ¨bzw. s0 sind aquivalent oder verhaltensgleich, wenn f¨ r eine beliebige Eingabese- uquenz w ∈ I + , die an beide Automaten angelegt wird, die selbe Ausgabesequenz ent-steht, d. h. ∀w ∈ I + : g+ (s0 , w) = g + (s0 , w) . ¨ Dieser Definition von Automaten-Aquivalenz liegt eine simulativen Methode zur ¨expliziten Aquivalenzpr¨ fung zu Grunde. Da simulative Verfahren in der Regel un- u ¨vollst¨ ndig sind, wird ein geeignetes Uberdeckungsmaß zur Bestimmung der Ve- arifikationsvollst¨ ndigkeit ben¨ tigt. Hierin liegt aber ein Problem, da I + unendlich a o ¨groß ist und alle enthaltenen Sequenzen uberpr¨ ft werden m¨ ssen, um eine 100%- u u a u ¨ige Vollst¨ ndigkeit zu erzielen. Somit ist Definition 4.3.1 f¨ r einen Beweis der Aqui-valenz zweier Automaten ungeeignet. ¨ Um formal die Aquivalenz zweier Automaten zu zeigen, wird zun¨ chst die Zu- astands¨ quivalenz definiert. aDefinition 4.3.2 (Zustands¨ quivalenz). Gegeben seien zwei deterministische end- aliche Automaten M := (I, O, S, s0 , f , g) und M := (I, O, S , s0 , f , g ) mit Anfangszu- ¨stand s0 bzw. s0 und identischem Eingabe- und Ausgabealphabet. Die Aquivalenzre-lation f¨ r Zust¨ nde ≡ ⊆ S × S ist die gr¨ ßte Relation mit u a o s ≡ s ⇔ ∀i ∈ I : (g(s, i) = g (s , i)) ∧ ( f (s, i) ≡ f (s , i)) .Aus Definition 4.3.2 folgt direkt: ∀w ∈ I + : s ≡ s ⇔ f + (s, w) ≡ f + (s , w) (4.5)Somit gilt ¨ 4.3 Sequentielle Aquivalenzpr¨ fung u 143 ¨Theorem 4.3.1. Zwei deterministische endliche Automaten M und M sind aquiva-lent, geschrieben als M ≡ M , genau dann, wenn ihre Anfangszust¨ nde aquivalent a ¨sind, d. h. s0 ≡ s0 . ¨ Somit reduziert sich das Problem der Automaten-Aquivalenz auf eine rekursive ¨ ¨Definition. Diese kann in eine iterative Uberpr¨ fung der Aquivalenz der Ausgaben ug(s, i) = g (s , i) umgewandelt werden. Dabei m¨ ssen allerdings nicht alle m¨ glichen u oZustandspaare (s, s ) ∈ S × S uberpr¨ ft werden, ...