Verifikation Digitaler Schaltungen / Verification of Digital Circuits - Winter semester 2020/21

overview

description

Many modern products are based on microelectronic components. Frequently the correct functioning of these products is essential, e. g., in medicine technology or automotive systems. For this reason, strict requirements on the quality of the applied microelectronic systems are imposed. These requirements can be divided into three groups: (1) The system has to be designed correctly according to its specification. (2) The physically manufactured system has to work correctly after being manufactured. (3) Additionally the system should work reliably (without any breakdown) for a specified period of time. While requirement (2) can be handled by test methods and requirement (3) by methods for increasing the reliability, for requirement (1) verification and validation methods play a central role. The focus of the lecture lies on verification and validation methods for digital systems. Here both the formal proof of system properties and the conformance of the design to a given specification are of interest. First a number of different basic technologies for formal verification like binary decision diagrams, SAT solvers, and and-inverter graphs are presented. Building on that, we describe approaches (which are based on symbolic methods) for checking the equivalence of combinational and sequential circuits as well as for model checking different classes of properties.

comment

Specialization for the BSC and MSc in Computer Science and ESE.