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.