In der digitalen Welt ist die Formale Verifikation von Schaltungen sehr verbreitet und wird mit Erfolg eingesetzt. Die Verifikation von nichtlinearen, analogen Schaltungen hingegen ist noch neu. In Schaltkreisen mit digitalen wie auch analogen Teilen entstehen im analogen Anteil ungefähr 50% der Fehler, die zu einer Neuimplementierung führen. Daher ist es von großem Interesse den analogen Teil ebenfalls verifizieren zu können.
Dieser Text entstand im Zuge einer Studienarbeit im Bereich Rechnersysteme an der Technischen Universität in Darmstadt. Die Motivation dieser Arbeit ist es, einen bereits bestehenden Ansatz zur Verifikation von analogen Schaltungen unter Verwendung des Model-Checking-Verfahrens zu vervollständigen und effizienter zu gestalten. Dieser verwendete Ansatz von Scholz und Ehrenfried basiert auf der Arbeit von Hartong.
Im Zuge der Arbeit wurde weiterhin untersucht, inwiefern sich der verwendete Ansatz um die Möglichkeit der Verifikation von analogen Schaltungen mit verschiedenen Arten von Eingangssignalen erweitern lässt.
Inhaltsverzeichnis
1 Motivation
2 Formale Verifikation analoger Schaltungen
3 Das bestehende Programm
3.1 Initialaufteilung des Zustandsraums
3.2 Ermittlung der Testvektoren
3.3 Weitere Aufteilung des Zustandsraums
3.4 Übergänge berechnen
3.5 Die Ausgabe
4 Erweiterungen des Programms
4.1 Dynamische Anpassung der Zeit
4.1.1 Erkennung von übersprungenen Zuständen
4.1.2 Das Verhalten wenn ein Zustand übersprungen wurde
4.1.3 Ungültige Vektoren
4.2 Auffinden von ungerechtfertigten Selbstverweisen
4.3 Berechnen der Übergangszeit
4.4 Weitere Zustandsaufteilungen
4.4.1 Der Zustand-Vektorwinkel-Vergleich
4.4.2 Der Zustand-Vektorlängen-Vergleich
4.4.3 Problem mit dem Zustand-Vektorlängen-Vergleich
4.4.4 Ergebnis der neuen Zustandsaufteilungen
5 Das Komplexitätsproblem
5.1 Angabe einer Grenzwahrscheinlichkeit
5.2 Angabe einer Mindestwahrscheinlichkeit
5.3 Auswahl einer Nachfolgedimension
5.4 Ergebnis der Verbesserungen
5.5 Weiterhin bestehende Probleme
6 Eingangssignale
6.1 Schaltungen mit (periodischen) Eingangssignalen
6.2 Erweiterung auf analoge Schaltungen mit digitalen Eingangssignalen
6.2.1 Der Zustandsraum
6.2.2 Vektoren berechnen
6.2.3 Zustände einteilen
6.2.4 Ergebnis
Zielsetzung & Themen
Die Arbeit verfolgt das Ziel, einen bestehenden Ansatz zur Verifikation analoger Schaltungen mittels Model-Checking zu vervollständigen und effizienter zu gestalten. Dabei wird insbesondere untersucht, wie das Verfahren auf die Verifikation analoger Schaltungen mit variablen Eingangssignalen erweitert werden kann.
- Optimierung der Zeitsteuerung und Zustandsaufteilung.
- Lösung des Komplexitätsproblems bei Zustandsautomaten.
- Einführung periodischer Eingangssignale als zusätzliche Dimension.
- Erweiterung auf Schaltungen mit digitalen Eingangssignalen.
- Automatisierte Testpunktgenerierung zur Validierung.
Auszug aus dem Buch
4.1 Dynamische Anpassung der Zeit
Für die Berechnung der Vektoren wird in dem Programm eine Zeit dt bestimmt, mit welcher der Übergang vom Startpunkt zum Zielpunkt des Vektors simuliert wird. Einen einheitlichen Wert dt zu finden, der in jedem Zustand des Systems sinnvoll ist, ist jedoch nicht möglich. In Bereichen, in denen sich das System nur langsam ändert, ist ein großes dt notwendig und in Bereichen, in denen sich das System schnell ändert, ein kleines dt.
Dieses Problem zeigte sich besonders darin, dass das Programm Übergänge zwischen Zuständen berechnete, die nicht aneinander grenzen. Übertragen würde dies bedeuten, dass ein Kondensator z.B. von „ein Volt“ auf „drei Volt“ kommen könnte ohne dazwischen den Wert „zwei Volt“ zu erreichen. Dieses Verhalten ist in Abbildung 4.1 zu erkennen.
Um die Zeit dt für die Testvektoren eines Zustands dynamisch anzupassen, gibt es zwei denkbare einfache Ansätze:
1. Man wählt generell ein kleines Standard-dt und versucht zu erkennen, für welche Zustände es vergrößert werden sollte.
2. Man wählt ein großes Standard-dt und versucht zu erkennen, wann Zustände übersprungen werden. In diesen Fällen verkleinert man die Zeit dt für den entsprechenden Startzustand.
Da es bei der ersten Methode möglich ist, die Zeit dt unter Umständen so groß werden zu lassen, dass wiederum ein Zustand übersprungen wird, müsste man hierbei ebenfalls die Überprüfung nach Zustandübersprüngen folgen lassen. Da in beiden Fällen nach übersprungenen Zuständen getestet werden musste, wurde nur die zweite Methode implementiert.
Zusammenfassung der Kapitel
1 Motivation: Einführung in die Problematik der Verifikation nichtlinearer, analoger Schaltungen und Zielsetzung der Studienarbeit.
2 Formale Verifikation analoger Schaltungen: Erläuterung der Grundlagen des Model-Checkings und der Notwendigkeit einer Diskretisierung analoger Schaltungen durch Meta-Zustände.
3 Das bestehende Programm: Beschreibung der Funktionsweise der Initialaufteilung des Zustandsraums, der Ermittlung von Testvektoren und der Erstellung von Zustandsautomaten.
4 Erweiterungen des Programms: Detaillierte Darstellung der Verbesserungen, insbesondere der dynamischen Zeit-Anpassung, des Umgangs mit ungültigen Vektoren und der Verfeinerung der Zustandsaufteilung.
5 Das Komplexitätsproblem: Behandlung des exponentiellen Anstiegs der Zustandsanzahl und Strategien zur Reduktion der Komplexität mittels Wahrscheinlichkeitskriterien.
6 Eingangssignale: Implementierung von periodischen und digitalen Eingangssignalen als zusätzliche Dimensionen im Zustandsraum für eine erweiterte Verifikation.
Schlüsselwörter
Formale Verifikation, Model-Checking, analoge Schaltungen, Zustandsraum, Meta-Zustände, Testvektoren, Zustandsautomat, Zeitsteuerung, Schwingkreis, Komplexitätsproblem, Eingangssignale, Zustandsaufteilung, VHDL, Diskretisierung, Verifikationszeit.
Häufig gestellte Fragen
Worum geht es in der Arbeit grundlegend?
Die Arbeit befasst sich mit der formalen Verifikation von analogen und gemischt analog/digitalen Schaltungen unter Verwendung von Model-Checking-Ansätzen.
Welche zentralen Themenfelder werden bearbeitet?
Die Hauptthemen umfassen die Diskretisierung kontinuierlicher Zustandsräume, die effiziente Erzeugung von Zustandsautomaten und die Handhabung unterschiedlicher Eingangssignaltypen.
Was ist das primäre Ziel der Untersuchung?
Das primäre Ziel ist die Verbesserung eines bestehenden Verifikationsprogramms, um physikalisches Systemverhalten präziser abzubilden und die Berechnungszeit bzw. Zustandsanzahl zu optimieren.
Welche wissenschaftliche Methode kommt zum Einsatz?
Es wird das Model-Checking-Verfahren genutzt, ergänzt durch mathematische Ansätze zur Zustandsraumzerlegung mittels Hyperboxen und dynamischer Zeit-Anpassung.
Was sind die inhaltlichen Schwerpunkte des Hauptteils?
Der Hauptteil konzentriert sich auf die algorithmischen Erweiterungen der Software, insbesondere zur Vermeidung von Fehlern bei der Simulation und zur Bewältigung der Berechnungskomplexität.
Welche Schlüsselbegriffe definieren die Arbeit?
Wichtige Begriffe sind Meta-Zustände, Testvektoren, Zustandsautomaten und die dynamische Anpassung der Simulationszeit dt.
Wie werden ungerechtfertigte Selbstverweise in der Verifikation behandelt?
Das Programm führt eine zusätzliche Funktion aus, die Testpunkte prüft; falls ein Testpunkt in seinem Startzustand endet, wird dessen Validität durch eine Vektorverlängerung verifiziert.
Wie werden digitale Eingangssignale in das bestehende Modell integriert?
Dies erfolgt durch eine Teilung des dreidimensionalen Zustandsraums in der dritten Dimension, wobei eine Hälfte für den Eingangswert U-Low und die andere für U-High reserviert ist.
- Quote paper
- Christoph Holzbaur (Author), 2006, Erweiterung der Simulation um die formale Verifikation von Schaltungen mit analogen und gemischt analog-digitalen Eingangssignalen, Munich, GRIN Verlag, https://www.grin.com/document/186358
