tailieunhanh - Digitale Hardware/ Software-Systeme- P19

Digitale Hardware/ Software-Systeme- P19: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 | 534 B Binare Entscheidungsdiagramme für jeden Nichtterminalknoten v e VN weist eine Funktion child VN x 1 . A Aindex v V dem Knoten v seine Nachfolger zu d. h. v child v k e E mit 1 k 4 AindeX v eine Funktion value VT B weist jedem Terminalknoten einen Wert aus der Zielmenge B zu. Ein Entscheidungsdiagramm besitzt genau einen ausgezeichneten Quellknoten d. h. einen Knoten ohne Vorgänger von dem aus alle Knoten v e V erreichbar sind. Terminalknoten sind Blatter und besitzen die Eigenschaft dass sie keine Nachfolger haben. Die Große eines Entscheidungsdiagramms ist gegeben durch die Anzahl seiner Knoten d. h. size G V . Ein Entscheidungsdiagramm heißt komplett wenn jede Variable ai auf jedem Pfad vom Quellknoten zu einem Terminalknoten genau einmal auftritt. Ein Entscheidungsdiagramm heißt frei falls jede Variable ai auf jedem Pfad vom Quellknoten zu einem Terminalknoten höchstens einmal auftritt. Ein Entscheidungsdiagramm G heißt geordnet falls G frei ist und auf jedem Pfad vom Quellknoten zu einem Terminalknoten die Variablen in der selben Reihenfolge auftreten. Binäre Entscheidungsdiagramme Boolesche Funktionen können als binare Entscheidungsdiagramme reprasentiert werden. Grundlage hierzu bildet die Shannon-Zerlegung 393 welche auf dem Konzept von Kofaktoren basiert. Gegeben sei ein Boolesche Funktion f Bn B mit Variablen x1 . xn. Die Funktion f x f f x1 . xi-1 F xi 1 .xn heißt negativer Kofaktor bezüglich Xi. Die Funktion f x t f x1 . xi-1 T xi 1 . xn heißt positiver Kofaktor bezüglich x . Sowohl f x F als auch f x T sind unabhangig von der Variablen x . Jede Boolesche Funktion f lasst sich mit Hilfe der ShannonZerlegung wie folgt mit Kofaktoren schreiben f -xt A f x f v x A f x t Falls nun in einem Entscheidungsdiagramm in jedem Nichtterminalknoten v e VN die Shannon-Zerlegung nach der mit den Knoten assoziierten Variablen xindex v durchgeführt wird so erhalt man ein binäres Entscheidungsdiagramm engl. Binary Decision Diagram BDD . Mit Vv e VN A B Ao B