Zur Hauptnavigation / To main navigation

Zur Sekundärnavigation / To secondary navigation

Zum Inhalt dieser Seite / To the content of this page

Sekundärnavigation / Secondary navigation

Inhaltsbereich / Content

EIT-EIS-560-V-4 (with class project: EIT-EIS-562-M-7)

Verification of Digital Systems

13:45 - 15:15
13:45 - 15:15
Room: 11-241
Room: 11-243

2 hours of lecture / 2 hours of assignments (5 ECTS credits) plus 3 ECTS class project (optional)

Start: Thursday, October 26, 2017



Ensuring functional corectness of a complex System-on-Chip consumes 60-80% of the total design costs. This lecture presents basic principles of formal verification techniques and their application within state-of-the-art design flows. 

  • Graph Representations of Boolean Functions
  • Formal Property Checking an Overview
  • Model checking with Temporal Logic
  • Symbolic Traversal of Finite State Machines
  • SAT-based Property Checking
  • Equivalence Checking



see extra webpage


Adding the Class Project: EIT-EIS-562-M-7

A class project is offered to students with expertise in C++ programming. An additional 3 ECTS (2SWS) can be earned when participating in the class project, see extra webpage.




Gary Hachtel, Fabio Somenzi: Logic Synthesis and Verification Algorithms, Springer, 2010, EIT 864/089, L INF 38



Interesting information from the last few years can still be found in the archive.


(will be updated during the semester)
Access information for the course material is given in class.

0 -Verification of Digital Systemsverif-1617-0.pdf
1 -Introductionverif-1617-1.pdf
2 -Graph Representations of Boolean Functionsverif-1617-2.pdf
3 -Formal Property Checking – Overviewverif-1617-3.pdf
4 -Model Checking with Temporal Logicverif-1617-4.pdf
5 -Symbolic Traversal of Finite State Machinesverif-1617-5.pdf
6 -SAT-based Property Checkingverif-1617-6.pdf


Some information about the exam:

  • The exam is an oral exam. 
  • Exam dates will be published on this web page.
  • You must have registered with the authorities responsible for your study course/program (Abteilung für Prüfungsangelegenheiten) in order to be able to take the exam.
  • Appointments for exams must be made online. For instructions download [PDF]
  • After online registration, you also need to have your student ID card verified with our secretary, Carmen Vicente-Fess (office hours: Mo-Fr 10:00h - 13:00h). 
    (In case you have already done this in an earlier semester for a different exam and your login still works you don't have to go through the registration procedure again. Your email address needs to be from the rhrk.uni-kl.de domain.)
  • Please note: the number of available time slots on each oral exam date is limited. If all time slots on a particular day are taken the online registration system will not allow you to select that day and you will have to make a different choice.

Exam dates

  • Thu, 2017-07-20
  • Tue, 2017-10-10

Important notes regarding exam dates

  • No other exam dates besides the listed ones are available in this semester. New dates will be fixed only in the next semester.
  • The number of time slots per exam date is limited. If you have constraints regarding your exam dates, maybe because you have another exam on one of shown dates, please make sure to register early while your favorite date is still available.  Time slots are assigned "first come - first serve".