Excerpt
Studienarbeit
Erweiterung der Simulation um die
formale Verifikation von Schaltungen
mit analogen und gemischt
analog/digitalen Eingangssignalen
Christoph Holzbaur
Matr. 959821
Technische Universit¨at Darmstadt
24. Oktober 2006
Technische Universit¨at Darmstadt
Fachgebiet Rechnersysteme
Inhaltsverzeichnis
Inhaltsverzeichnis
Inhaltsverzeichnis
I
Abbildungsverzeichnis
III
1 Motivation
1
2 Formale Verifikation analoger Schaltungen
2
3 Das bestehende Programm
5
3.1 Initialaufteilung des Zustandsraums . . . . . . . . . . . . . . . . . .
5
3.2 Ermittlung der Testvektoren . . . . . . . . . . . . . . . . . . . . . .
6
3.3 Weitere Aufteilung des Zustandsraums . . . . . . . . . . . . . . . .
6
3.4
¨
Uberg¨ange berechnen . . . . . . . . . . . . . . . . . . . . . . . . . .
8
3.5 Die Ausgabe . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
9
4 Erweiterungen des Programms
11
4.1 Dynamische Anpassung der Zeit . . . . . . . . . . . . . . . . . . . .
11
4.1.1
Erkennung von ¨ubersprungenen Zust¨anden . . . . . . . . . .
12
4.1.2
Das Verhalten wenn ein Zustand ¨ubersprungen wurde . . . .
13
4.1.3
Ung¨ultige Vektoren . . . . . . . . . . . . . . . . . . . . . . .
14
4.2 Auffinden von ungerechtfertigten Selbstverweisen
. . . . . . . . . .
15
4.3 Berechnen der ¨
Ubergangszeit . . . . . . . . . . . . . . . . . . . . . .
17
4.4 Weitere Zustandsaufteilungen . . . . . . . . . . . . . . . . . . . . .
18
4.4.1
Der Zustand-Vektorwinkel-Vergleich . . . . . . . . . . . . . .
20
4.4.2
Der Zustand-Vektorl¨angen-Vergleich . . . . . . . . . . . . .
21
4.4.3
Problem mit dem Zustand-Vektorl¨angen-Vergleich . . . . . .
22
4.4.4
Ergebnis der neuen Zustandsaufteilungen . . . . . . . . . . .
23
-I-
Inhaltsverzeichnis
5 Das Komplexit¨
atsproblem
27
5.1 Angabe einer Grenzwahrscheinlichkeit . . . . . . . . . . . . . . . . .
28
5.2 Angabe einer Mindestwahrscheinlichkeit
. . . . . . . . . . . . . . .
29
5.3 Auswahl einer Nachfolgedimension
. . . . . . . . . . . . . . . . . .
30
5.4 Ergebnis der Verbesserungen . . . . . . . . . . . . . . . . . . . . . .
31
5.5 Weiterhin bestehende Probleme . . . . . . . . . . . . . . . . . . . .
34
6 Eingangssignale
35
6.1 Schaltungen mit (periodischen) Eingangssignalen . . . . . . . . . .
35
6.2 Erweiterung auf analoge Schaltungen mit digitalen Eingangssignalen
38
6.2.1
Der Zustandsraum . . . . . . . . . . . . . . . . . . . . . . .
39
6.2.2
Vektoren berechnen . . . . . . . . . . . . . . . . . . . . . . .
40
6.2.3
Zust¨ande einteilen . . . . . . . . . . . . . . . . . . . . . . . .
41
6.2.4
Ergebnis . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
42
Literaturverzeichnis
44
-II-
Abbildungsverzeichnis
Abbildungsverzeichnis
2.1 Zustandsraum f¨ur eine RLC-Schaltung mit Eingangsspannung . . .
3
2.2 Meta-Zustand f¨ur eine RLC-Schaltung mit Eingangsspannung . . .
4
3.1 Zustandsaufteilung im zweidimensionalen Raum . . . . . . . . . . .
6
3.2 Aufgeteilter Zustandsraum . . . . . . . . . . . . . . . . . . . . . . .
7
3.3 Graphische Ausgabe der ¨
Uberg¨ange . . . . . . . . . . . . . . . . . .
8
3.4 Teil des zu Abbildung 3.3 geh¨orenden Zustandsautomaten . . . . .
9
3.5 Zustandsraum einer RLC-Schaltung mit Eingangsspannung . . . . .
9
4.1
¨
Ubersprungener Zustand . . . . . . . . . . . . . . . . . . . . . . . .
12
4.2 Testen auf Nachbarschaft . . . . . . . . . . . . . . . . . . . . . . . .
13
4.3 Ungerechtfertigte Selbstverweise . . . . . . . . . . . . . . . . . . . .
16
4.4 Testen auf regul¨are Selbstverweise . . . . . . . . . . . . . . . . . . .
17
4.5 Geschwindigkeiten der ¨
Uberg¨ange . . . . . . . . . . . . . . . . . . .
18
4.6 Schaltkreis mit zwei Kondensatoren . . . . . . . . . . . . . . . . . .
18
4.7 PSpice-Simulation der Schaltung
. . . . . . . . . . . . . . . . . . .
19
4.8 Problem bei der Zustandsaufteilung . . . . . . . . . . . . . . . . . .
20
4.9 Zustand-Vektorwinkel-Vergleich . . . . . . . . . . . . . . . . . . . .
21
4.10 Teilung beim Zustand-Vektorwinkel-Vergleich . . . . . . . . . . . .
21
4.11 Zustand-Vektorl¨angen-Vergleich . . . . . . . . . . . . . . . . . . . .
22
4.12 Problem mit dem Zustand-Vektorl¨angen-Vergleich . . . . . . . . . .
23
4.13 Flussdiagramm f¨ur die L¨osung des Problems . . . . . . . . . . . . .
24
4.14 Alte Zustandsaufteilung . . . . . . . . . . . . . . . . . . . . . . . .
25
4.15 Neue Zustandsaufteilung . . . . . . . . . . . . . . . . . . . . . . . .
26
5.1 Kein Nachfolger wird ausgew¨ahlt . . . . . . . . . . . . . . . . . . .
28
5.2 Falsche Richtung wird gew¨ahlt . . . . . . . . . . . . . . . . . . . . .
29
-III-
Abbildungsverzeichnis
5.3 Vergleich der Richtungen . . . . . . . . . . . . . . . . . . . . . . . .
30
5.4 Verschiedene Bewertungsgrundlagen . . . . . . . . . . . . . . . . . .
31
5.5 Schaltung des ged¨ampften Schwingkreises . . . . . . . . . . . . . . .
32
5.6 Ausgabe f¨ur den ged¨ampften Schwingkreis . . . . . . . . . . . . . .
33
5.7 Schaltung des unged¨ampften Schwingkreises . . . . . . . . . . . . .
33
5.8 Ausgabe f¨ur den unged¨ampften Schwingkreis . . . . . . . . . . . . .
34
6.1 Aufladung eines Kondensators . . . . . . . . . . . . . . . . . . . . .
36
6.2 Test mit einer Sinus-Spannung . . . . . . . . . . . . . . . . . . . . .
38
6.3 Zustandsraum f¨ur eine Schaltung mit digitaler Eingangsspannung .
39
6.4 Verwendung der Zustandsautomaten . . . . . . . . . . . . . . . . .
41
6.5 Ged¨ampfter Schwingkreis mit digitalem Eingangssignal . . . . . . .
42
6.6 Zustandsaufteilung f¨ur U = U
low
. . . . . . . . . . . . . . . . . . . .
43
6.7 Zustandsaufteilung f¨ur U = U
high
. . . . . . . . . . . . . . . . . . .
43
-IV-
KAPITEL 1. MOTIVATION
1 Motivation
In der digitalen Welt ist die Formale Verifikation von Schaltungen sehr verbrei-
tet und wird mit Erfolg eingesetzt. Die Verifikation von nichtlinearen, analogen
Schaltungen hingegen ist noch neu. In Schaltkreisen mit digitalen wie auch ana-
logen Teilen entstehen im analogen Anteil ungef¨ahr 50% der Fehler, die zu einer
Neuimplementierung f¨uhren[4]. Daher ist es von großem Interesse den analogen Teil
ebenfalls verifizieren zu k¨onnen.
Dieser Text entstand im Zuge einer Studienarbeit im Bereich Rechnersysteme an
der Technischen Universit¨at 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¨andigen und effizienter zu
gestalten. Dieser verwendete Ansatz von Scholz [5] und Ehrenfried [1] basiert auf
der Arbeit von Hartong [2, 3].
Im Zuge der Arbeit wurde weiterhin untersucht, inwiefern sich der verwendete An-
satz um die M¨oglichkeit der Verifikation von analogen Schaltungen mit verschiede-
nen Arten von Eingangssignalen erweitern l¨asst.
-1-
KAPITEL 2. FORMALE VERIFIKATION ANALOGER SCHALTUNGEN
2 Formale Verifikation analoger
Schaltungen
Unter Formaler Verifikation (von lat. veritas, Wahrheit) wird der mathematisch
logische Beweis verstanden, dass eine Implementierung alle in einer vorgegebenen
Spezifikation geforderten Eigenschaften aufweist.
Ein bekanntes Verfahren der Formalen Verifikation ist das Model-Checking. Es
dient zur Verifikation von Systemmodellen und ist im Bereich der Verifikation von
digitalen Schaltungen sehr verbreitet. Die Systembeschreibung erfolgt hierbei durch
einen endlichen Automaten, welcher aus Zust¨anden und ¨
Uberg¨angen besteht.
Da eine analoge Schaltung mit kontinuierlichen Werten arbeitet und somit nicht
durch Zust¨ande und ¨
Uberg¨ange beschrieben werden kann, muss man sich ¨uberlegen
wie man einen solchen Schaltkreis so diskretisieren kann, dass eine Verifikation
m¨oglich ist.
Gesucht wird also einerseits eine sinnvolle Zusammenfassung der unendlichen Zahl
von Zust¨anden eines Schaltkreises in eine begrenzte Anzahl von Meta-Zust¨anden,
sowie eine M¨oglichkeit die ¨
Uberg¨ange zwischen diesen Zust¨anden zu erzeugen.
F¨ur die Ermittlung der Meta-Zust¨ande ist es notwendig zu wissen, welche Eigen-
schaften eines analogen Schaltkreises ¨uberhaupt einen Zustand definieren. Abgese-
hen von den Eingangsspannungen und -str¨omen ist ein analoger Schaltkreis durch
die Energie in seinen Energiespeichern eindeutig bestimmt. Diese Energiespeicher
sind hierbei die Kondensatoren wie auch die Spulen. Die Energie einer Spule wird
durch den Strom, der durch sie fließt und die Energie des Kondensators durch die
an ihm anliegende Spannung gekennzeichnet.
-2-
KAPITEL 2. FORMALE VERIFIKATION ANALOGER SCHALTUNGEN
F¨ur jeden Energiespeicher und jedes Eingangssignal erh¨oht sich demnach die Di-
mension des Zustandsraums um eins. Der Zustandsraum eines RLC-Schaltkreises
1
mit der Eingangsspannung U
Eingang
ist in Abbildung 2.1 dargestellt, wobei der
Punkt Z einen beliebigen Zustand des RLC-Schaltkreises darstellt
I
Spule
U
Kondensator
U
Eingang
Z
Abbildung 2.1: Zustandsraum f¨ur eine RLC-Schaltung mit Eingangsspannung
Dieser Zustandsraum besteht naturgem¨aß aus einer unendlichen Anzahl an m¨ogli-
chen Zust¨anden. Um diese Zust¨ande zu einer begrenzten Anzahl an Meta-Zust¨an-
den zusammen zu fassen, m¨ussen folgende Schritte durchgef¨uhrt werden:
·
Begrenzung des unendlichen Zustandsraums auf endliche Werte.
·
Einteilung des nun begrenzten Zustandsraums in mehrere zueinander dis-
junktive Meta-Zust¨ande.
Die Begrenzung des Zustandsraums ist vergleichsweise einfach, da jedem Schaltkreis
physikalische Grenzen gesetzt sind. Jeder Kondensator wie auch jede Spule haben
ihre maximale Spannung bzw. ihren maximalen Strom. Diese Werte begrenzen den
Zustandsraum.
Bei der Aufteilung des Raums in mehrere Meta-Zust¨ande muss beachtet werden,
dass keine ¨
Uberschneidungen und keine L¨ucken zwischen diesen Zust¨anden ent-
stehen. Bei einem n-dimensionalen Zustandsraum bietet es sich daher an, ihn mit
n-dimensionalen Hyperboxen aufzuf¨ullen. Eine solche Hyperbox im Zustandsraum
1
Ein Widerstand, eine Spule und ein Kondensator
-3-
KAPITEL 2. FORMALE VERIFIKATION ANALOGER SCHALTUNGEN
des RLC-Kreises aus Abbildung 2.1 ist in Abbildung 2.2 dargestellt. Ein Vorteil
dieser Hyperboxen ist, dass jeder Meta-Zustand durch die Zuteilung einer Ober-
und einer Untergrenze in jeder Dimension eindeutig gekennzeichnet wird. Die Un-
tergrenze des Zustands S in Dimension d wird hier Zustand [s].ug[d ] und die Ober-
grenze Zustand [s].ug[d ] genannt.
I
Spule
U
Kondensator
U
Eingang
Abbildung 2.2: Meta-Zustand f¨ur eine RLC-Schaltung mit Eingangsspannung
Um den f¨ur die Verifikation mit Hilfe des Modell-Checkings notwendigen Zustands-
automaten zu erhalten, m¨ussen als weiterer Schritt die ¨
Uberg¨ange zwischen den
neu erzeugten Meta-Zust¨anden ermittelt werden. Hierf¨ur werden in jedem Meta-
Zustand Testpunkte erzeugt, f¨ur die das Verhalten des Systems simuliert wird.
Dieses Verhalten kann nun auf den jeweiligen Meta-Zustand hoch gerechnet wer-
den.
-4-
KAPITEL 3. DAS BESTEHENDE PROGRAMM
3 Das bestehende Programm
Da diese Arbeit auf einem schon existierenden Programm aufbaut, welches die
zuvor genannten Schritte durchf¨uhrt, wird in diesem Kapitel zun¨achst erl¨autert,
wie dieses Programm die einzelnen Schritte implementiert.
3.1 Initialaufteilung des Zustandsraums
Der erste Schritt des Programms ist die Aufteilung des Zustandsraums in gleich
große Meta-Zust¨ande. Dies wird erreicht, indem der Zustandsraum mittig in ei-
ner Dimension geteilt wird. Die entstehenden Zust¨ande werden nun in einer der
n¨achsten Dimensionen wiederum mittig geteilt. Dieser Vorgang wird so oft wieder-
holt, bis die gew¨unschte Anzahl an Zust¨anden erreicht ist. Durch dieses Vorgehen
erh¨alt man eine gleichm¨aßige Verteilung der Zust¨ande wie sie in Abbildung 3.1 f¨ur
den zweidimensionalen Fall gezeigt ist.
Je h¨oher die Anzahl der Teilungen ist, desto homogener werden die Zust¨ande
bez¨uglich ihres Systemverhaltens. Da jedoch durch die oben beschriebene Metho-
de auch Zust¨ande geteilt werden, die schon homogen sind, versucht das Programm
nach einer Initialaufteilung nur noch diejenigen Zust¨ande zu teilen, die ein inhomo-
genes Verhalten aufweisen. F¨ur diesen Zweck bestimmt das Programm Testvektoren
und vergleicht diese miteinander.
-5-
Excerpt out of 49 pages
- 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
Similar texts
Publish now - it's free
✕
Excerpt from
49
pages
Comments