Verifikation digitaler Systeme (VdS)5 ECTS
(englische Bezeichnung: Verification of Digital Systems)

Lehrveranstaltungen:

• • Verifikation digitaler Systeme
    (Vorlesung, 2 SWS, Oliver Keszöcze, Mi, 16:15 - 17:45, 00.152-113)
  • Übung zur Verifikation digitaler Systeme
    (Übung, 2 SWS, Oliver Keszöcze, Mo, 14:15 - 15:45, 00.152-113)

Inhalt:

Für den Entwurf eines digitalen Systems werden heute in der Industrie ebenso viele Verifikationsingenieure wie Designer benötigt. Trotzdem beansprucht die Verifikation heute bereits 70%-80% der gesamten Entwurfszeit. Neben konventionellen Verifikationserfahren wie der Simulation sind werden seit einigen Jahren sogenannte "formale Verifikationsmethoden" in heutigen Entwursflüssen eingesetzt. Der Umgang mit diesen Methoden stellt ein wichtiges neues Aufgabenfeld dar. Im Gegensatz zur Simulation beruht die formale Verifikation auf exakten mathematischen Methoden zum Nachweis funktionaler Schaltungseigenschaften. Dadurch können Entwurfsfehler frühzeitiger und mit höherer Zuverlässigkeit als bisher erkannt werden. Jedes System zur formalen Hardwareverifikation erfordert:
1. ein geeignetes Modell des zu verifizierenden Systems
2. eine Sprache zur Formulierung der zu verifizierenden Eigenschaften
3. eine Beweismethode.
Die Vorlesung behandelt diese drei Bereiche, vermittelt die grundlegenden Algorithmen und Konzepte moderner Werkzeuge für die formale Hardwareverifikation und erläutert deren Einsatz in der industriellen Praxis. Im Einzelnen werden in dieser Vorlesung die folgenden Punkte behandelt:
1. Modellierung digitaler Systeme
2. Unterschiede formaler und simulationsbasierter Verifikationsmethoden
3. Äquivalenzvergleich
4. Formale und simulationsbasierte Eigenschaftsprüfung
5. Assertions
6. Verifikation arithmetischer Schaltungen

Lernziele und Kompetenzen:

Verstehen

• Die Studierenden erläutern die wesentlichen Techniken zur Verifikation digitaler Systeme, zeigen deren Vor- und Nachteile auf und vergleichen diese bezüglich Ihrer Mächtigkeit und Komplexität.

Anwenden

• Die Studierenden wenden Modellierungstechniken aus den Bereichen der Binären Entscheidungsdiagramme inkl. bekannter Erweiterungen (MDD, etc.) sowie der SAT-Löser auf Systembeschreibungen an.

• Die Studierenden Verifikationstechniken aus den Bereichen der formalen Äquivalenz- und Eigenschaftsprüfung (Model Checking, Symbolic Model Checking, Bounded Model Checking) auf Systembeschreibungen an.

Verwendbarkeit des Moduls / Einpassung in den Musterstudienplan:
Das Modul ist im Kontext der folgenden Studienfächer/Vertiefungsrichtungen verwendbar:

1. 123#67#H
   (Po-Vers. 2008 | TechFak | Computational Engineering (Master of Science with Honours) | Gesamtkonto | Wahlpflichtbereich Informatik | Verifikation digitaler Systeme)
2. Artificial Intelligence (Master of Science)
   (Po-Vers. 2021s | TechFak | Artificial Intelligence (Master of Science) | Gesamtkonto | Wahlpflichtmodulbereich | Symbolic Artificial Intelligence | Verifikation digitaler Systeme)
3. Computational Engineering (Rechnergestütztes Ingenieurwesen) (Bachelor of Science)
   (Po-Vers. 2007 | TechFak | Computational Engineering (Rechnergestütztes Ingenieurwesen) (Bachelor of Science) | alte Prüfungsordnungen | Gesamtkonto | Technische Wahlmodule | Verifikation digitaler Systeme)
4. Computational Engineering (Rechnergestütztes Ingenieurwesen) (Bachelor of Science)
   (Po-Vers. 2009 | TechFak | Computational Engineering (Rechnergestütztes Ingenieurwesen) (Bachelor of Science) | alte Prüfungsordnungen | Gesamtkonto | Technische Wahlmodule | Verifikation digitaler Systeme)
5. Computational Engineering (Rechnergestütztes Ingenieurwesen) (Bachelor of Science)
   (Po-Vers. 2010 | TechFak | Computational Engineering (Rechnergestütztes Ingenieurwesen) (Bachelor of Science) | Gesamtkonto | Technische Wahlmodule | Verifikation digitaler Systeme)
