Modellierung analoger Schaltungen für die Erreichbarkeitsanalyse unter Berücksichtigung von Unsicherheiten

Die heutige Entwicklung von innovativen Produkten erfordert eine permanente Interaktion von komplexen analogen und digitalen Funktionsblöcken auf einem Chip. Sicherheitsrelevante Systeme müssen die sichere Funktion eines Chips in Steuergeräten garantieren. Um die Fehlerfreiheit eines zu entwickelnden Chips zu gewährleisten, muss während des gesamten Entwurfsprozesses die Korrektheit der Schaltungsmodelle verifiziert werden. Der zeitintensivste Teil des Entwurfsprozesses sind die gegenwärtig eingesetzten Verifikationsmethoden zur Untersuchung von Schaltungen mit Hilfe von Modellen. Eine stetig wachsende Herausforderung besteht in der Sicherstellung des korrekten Zusammenspiels sämtlicher Systemkomponenten unter allen möglichen Betriebsbedingungen. Trotz des enormen Zeitaufwands der gegenwärtig eingesetzten Verifikationsmethoden kann die Einhaltung der Spezifikation nicht garantiert werden.

Durch den Einsatz von formaler Verifikation kann die vollständige Einhaltung der Spezifikation gewährleistet werden. Gegenstand dieser Arbeit ist ein neuartiger Ansatz zur Modellierung analoger Schaltungen, für eine effiziente Erreichbarkeitsanalyse bei der formalen Verifikation. Zur Modellierung einer Schaltung wird ein Verfahren eingesetzt, das unter Zuhilfenahme stückweiser linearer Modelle das Verhalten einer Analogschaltung abstrahiert bzw. ein diskretes Modell einer Analogschaltung liefert. Eine Methode zur automatischen Erzeugung von hybriden Automaten aus einer Schaltungsnetzliste wird entwickelt. Unsicherheiten wie z.B. Prozessschwankungen und Approximationsfehler der Schaltungsmodelle werden dabei berücksichtigt. Die Evaluierung der Zustandsmenge durch eine Erreichbarkeitsanalyse soll eine minimale Überapproximation der erreichbaren Zustandsmenge liefern.

Die Leistungsfähigkeit verschiedener Modelle wird anhand von Schaltungsbeispielen untersucht. Vor- und Nachteile der Ansätze zur Modellerzeugung werden untersucht und ausgewertet. Die evaluierten Zustandsmengen werden mit verschiedenen Resultaten simulationsbasierter Verfahren verglichen.