Digitale Hardware/ Software-Systeme- P29: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. | 554 C Algorithmen Nach Abb. wird zunächst der SAT-Solver aufgerufen um die aussagenlogische Formel pa auf Erfüllbarkeit zu testen. Eine mögliche Belegung ß die pa erfüllt ware z. B. ß -ai -a2 -a -a4 b 1 6 1 . Durch BCP vervollstandigt sich die Belegung ß zu ß -a1 b1 -a2 b2 -a3 b3 -a4 b4 b5 1 b6 1 Dies impliziert die folgende Menge atomarer pradikatenlogischer Formeln O u - w 5 v w 6 z 0 u v 12 x z 1 y z 2 u v - 4 x - 4 y 0 Die Konjunktion der Formeln wird vom Theorieloser in diesem Fall ein LRA-Solver engl. Linear Reel Arithmetik auf Erfüllbarkeit überprüft. Die oben gegebene Formelmenge O ist nicht erfüllbar. Die anschließende Konfliktanalyse siehe Abb. ergibt dass die Belegung b1 b2 b4 T zu einem Konflikt geführt hat. Aus diesem Grund wird zur Verfeinerung der aussagenlogischen Formel pa die Klausel -b1 V -b2 V -b4 - b1 A b2 A b4 hinzugefügt. Abb. . Konfliktanalyse im LRA-Solver 397 In Beispiel konnte der Theorieloser keine konsistente Belegung der Variablen der pradikatenlogischen Formeln finden. In diesem Fall sagt man dass das Modell der aussagenlogischen Formel T-inkonsistent ist. Andernfalls heißt das Modell T-konsistent. In dem oben skizzierten Vorgehen werden lediglich vollstandige Modelle der aussagenlogischen Formel auf T-Konsistenz geprüft. Eine mogliche Verbesserung des SMT-Solvers besteht darin auch partielle Belegungen auf T -Konsistenz zu prüfen. SMT-Solver 555 Beispiel . Dies wird anhand des Beispiels verdeutlicht nachdem die Klausel b1 V b2 V b4 vom SMT-Solver gelernt wurde. Abbildung zeigt die einzelnen Entscheidungen des SAT-Solvers sowie die Interaktion des SAT-Solvers mit dem Theorieloser. Abb. . Schnelle Konfliktanalyse Im ersten Schritt Abb. belegt der SAT-Solver die Boolesche Variable a1 mit dem Wert F. Durch BCP wird die Variable b1 mit dem Wert T belegt. Da b1 T eine atomare pradikatenlogische Formel impliziert wird sofort der LRA-Solver aufgerufen. Neben der Formel u w 5 muss der LRA-Solver .
