Beschleunigungstechniken bei der Verifikation von Analogschaltungen mit Bounded Model Checking
Conference: ANALOG '06 - 9. ITG/GMM-Fachtagung
09/27/2006 - 09/29/2006 at Dresden, Germany
Proceedings: ANALOG '06
Pages: 6Language: germanTyp: PDF
Personal VDE Members are entitled to a 10% discount on this title
Authors:
Ehrenfried, Andreas (Fachgebiet Rechnersysteme, Fachbereich Elektrotechnik und Informationstechnik, TU Darmstadt, Deutschland)
Abstract:
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.