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

Unter formaler Verifikation versteht man Verfahren, die die korrekte Funktion eines Systems anhand von mathematischen Methoden nachweisen.

Voraussetzung für die erfolgreiche Anwendung von formalen Methoden zur Entwurfsverifikation ist eine formale Beschreibung des Testobjekts. Schaltungsdarstellungen in einer Hardware-Beschreibungssprache, aber auch strukturelle Darstellungen in Form von Netzlisten, genügen diesen Anforderungen und können somit mit formalen Methoden verifiziert werden.