Modern CPUs are extremely complex and error prone. In order to assure that a CPU indeed works correct, it no longer suffices to simulate the CPU since one can only cover a small part of the huge state space by simulation. The need for real verification becomes apparent.

However, paper and pencil proofs also tend to be error prone. Hence only the usage of formal methods can really guarantee that nothing has been overlooked.

In this seminar, we will give an overview of state of the art in hardware verification. On the one hand, there will be talks about automated tools that are capable of formally verifying properties by just clicking a button. We will introduce some of these tools and their limitations. On the other hand, there will be talks about the milestones in formal verification of hardware so far, i.e., the really big hardware components that have been formally verified.