Lecture Verification of Digital Circuits Winter Semester 2021 / 2022
Organization
- Type of the course: Specialization for the BSC and MSc in Computer Science and ESE.
- ECTS:: 6
- Requires basic knowledge in Technical Computer Science
- Lecturer: apl. Prof. Dr. Ralf Wimmer
- Assistant: MSc Leonore Winterer
- Exercisegroup: every other week
Procedure
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
Content
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).
Literature
- Kropf: “Introduction to Formal Hardware Verification” , Springer, 1999, ISBN 3-540-65445-3
- Clarke, Grumberg, Peled, “Model Checking”, MIT Press 1999
- Kropf (Ed.): “Formal Hardware Verification”, Springer, 1997, ISBN 3-540-63475-4
- Various original papers
ILIAS E-Learning link
Details, news and lecture materials will be shared via ILIAS:
The password will be shared with participants closer to the start of the course.