Chair of Computer Architecture

University of Freiburg

Lecture Verification of Digital Circuits Winter Semester 2021 / 2022



We wil try to offer the lecture in a hybrid format. Students are welcome to attend the lecture in person, if the 3G regulations (vaccinated, cured, tested) can be followed. We will also offer a livestream of lectures as well as recordings for anyone who can’t attend (or doesn’t feel comfortable).

Time and Place

Monday, 10am-12pm: Lecture

Wednesday, 10am-12pm: Lecture and Exercise alternating biweekly

Room: Building 51, R 03 026


Electronic components are present in more and more aspects of our life, especially in safety critical applications. Therefor, it is vital to ensure their correct functionality. Simulation and test are common methods to find obvious faults, but corner cases and rare faults are not that easy to find; these methods also don’t serve to prove the absence of faults. Therefor, formal methods are used in semi conductor industries to systematically search for faults and, optimally, prove their absence.

In this lecture, we will study data structures and methods that form the basis for formal verification of digital circuits, like binary decision diagrams, SAT solvers, And-Inverter-Graphs. Based on these methods, we will look at symbolic methods for equivalence checks and automatic model checking for digital circuits, as they are used daily in indistry.

The application of these methods is no longer limited to circuit verification. SAT solvers, for instance, play an important role in AI (Automated Reasoning, Knowledge Representation, Planning).


Details, news and lecture materials will be shared via ILIAS:


The password will be shared with participants closer to the start of the course.