6. Computational Engineering (Rechnergestütztes Ingenieurwesen) (Master of Science)
   (Po-Vers. 2008 | TechFak | Computational Engineering (Rechnergestütztes Ingenieurwesen) (Master of Science) | Gesamtkonto | Wahlpflichtbereich Informatik | Verifikation digitaler Systeme)
7. Informatik (Bachelor of Arts (2 Fächer))
   (Po-Vers. 2010 | TechFak | Informatik (Bachelor of Arts (2 Fächer)) | Vertiefung Informatik I und II | Vertiefungsmodul Hardware-Software-Co-Design | Verifikation digitaler Systeme)
8. Informatik (Bachelor of Arts (2 Fächer))
   (Po-Vers. 2013 | TechFak | Informatik (Bachelor of Arts (2 Fächer)) | Vertiefung Informatik I und II | Vertiefungsrichtung Hardware-Software-Co-Design | Verifikation digitaler Systeme)
9. Informatik (Bachelor of Science)
   (Po-Vers. 2009s | TechFak | Informatik (Bachelor of Science) | Wahlpflichtbereich (5. und 6. Semester) | Wahlpflichtmodule | Vertiefungsrichtung Hardware-Software-Co-Design | Verifikation digitaler Systeme)
10. Informatik (Bachelor of Science)
    (Po-Vers. 2009w | TechFak | Informatik (Bachelor of Science) | Gesamtkonto | Wahlpflichtbereich (5. und 6. Semester) | Wahlpflichtmodule | Vertiefungsrichtung Hardware-Software-Co-Design | Verifikation digitaler Systeme)
11. Informatik (Bachelor of Science)
    (Po-Vers. 2022w | TechFak | Informatik (Bachelor of Science) | Gesamtkonto | Wahlpflichtbereich (Wahlpflichtmodule aus mind. 2 Vertiefungsrichtungen) | Vertiefungsrichtung Hardware-Software-Co-Design | Verifikation digitaler Systeme)
12. Informatik (Master of Science)
    (Po-Vers. 2010 | TechFak | Informatik (Master of Science) | Gesamtkonto | Wahlpflichtbereich | Säule der systemorientierten Vertiefungsrichtungen | Vertiefungsrichtung Hardware-Software-Co-Design | Verifikation digitaler Systeme)
13. Information and Communication Technology (Master of Science)
    (Po-Vers. 2019s | TechFak | Information and Communication Technology (Master of Science) | Gesamtkonto | Wahlmodule | Wahlmodule aus dem Angebot von EEI und Informatik | Verifikation digitaler Systeme)
14. Informations- und Kommunikationstechnik (Master of Science)
    (Po-Vers. 2010 | TechFak | Informations- und Kommunikationstechnik (Master of Science) | Gesamtkonto | Wahlbereiche, Praktika, Seminar, Masterarbeit | Wahlmodule aus dem Angebot von EEI und Informatik | Verifikation digitaler Systeme)
15. Informations- und Kommunikationstechnik (Master of Science)
    (Po-Vers. 2016s | TechFak | Informations- und Kommunikationstechnik (Master of Science) | Gesamtkonto | Wahlbereiche, Praktika, Seminar, Masterarbeit | Wahlmodule aus dem Angebot von EEI und Informatik | Verifikation digitaler Systeme)
16. Mathematik (Bachelor of Science)
    (Po-Vers. | NatFak | Mathematik (Bachelor of Science) | Module des Nebenfachs | Nebenfach Informatik | Vertiefungsmodule | Vertiefungsrichtung Hardware-Software-Co-Design | Verifikation digitaler Systeme)
17. Mathematik (Bachelor of Science)
    (Po-Vers. 2019w | NatFak | Mathematik (Bachelor of Science) | weitere Module der Bachelorprüfung | Module des Nebenfachs | Nebenfach Informatik | Vertiefungsmodule | Vertiefungsrichtung Hardware-Software-Co-Design | Verifikation digitaler Systeme)

Studien-/Prüfungsleistungen:

Verifikation digitaler Systeme (Prüfungsnummer: 22801)

Prüfungsleistung, mündliche Prüfung, Dauer (in Minuten): 30, benotet, 5 ECTS

Anteil an der Berechnung der Modulnote: 100.0 %

Erstablegung: WS 2022/2023, 1. Wdh.: SS 2023

1. Prüfer:

Oliver Keszöcze