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)
  • Equivalence Checking für sequentielle Schaltungen mit Hilfe von OBDDs
  • Produktautomat
  • Model-Checking
  • Temporale Logik
  • Elemente von CTL
  • CTL-Syntax
  • CTL-Beispiele
  • AX und EX
  • AF and EF
  • AG und EG
  • Beispiel: Modulo-3-Zähler
Startseite

Für sequentielle Systemteile ist die Abbildung in eine BDD-Beschreibung weniger offensichtlich. Im Wesentlichen werden Beschreibungen für Zustandsmengen und Zustandsübergangsrelationen benötigt. Im Folgenden wird eine Speicherung dieser Daten mithilfe von OBDDs erläutert.

Betrachtet man alle Wertebelegungen des Variablenvektors X einer booleschen Funktion fA, bei der das Ergebnis der Funktion 1 entspricht, so ergibt sich eine Menge von Werten A = {X | fA(X) = 1}. Identifiziert man einen Zustand eines Zustandsautomaten mit jeweils einem dieser Vektoren, können Zustandsmengen durch boolesche Funktionen und damit auch mit OBDDs beschrieben werden. Die boolesche Funktion fA(X) wird als charakteristische Funktion der Wertemenge A bezeichnet.

fA(X) = 1, falls X Element von A oder 0, falls nicht

Zur Beschreibung von Zustandsübergängen muss die Darstellung erweitert werden. Für jeden Zustand X1 bestimmt man einen oder mehrere Folgezustände X2. Das heisst, die Zustandsübergangs-Relation kann beispielsweise als (X1,X2) beschrieben werden.