Verifikation digitaler Systeme - Cheatsheet

Zustandsautomaten in der modellbasierten Verifikation

Definition:

Zustandsautomaten in der modellbasierten Verifikation werden genutzt, um das Verhalten von digitalen Systemen formal zu spezifizieren und zu überprüfen.

Details:

• Zustandsautomat besteht aus Zuständen, Übergängen, Eingaben und Ausgaben.
• Zustandsraum: \(\text{S}\), Eingabemenge: \(\text{I}\), Ausgangsmenge: \(\text{O}\).
• Übergangsfunktion: \(\text{S} \times \text{I} \rightarrow \text{S}\).
• Ausgabefunktion: Mealy-Automat: \(\text{S} \times \text{I} \rightarrow \text{O}\), Moore-Automat: \(\text{S} \rightarrow \text{O}\).
• Verifikation mittels formaler Methoden wie Model Checking.

Festlegung und Anwendung von Verifikationskriterien

Definition:

Festlegung und Anwendung von Verifikationskriterien im Rahmen der Verifikation digitaler Systeme

Details:

• Verifikationskriterien definieren, um sicherzustellen, dass digitale Systeme korrekt funktionieren
• Prüfen der Übereinstimmung mit spezifikationen und anforderungen
• Anwenden formaler Methoden wie Modellprüfung (\textit{model checking}) und formale Beweise
• Nutzung von Simulationen zur Validierung
• Kriterien: Vollständigkeit, Konsistenz, Korrektheit, Leistungsfähigkeit

Logikbasierte Methoden zur Verifikation

Definition:

Logikbasierte Methoden zur Verifikation verwenden mathematische Logikmodelle, um die Korrektheit digitaler Systeme sicherzustellen.

Details:

• Verwendung von formalen Spezifikationen zur Beschreibung des erwarteten Verhaltens.
• Model Checking: Überprüfung, ob ein Modell eines Systems eine gegebene Spezifikation erfüllt.
• Beweistechnik: Mathematischer Beweis, dass ein System eine Spezifikation erfüllt.
• Sat-Solver: Verwenden von logischen SAT-Solvern zur Überprüfung logischer Aussagen.
• SMT-Solver (Satisfiability Modulo Theories): Erweitern von SAT um Weitere Theorien wie Arithmetik.

Automatisierte Beweisverfahren

Definition:

Automatisierte Beweisverfahren sind Werkzeuge zur formalen Verifikation, die mathematische Beweise automatisch erstellen und prüfen.

Details:

• Ziel: Korrektheit beweisen, Fehler finden.
• Verfahren: SAT-Solver, SMT-Solver, Theorembeweiser.
• Formale Modelle: Logiken, Automaten.
• Gängige Tools: Z3, Coq, Isabelle.
• Vorteile: Schneller als manuelle Beweise, hohe Präzision.
• Herausforderungen: Skalierung, Komplexität.

Syntax und Semantik von VHDL und Verilog

Definition:

Syntax und Semantik von VHDL und Verilog - grundlegende Kenntnisse über die Notation und Bedeutung der Sprachelemente zur Beschreibung und Simulation digitaler Systeme.

Details:

• VHDL: Synchrone und asynchrone Prozesse, Konfigurationen, Entwurfseinheiten (Entity, Architecture), Signale und Variablen.
• Verilog: Module, Always-Blöcke, Initial-Blöcke, Netze, Regs.
• Simulation: Unterschiede in der Zeitspezifikation und der Einflüsse auf die Simulationsergebnisse.
• Signifikante Unterschiede in der Syntax: VHDL stark typisiert, Verilog weniger strikt.
• Semantik: Umgang mit Zeit und Signalzuweisungen.
• Verifikation: Testbenches schreiben, funktionale Simulationen durchführen.

Grundkonzepte der temporalen Logik

Definition:

Temporale Logik bezieht sich auf die Nutzung von Logikformeln, um zeitliche Aspekte von Systemen zu modellieren und zu verifizieren.

Details:

• Lineare Temporale Logik (LTL): Modelliert Sequenzen von Zuständen in linearen Zeitachsen. Syntax: \(X\), \(G\), \(F\), \(U\).
• Branching-Time-Logik (CTL): Modelliert verzweigende Zeitachsen. Syntax: \(EX\), \(AX\), \(EG\), \(AG\).
• Zusammengesetzte Operatoren: Kombinationen wie \(E[f U g]\), \(A[G f]\).
• Syntax: Formeln bestehen aus Zustandseigenschaften und temporalen Operatoren.
• Semantik: Beschreibt die Erfüllung von Formeln innerhalb des Modells über Zeit.

Unterscheidung zwischen linearer und verzweigter temporaler Logik

Definition:

Unterschied zwischen LTL (Linear-temporale Logik) und CTL (Berechnungsbaum-Logik)

Details:

• LTL: beschreibt Sequenzen von Zuständen; Formel gilt entlang einer einzigen Zeitleiste.
• CTL: beschreibt Baumstrukturen von Zuständen; Verzweigungen in der Zukunft werden berücksichtigt.
• LTL Basissyntax:
  • \textbf{X}φ (Next φ)
  • \textbf{F}φ (Eventually φ)
  • \textbf{G}φ (Globally φ)
  • φ\textbf{U}ψ (φ Until ψ)
• CTL Basissyntax:
  • \textbf{EX} φ (Existiert Next φ)
  • \textbf{EG} φ (Existiert Globally φ)
  • \textbf{EU} (Existiert φ Until ψ)
  • \textbf{AX} φ (Für alle Next φ)
  • \textbf{AG} φ (Für alle Globally φ)
  • \textbf{AU} (Für alle φ Until ψ)
• LTL ist einfacher, aber weniger ausdrucksstark als CTL.
• CTL kann komplexere temporale Behauptungen modellieren.

Algorithmen und Datenstrukturen im Model Checking

Definition:

Algorithmen und Datenstrukturen, die verwendet werden, um Zustandsräume in formalen Modellen zu durchsuchen und zu verifizieren.

Details:

• Symbolische Model Checking: Nutzt \textbf{BDD}s (Binary Decision Diagrams) zur effizienten Zustandsraumerkundung.
• Explizite Model Checking: Durchläuft den Zustandsraum explizit, oft mit Tiefensuche (\textbf{DFS}) oder Breitensuche (\textbf{BFS}).
• \textbf{LTL}-Model Checking: Verwendet Automaten-Theorie, um lineare temporale Logiken zu verifizieren.
• \textbf{SAT}-basierendes Model Checking: Reduziert das Model Checking auf eine Reihe von Befriedbarkeitsproblemen.
• Abstraktionsverfahren: Reduziert die Komplexität des Zustandsraums, z.B. mittels CEGAR (Counterexample-Guided Abstraction Refinement).