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

Binäre Entscheidungsgraphen wurden durch R. E. Bryant entscheidend weiterentwickelt. Mit dieser Art von Graphen lassen sich boolesche Funktionen in einer sowohl kanonischen als auch kompakten Darstellung speichern und verarbeiten.