Verifikation Digitaler Schaltungen / Verification of Digital Circuits - Winter 21/22

Electronic components are present in more and more aspects of our life, especially in safety critical applications. Therefore, 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 do not serve to prove the absence of faults. Therefore, 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 industry.

 

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).