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

Statt ein Erfüllbarkeitsproblem zu untersuchen, kann man beim Equivalence Checking versuchen, die beiden Systeme direkt miteinander zu vergleichen. Dazu bildet man die Systeme jeweils auf einen Graphen ab und versucht, die Isomorphie der beiden Graphen zu beweisen. Damit dies möglich ist (das generelle Graphenisomorphieproblem ist NP-vollständig), muss eine eindeutige (kanonische) Darstellung gefunden werden. Diese ist durch so genannte binäre Entscheidungsgraphen Binary Decision Diagrams (BDDs) gegeben.