Beschleunigungstechniken bei der Verifikation von Analogschaltungen mit Bounded Model Checking

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.