Digitale Hardware/ Software-Systeme- P18: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. | Funktionale Eigenschaftsprüfung 333 a req_in token_out overridejn tokenjn override_out grantjn b F reqn-1 reqi req0 Abb. . Ein skalierbarer Arbitrierer 206 G acki reqi 3. Lebendigkeit Jede Anforderung wird innerhalb von 2n Zeitschritten durch Signal acki bestätigt G reqi F n-i acki Für die letzte Eigenschaft wurde das zu berücksichtigende Zeitintervall 0 2n - 1 an den Operator F annotiert. Diese Erweiterung beschrankt die Gültigkeit des Operators auf das gegebene Zeitintervall. Weiterhin lasst sich die Lebendigkeitseigenschaft in der Form G reqi F 0 2n-1 acki nicht beweisen. Hierzu ist es notwendig eine Annahme über die Umgebung zu treffen 206 Ein Signal reqi muss solange auf T gehalten werden bis die zugehörige Bestatigung durch Signal acki erfolgte. Somit 334 6 Hardware-Verifikation ergibt sich als Lebendigkeitseigenschaft G G oi2 _i reqt -ach X reqi reqt F o 2 _i ackt Der Operator G gilt entsprechend dem erweiterten Operator F hier nur für das gegebene Zeitintervall. Große und Drechsler berichten in 206 die Anzahl erreichbarer Zustande des skalierbaren Arbitrierers. Diese sind in Tabelle dargestellt. Tabelle . Anzahl erreichbarer Zustande des skalierbarer Arbitrierers 206 Zellen Zustande Zellen Zustande Zellen Zustande Zellen Zustande 2 8 6 384 10 50 5 63 1016 3 24 7 896 11 100 1 27 1032 4 64 8 12 150 2 14 1047 5 160 9 20 2 10 107 200 3 21 1062 Schaltungen auf der Logikebene erlauben eine direkte Übersetzung in endliche Automaten die sich symbolisch repräsentieren lassen. Somit lasst sich die in Abschnitt beschriebene SAT-basierte Modellprüfung auch direkt auf Schaltungen auf der Logikebene anwenden. Im Folgenden werden daher lediglich einige Besonderheiten bei der formalen Modellprüfung von Hardware betrachtet. SAT-basierte Modellprüfung bei mehreren Taktdomänen Typische eingebettete Computersysteme sogar wenn auf einem einzelnen Chip integriert verfügen über mehrere sog. Taktdomänen. Der Grund .
