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
- Abbildungsverzeichnis
- 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
- 4.1 Dynamische Anpassung der Zeit
- 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
- Literaturverzeichnis
Zielsetzung und Themenschwerpunkte
Die vorliegende Studienarbeit befasst sich mit der Erweiterung eines Programms zur formalen Verifikation von analogen Schaltungen. Ziel ist es, die Simulation um die Möglichkeit zu erweitern, analoge und gemischt analog/digitale Eingangssignale zu verarbeiten. Die Arbeit untersucht verschiedene Ansätze zur Erweiterung des bestehenden Programms, um die Komplexität der Simulation zu bewältigen und die Genauigkeit der Ergebnisse zu verbessern.
- Formale Verifikation analoger Schaltungen
- Dynamische Anpassung der Zeit
- Zustandsaufteilung
- Komplexitätsproblem
- Eingangssignale
Zusammenfassung der Kapitel
Kapitel 1 führt in die Thematik der formalen Verifikation analoger Schaltungen ein und erläutert die Motivation für die Erweiterung des bestehenden Programms. Kapitel 2 beschreibt die Grundlagen der formalen Verifikation analoger Schaltungen und stellt die Herausforderungen dar, die bei der Verarbeitung von analogen und gemischt analog/digitalen Eingangssignalen auftreten. Kapitel 3 präsentiert das bestehende Programm und seine Funktionsweise. Es werden die einzelnen Schritte der Simulation erläutert, von der Initialaufteilung des Zustandsraums bis zur Ausgabe der Ergebnisse. Kapitel 4 befasst sich mit den Erweiterungen des Programms, die notwendig sind, um die Verarbeitung von analogen und gemischt analog/digitalen Eingangssignalen zu ermöglichen. Es werden verschiedene Ansätze zur dynamischen Anpassung der Zeit, zur Zustandsaufteilung und zur Berechnung der Übergangszeit vorgestellt. Kapitel 5 analysiert das Komplexitätsproblem, das bei der Simulation von analogen Schaltungen mit komplexen Eingangssignalen auftritt. Es werden verschiedene Ansätze zur Reduzierung der Komplexität und zur Verbesserung der Effizienz der Simulation diskutiert. Kapitel 6 behandelt die Erweiterung des Programms auf Schaltungen mit analogen und gemischt analog/digitalen Eingangssignalen. Es werden die notwendigen Anpassungen des Zustandsraums, der Vektorberechnung und der Zustandsaufteilung beschrieben.
Schlüsselwörter
Die Schlüsselwörter und Schwerpunktthemen des Textes umfassen die formale Verifikation, analoge Schaltungen, gemischt analog/digitale Eingangssignale, Zustandsraum, Zustandsaufteilung, dynamische Anpassung der Zeit, Komplexitätsproblem, Simulation, Testvektoren, Übergangszeit, Eingangssignale.
- Citar trabajo
- Christoph Holzbaur (Autor), 2006, Erweiterung der Simulation um die formale Verifikation von Schaltungen mit analogen und gemischt analog-digitalen Eingangssignalen, Múnich, GRIN Verlag, https://www.grin.com/document/186358
