Formal methods can guarantee 100% coverage which cannot be achieved by simulation based verification.  The tutorial presents an overview of formal methods and their use along the design process.  Underlying reasoning techniques are studied in detail.  Then, the tutorial focuses on three recent innovative developments:

(i) Dynamic verification of functional specifications

Assertions are written in formal languages: PSL and SVA are IEEE standards.  The tutorial will focus on the tools that compile properties into synthesizable modules.  This approach automates the debugging using both simulation and emulation, and still can be founded on formal techniques.

(ii) Combined verification of functional and timing specifications

Until now functional correctness and timing requirements are either verified in a separate way or by simulation.  The tutorial shows how formal methods verify both aspects within a single timed model.

(iii) Robustness analysis

Due to continuously shrinking feature sizes fault tolerance will be required for almost any electronic device in the near future. The final part of the tutorial focuses on techniques to assess the robustness of a design.  A fully automatic formal approach for robustness checking is introduced.

The purpose of the tutorial is an introduction to formal methods and to show their ability to solve recent and newly emerging design challenges.