INF.08071.02 - Entwurf digitaler Schaltungen: Logiksynthese, Formale Verifikation und Fabrikationstest (Teil 1) (Complete module description)

INF.08071.02	5 CP
Module label	Entwurf digitaler Schaltungen: Logiksynthese, Formale Verifikation und Fabrikationstest (Teil 1)
Module code	INF.08071.02
Semester of first implementation
Faculty/Institute	Institut für Informatik
Module used in courses of study / semesters	Informatik (MA120 LP) (Master) > Informatik InformatikMA120, Version of accreditation valid from SoSe 2023 > Basismodule der Vertiefungsrichtung `Technische Informatik und IT-Sicherheit` Wirtschaftsinformatik (Business Information Systems) (MA120 LP) (Master) > Wirtschaftsinformatik WirtschaftsinformatMA120, Version of accreditation valid from WS 2020/21 > 2.2 Informatik
Responsible person for this module
Further responsible persons	Dr. Jörg Ritter
Prerequisites
Skills to be acquired in this module	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.
Module contents	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
Forms of instruction	Lecture (4 SWS) Course
Languages of instruction	German, English
Duration (semesters)	1 Semester Semester
Module frequency	jedes Wintersemester
Module capacity	unrestricted
Time of examination
Credit points	5 CP
Share on module final degree	Course 1: %; Course 2: %.
Share of module grade on the course of study's final grade	1
Reference text	Basismodul der Vertiefungsrichtung `Technische Informatik und IT-Sicherheit`

Module course label	Course type	Course title	SWS	Workload of independent learning	Sum workload
Course 1	Lecture	Vorlesung mit integrierten Übungen	4		0
Course 2	Course	Selbststudium: Bearbeiten der Übungsaufgaben und Prüfungsvorbereitung			0
Workload by module				150	150
Total module workload					150

Examination	Exam prerequisites	Type of examination
Course 1
Course 2
Final exam of module	Aktive Mitarbeit in der Vorlesung und den Übungen	mündliche Prüfung
Exam repetition information

Prerequisites and conditions	Prerequisites	Frequency	Compulsory attendance	Share on module grade in percent
Course 1		Winter semester	No	%
Course 2		Winter semester	No	%