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

Ein binärer Entscheidungsbaum kann durch zwei Vereinfachungsoperationen vereinfacht werden. Erstens können identische Teilbäume zusammengefasst werden und zweitens können Knoten, von denen beide Kanten auf den selben Folgeknoten zeigen, entfernt werden. Führt man darüber hinaus eine feste Reihenfolge für die booleschen Variablen im Entscheidungsgraphen ein, so entsteht ein geordneter Entscheidungsgraph (Ordered Binary Decision Diagram, OBDD). Der OBDD bildet eine kanonische Darstellung einer booleschen Funktion, die gegenüber den bekannten konjunktiven und disjunktiven kanonischen Normalformen oft kompakter und leichter zu manipulieren ist.