Diese Arbeit baut auf einem Programm auf, das einen analogen Schaltkreis in das entsprechende VHDL-Modell zur späteren formalen Verifikation überführt. Das Programm wurde an der Technischen Universität in Darmstadt im Fachbereich Rechnersysteme entwickelt und ist durch die Erfolge dieser Arbeit letztendlich einsatzbereit.
Inhaltsverzeichnis
1 Einleitung
1.1 Formale Verifikation analoger Schaltungen
1.2 Das bestehende Programm
2 Ziele dieser Diplomarbeit
2.1 Vergleichbarkeit mit den Ergebnissen anderer Arbeiten
2.2 Ausnutzung des Zustandsraums
2.3 Maximale Anzahl an Zuständen
2.4 Rechenzeit
3 Vergleichbarkeit zu anderen Arbeiten herstellen
3.1 Mehrere Startpunkte
3.2 Neue Methode zur Berechnung der Nachfolger
3.3 Wiederverwendung der Ergebnisse
4 Bessere Verwendung der verfügbaren Zustandsanzahl
4.1 Adaptive Anpassung des Zustandsraums
4.2 Eingrenzung des Zustandsraums
5 Optimierung der Speicherorganisation
5.1 Einführung in die Speicherverwaltung von C++
5.1.1 Structs
5.1.2 Stack und Heap
5.1.3 Vektoren, Listen und die STL
5.2 Die Speicherorganisation vor Beginn der Arbeit
5.3 Umstrukturierung der Felder
5.4 Einführung einer dynamischen Speicherverwaltung
5.5 Auslagerung der Übergänge in eine Datei
5.6 Die neue Speicherorganisation
6 Optimierung der Rechenzeit
6.1 Frühe Anpassung des Zeitfaktors
6.2 Optimierungen der Nachbarschaftsprüfung
6.2.1 Optimierung der Schleifen
6.2.2 Optimierungen bei der Berechnung der Nachbarschaft
6.3 Speicherung der Endergebnisse in einer Datei
7 Fazit
A Die Beispiel-Dateien
Zielsetzung & Themen
Diese Arbeit zielt darauf ab, die Leistung und Effizienz eines bestehenden Programms zur formalen Verifikation analoger Schaltungen zu steigern, indem sowohl die Speicherorganisation als auch die Rechengeschwindigkeit signifikant optimiert werden.
- Optimierung der Speicherverwaltung durch dynamische Allokation und Auslagerung
- Verbesserung der Zustandsraum-Aufteilung zur effizienteren Nutzung begrenzter Ressourcen
- Beschleunigung der Berechnung von Zustandsübergängen durch optimierte Nachbarschaftsprüfung
- Anpassung des Zeitfaktors zur präziseren und schnelleren Zustandsmodellierung
- Verbesserung der Vergleichbarkeit mit existierenden Verifikationsmethoden
Auszug aus dem Buch
6.2.2 Optimierungen bei der Berechnung der Nachbarschaft
Durch Beobachtungen konnte man feststellen, dass aufgrund der Veränderung der Zeitfaktoren die Nachbarschaften wiederholt berechnet wurden und dies einen beachtlichen Anteil der Rechenzeit ausmachte. Aus diesem Grunde wurde speziell dieser Teil versucht zu optimieren, da hier das größte Einsparpotential vermutet werden konnte.
6.2.2.1 Zwischenspeicherung von Ergebnissen bei der Berechnung von Nachbarschaftsverhältnissen
Da die Neuberechnung aufgrund eines ungünstigen Zeitfaktors relativ häufig stattfand, wurde das Programm der Art erweitert, dass es die Ergebnisse der Nachbarschaftsprüfung in einem Feld Z_B^i zwischenspeichert. Durch diese Zwischenspeicherung konnte die Berechnung der Nachbarschaft für die wiederholte Betrachtung von Zustand Z_A komplett weggelassen werden.
Die oben beschriebenen Maßnahmen verkürzten die Rechenzeit für das Standard-Beispiel auf 147 Minuten. Dies entspricht nur noch 5,1% der zuvor benötigten Rechenzeit. Der hierfür zusätzlich verwendete Speicherplatz ist minimal, da das Feld Z_B^i für jeden Zustand Z_A wiederverwendet werden kann.
Zusammenfassung der Kapitel
1 Einleitung: Beschreibt die Motivation zur formalen Verifikation analoger Schaltungen und stellt das zugrundeliegende Programm vor.
2 Ziele dieser Diplomarbeit: Definiert die angestrebten Verbesserungen bezüglich Vergleichbarkeit, Speichernutzung, Zustandsanzahl und Rechenzeit.
3 Vergleichbarkeit zu anderen Arbeiten herstellen: Behandelt die Implementierung von mehreren Startpunkten und Methoden zur Nachfolgeberechnung.
4 Bessere Verwendung der verfügbaren Zustandsanzahl: Erläutert die adaptive Anpassung und Eingrenzung des Zustandsraums für eine effizientere Verifikation.
5 Optimierung der Speicherorganisation: Dokumentiert die umfassende Umstrukturierung der Speicherverwaltung hin zu dynamischen Strukturen und Dateiauslagerungen.
6 Optimierung der Rechenzeit: Beschreibt algorithmische Verbesserungen bei der Zustandsberechnung und der effizienten Prüfung von Nachbarschaften.
7 Fazit: Fasst die erreichten Ziele zusammen, insbesondere die deutliche Steigerung der verarbeitbaren Zustandsanzahl und die massiven Rechenzeitverkürzungen.
A Die Beispiel-Dateien: Erläutert die Struktur der für Berechnungen notwendigen Konfigurations- und Parameterdateien.
Schlüsselwörter
formale Verifikation, analoge Schaltungen, Modell-Checking, Zustandsraum, Speicherorganisation, C++, STL, dynamische Speicherverwaltung, Nachbarschaftsprüfung, Zeitfaktor, Rechenzeitoptimierung, VHDL-Modell, Zustandsautomaten
Häufig gestellte Fragen
Worum geht es in dieser Arbeit grundsätzlich?
Die Arbeit beschäftigt sich mit der Optimierung und Performancesteigerung eines Softwareprogramms, das zur formalen Verifikation analoger Schaltungen durch die Generierung von VHDL-Modellen eingesetzt wird.
Was sind die zentralen Themenfelder der Arbeit?
Die Arbeit fokussiert sich primär auf die Bereiche Speicherverwaltung (RAM-Effizienz) und die algorithmische Optimierung der Rechengeschwindigkeit bei der Zustandsraum-Exploration.
Was ist das primäre Ziel oder die Forschungsfrage?
Ziel ist es, das bestehende Programm so zu modifizieren, dass deutlich mehr Zustände in kürzerer Zeit berechnet werden können, um auch größere Schaltungen effizient verifizieren zu können.
Welche wissenschaftlichen Methoden werden verwendet?
Es kommen Ansätze aus dem Model-Checking zur Anwendung, ergänzt durch spezifische C++-Programmiertechniken zur dynamischen Speicherverwaltung und mathematische Optimierungen zur Nachbarschaftsprüfung.
Was wird im Hauptteil behandelt?
Der Hauptteil gliedert sich in die methodische Anpassung der Zustandsraum-Aufteilung, eine vollständige Umstrukturierung der Speicherorganisation (inklusive dynamischer Vektoren und Dateiauslagerung) sowie die Optimierung der Rechenalgorithmen.
Welche Schlüsselwörter charakterisieren die Arbeit am besten?
Formale Verifikation, Zustandsraum-Optimierung, Speicherverwaltung in C++ und effiziente Berechnung von Zustandsübergängen.
Wie wurde das Problem des begrenzten Arbeitsspeichers gelöst?
Durch den Wechsel von statischen Arrays zu dynamischen Speicherstrukturen (STL-Container) und das Auslagern der Zustandsübergänge in externe Dateien konnte der Speicherbedarf drastisch gesenkt werden.
Was bewirkte die Optimierung der Nachbarschaftsprüfung?
Durch die Einführung einer effizienteren Prüfung von Zustandsnachbarschaften und die Zwischenspeicherung von Berechnungsergebnissen konnte die Rechenzeit für Standard-Beispiele auf einen Bruchteil der ursprünglichen Dauer reduziert werden.
- Quote paper
- Christoph Holzbaur (Author), 2007, Optimierung und Performancesteigerung bei der Generierung von VHDL-Modellen analoger Schaltungen, Munich, GRIN Verlag, https://www.grin.com/document/186359
