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

Das gezeigte Bild gibt einen Eindruck, wie zwei Systeme, die in unterschiedlicher Darstellung vorliegen (Spezifikation in funktioneller Sicht, Realisierung in struktureller Sicht jeweils auf Gatterebene) über die Beschreibungsform BDD miteinander verglichen werden können.

Wichtig ist, dass zum Beweis ihrer Übereinstimmung keinerlei Stimuli benötigt werden, man spricht deshalb beim Equivalence Checking auch von einer statischen Verifikationsmethode.

Für sequentielle Systemteile ist das Equivalence Checking deutlich schwieriger. In der Praxis kann es nur für Sonderfälle oder für kleine Beispiele verwendet werden. In diesem Script wird daher darauf auch nicht eingegangen.