Digitale Hardware/ Software-Systeme- P15: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. | Äquivalenzprüfung arithmetischer Schaltungen 273 Ausgange der Schaltwerke gezeigt werden. Hierzu muss zusätzlich der Fall betrachtet werden dass y1 2 aquivalent mit z 1 2 ist. Die neue Instruktionsqueue ergibt sich zu ß 3 yi i - z1 t 3i t - S2 t Die Stub-Schaltung ergibt sich durch Bestimmung der Verschmelzungspunkte und ist in Äbb. zu sehen. zi 1 X1 1 V2 1 X1 2 X2 2 Abb. . Stub-Schaltung für den dritten Zeitschritt 412 Man erkennt dass die im zweiten und dritten Schritt ermittelte Stub-Schaltung identisch ist. Äus diesem Grund wird durch Äbspielen von ß 3 nach Änhangen des Schaltungsmodells für den vierten Zeitschritt Äquivalenz erkannt. Da somit der Fixpunkt detektiert ist und in keinem Zeitschritt der Miter-Äusgang erfüllbar war sind die beiden Schaltwerke aquivalent. Aquivalenzpriifung arithmetischer Schaltungen Im Folgenden werden Verfahren für die Ärchitekturebene prasentiert die zur Äquivalenzprüfung arithmetischer Schaltungen geeignet sind. Diese eignen sich weiterhin auch zur Äquivalenzprüfung zwischen Modellen auf Ärchitektur- und Logikebene. Implizite Aquivalenzpriifung auf der Architekturebene Äuf der Ärchitekturebene siehe Äbb. auf Seite 235 ist die Granuläritat der Operationen in der Verhaltensspezifikation oftmals durch arithmetische Funktionen spezifiziert. Entsprechend sind die Objekte der Strukturmodelle der Implementierung Äddierer Multiplizierer ÄLUs engl. Arithmetic Logical Units etc. In der Synthese werden die arithmetischen Funktionen auf eine Ärchitektur bestehend aus einem 274 6 Hardware-Verifikation Datenpfad und einem Steuerwerk abgebildet. Ganzzahlige arithmetische Funktionen besitzen die Form f Zn Z. Für die implizite Äquivalenzprüfung dieser Funktionen bedarf es einer geeigneten kanonischen Repräsentation. Eine mögliche kanonische Repräsentation besteht darin erweiterte Diagramme ahnlich zu ROBDDs zu verwenden. Da bei BDDs allerdings der Definitionsbereich endlich ist bedarf es einer Einschränkung der Menge .
