Formale Verifikation
Formale Verifikation
Simulation und formale Verifikation
Werkzeuge der formalen Verifikation
Equivalence-Checking: Problemstellung
Erfüllbarkeitsproblem(Satisfiability,SAT)
SAT1-Problem
SAT-Equivalence-Checker
Graphenisomorphie
Binary Decision Diagrams (BDDs)
Binärer Entscheidungsbaum: Beispiel
Zusammenfassen identischer Teilbäume
Entfernen überflüssiger Knoten
Abhängigkeit der Knotenanzahl von der Entwicklungsreihenfolge
Vorteile der BDDs
Beispiel:ALU(SN74181)
Model-Checking
Symbolic Model Checking
Zustandsmengen
Temporale Logik
Elemente von CTL
CTL-Syntax
AX und EX
AF and EF
AG und EG
Beispiel: Modulo-3-Zähler
Startseite
Hinweis
: Da Javascript ausgeschaltet ist, sind die Grafiken nicht animiert.
Entfernen überflüssiger Knoten
a
x
x
0
1
a
0
1
b
b
0
1
0
1
c
c
0
1
0
1
0
1
OBDD
a
0
1
b
1
0
c
0
1
0
1
f(
x
) = c (a b + a)
ROBDD
Äquivalente boolesche Funktion: