Digitale Hardware/ Software-Systeme- P10: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 | Äquivalenzprüfung kombinatorischer und sequentieller Schaltungen 263 wahrend der symbolischen Simulation die Erreichbarkeitsmenge SR t für die in Zeitschritt t erreichbaren Zustande berechnet. Man beachte den Unterschied der beiden Definitionen von Erreichbarkeitsmengen Wahrend bei den Verfahren zur Prüfung von Automatenaquivalenz aus Kapitel alle wahrend t Zeitschritten erreichbaren Zustande berechnet werden SR t SR t - 1 U SUCC SR t - 1 wird bei der symbolischen Simulation der Miter-Schaltung lediglich die Menge an Zuständen bestimmt in der die Schaltwerke nach genau t Zeitschritten sein können SR t SUCC SR t 1 . SUCC S ist dabei jeweils die Menge der aus der Menge S von Zustanden in genau einem Schritt erreichbaren Zustanden. Um den Fixpunkt bei der symbolischen Simulation erkennen zu konnen muss somit vor der Simulation eines neuen Zeitschritts die Menge aller bisher erreichten Zustande bestimmt und mit der vorherigen verglichen werden. Strukturelle Aquivalenzprüfung auf der Logikebene Die implizite kombinatorische Aquivalenzprüfung auf der Logikebene mit ROBDDs oder ROKFDDs kann aufgrund des hohen Speicherbedarfs oftmals nicht für große kombinatorische Schaltungen durchgeführt werden. Äuf der anderen Seite ist die formale explizite kombinatorische Aquivalenzprüfung für große Systeme aufgrund der großen Laufzeit auch nicht anwendbar. Zusammenfassend kann man sagen dass sich die formalen Methoden lediglich auf kleine bis mittlere Probleminstanzen anwenden lassen. Um diese Verfahren auch für größere Systeme zu verwenden besteht die Moglichkeit diese mit strukturellen Verfahren zu kombinieren. Im Folgenden werden zunachst wieder nur Schaltnetze also Systeme ohne Speicher betrachtet. Anschließend wird ein strukturelles Verfahren für Schaltwerke vorgestellt. Strukturelle Aquivalenzprüfung auf Basis von Schaltungspartitionierung Für eine explizite strukturelle Aquivalenzprüfung ist der Ausgangspunkt die Miter-Schaltung zweier kombinatorischer .
