Beschleunigungstechniken bei der Verifikation von Analogschaltungen mit Bounded Model Checking

Konferenz: ANALOG '06 - 9. ITG/GMM-Fachtagung
27.09.2006 - 29.09.2006 in Dresden, Germany

Tagungsband: ANALOG '06

Seiten: 6Sprache: DeutschTyp: PDF

Persönliche VDE-Mitglieder erhalten auf diesen Artikel 10% Rabatt

Autoren:
Ehrenfried, Andreas (Fachgebiet Rechnersysteme, Fachbereich Elektrotechnik und Informationstechnik, TU Darmstadt, Deutschland)

Inhalt:
In der vorliegenden Arbeit wird die in "W. Hartong, Ansätze zum Model-checking nichtlinearere analoger Systeme" und "D. Platte, D. Grabowski, L. Hedrich, E. Barke, Verifikation von Zeitbedingungen analoger Schaltungen durch Model-Checking- Verfahren" vorgestellte Methode zur Zustandsraumdiskretisierung und die in "A. Ehrenfried, D. Scholz, T. Welp, Anwendungsmöglichkeiten von Bounded Model Checking und affiner Arithmetik für die Verifikation von Analogschaltungen" vorgestellte Methode zu VHDL Erzeugung aus dem diskreten Zustandsraum erweitert. Eine Wahrscheinlichkeitsvariable für die Zustandsübergänge wird eingeführt. Diese ermöglicht beim Bounded Model Checking unwahrscheinliche Zustandsübergänge auszuschließen. Des Weiteren werden einige noch offene Probleme des Bounded Model Checking von Analogschaltungen angesprochen.