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

Im Gegensatz zur Simulation, die aufgrund der endlichen Anzahl von Stimuli stets experimentellen Charakter hat, liefern die Methoden der formalen Verifikation einen mathematischen Beweis. Auf diese Weise können nicht nur Fehler im Entwurf gefunden, sondern es kann auch die Fehlerfreiheit eines Entwurfs bewiesen werden.