INF.08071.02 - Entwurf digitaler Schaltungen: Logiksynthese, Formale Verifikation und Fabrikationstest (Teil 1) (Vollständige Modulbeschreibung)

Menü

MLU

INF.08071.02	5 CP
Modulbezeichnung	Entwurf digitaler Schaltungen: Logiksynthese, Formale Verifikation und Fabrikationstest (Teil 1)
Modulcode	INF.08071.02
Semester der erstmaligen Durchführung
Fachbereich/Institut	Institut für Informatik
Verwendet in Studiengängen / Semestern	Informatik (MA120 LP) (Master) > Informatik InformatikMA120, Akkreditierungsfassung gültig ab SoSe 2023 > Basismodule der Vertiefungsrichtung `Technische Informatik und IT-Sicherheit` Wirtschaftsinformatik (Business Information Systems) (MA120 LP) (Master) > Wirtschaftsinformatik WirtschaftsinformatMA120, Akkreditierungsfassung gültig ab WS 2020/21 > 2.2 Informatik
Modulverantwortliche/r
Weitere verantwortliche Personen	Prof. Dr. Paul Molitor/Dr. Jörg Ritter
Teilnahmevoraussetzungen
Kompetenzziele	Studierende sollen durch das Modul folgende Kompetenzen erwerben Sie wissen von der Bedeutung der formalen Verifikation von Hardware und dem Fabrikationstest integrierter Schaltungen. Sie kennen die grundlegenden Ansätze des Model Checking, mit denen eine Hardwarespezifikation auf vorgegebene Eigenschaften geprüft wird. Sie kennen die grundlegenden Ansätze zum formalen Äquivalenztest zweier kombinatorischer bzw. sequentieller Schaltungen. Sie kennen die üblichen in der Industrie verwendeten Fehlermodelle und die Ansätze zur Testmustergenerierung und können diese anwenden. Sie verstehen die prinzipiellen Vorgehensweisen von SAT-Solvern und können diese erklären und anwenden. Sie kennen die grundlegenden rechnerinternen Darstellungen Boolescher Funktionen, insbesondere implizite Darstellungen (BDDs, BMDs) Boolescher Funktionen, und können diese zur Analyse und Verifikation kombinatorischer Schaltungen anwenden. Sie haben verstanden, dass unabhängig von der gewählten Darstellung Boolescher Funktionen fast alle Boolesche Funktionen nicht mit traktablem Platz darstellbar sind.
Modulinhalte	Grundlagen: Rechnerinterne Darstellungen Boolescher Funktionen: Funktionstabelle, Boolesche Ausdrücke, disjunktive Normalform, konjunktive Normalform, Binary Decision Diagrams, Binary Moment Diagrams Grundlagen: Satz von Shannon (Shannon-Effekt) Grundlagen: Operationen auf den rechnerinternen Darstellungen Boolescher Funktionen und ihre Komplexität Grundlagen: Ansätze zum effizienten SAT-Solving Formale Verifikation: Model Checking und Symbolic Model Checking Formale Verifikation: Formaler Äquivalenztest kombinatorischer Schaltungen Fabrikationstest: Fehlermodelle, Fehlersimulation Fabrikationstest: Random Testing, Automatische Testmustergenerierung
Lehrveranstaltungsformen	Vorlesung (4 SWS) Kursus
Unterrichtsprachen	Deutsch, Englisch
Dauer in Semestern	1 Semester Semester
Angebotsrhythmus Modul	jedes Wintersemester
Aufnahmekapazität Modul	unbegrenzt
Prüfungsebene
Credit-Points	5 CP
Modulabschlussnote	LV 1: %; LV 2: %.
Faktor der Modulnote für die Endnote des Studiengangs	1
Hinweise	Basismodul der Vertiefungsrichtung "Technische Informatik und IT-Sicherheit"

Modulveranstaltung	Lehrveranstaltungsform	Veranstaltungstitel	SWS	Workload selbstgestaltete Arbeit	Workload Summe
LV 1	Vorlesung	Vorlesung mit integrierten Übungen	4		0
LV 2	Kursus	Selbststudium: Bearbeiten der Übungsaufgaben und Prüfungsvorbereitung			0
Workload modulbezogen				150	150
Workload Modul insgesamt					150

Prüfung	Prüfungsvorleistung	Prüfungsform
LV 1
LV 2
Gesamtmodul	Aktive Mitarbeit in der Vorlesung und den Übungen	mündliche Prüfung
Wiederholungsprüfung

Regularien	Teilnahmevoraussetzungen	Angebotsrhythmus	Anwesenheitspflicht	Gewicht an Modulnote in %
LV 1		Wintersemester	Nein	%
LV 2		Wintersemester	Nein	%