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