|
Training Course on Formal Verification
Tuesday 5 December, 2006 -- [09h00 - 11h00]
 Huy Nam Nguyen
Meta Symbiose
SUMMARY
The purpose of this training course is to introduce the
multiple aspects of Formal Verification in a design flow and to
illustrate those purposes on real life designs.
The course will address the following main topics:
- Abstraction and Equivalence Checking to support verification of
compatibility/equivalence at different design steps from RTL down to
switch level.
- Assertion-based Verification including Model Checking and the
Formal
Verification Language PSL. To compliment Model Checking, ABV-dynamic
checking will be also addressed to provide a complete scheme of
verification at RT level.
- Specific applications of Formal Verification at higher level of
abstractions as proof of concept in some domains of application (eg.
verification of protocol coherence).
The main objective is to provide an overview of Formal Verification
techniques and a pragmatic approach to this discipline with an analysis
of the effectiveness and maturity of those techniques.
OUTLINE
1. Introduction to Formal Verification
- Overview of FV techniques
- Definitions and Classifications
- Formal Verification in the design flow
2. Abstraction
- Abstraction methods
- Abstraction of switch level to RTL
3. Equivalence Checking
- Equivalence Checking Techniques: Principles and limitations
- Application of Equivalence Checking: Usage, constraints, debugging
4. Model Checking
- Temporal Logic (LTL, CTL)
- The PSL standard
- Assertion-based Verification
5. Formal Verification to support Proof-of-concept
- Ad-hoc application of FV at higher level of abstraction (eg.
Coherence protocol verification)
AUTHOR BIO
NGUYEN Huy-Nam is president of METASymbiose S.A.S. where he is
responsible for the development and marketing of Formal Verification
products. He is also responsible for many verification activities
including TLM, Formal verification, Emulation/Prototyping at Bull S.A.S.
NGUYEN Huy-Nam holds an engineering degree from the Ecole National
Supérieure des Mines de Paris and a Docteur-Ingénieur
(PhD) in applied mathematics from University Paris-IX.
AUDIENCE
The course targets system/hardware designers/verifiers/managers willing
to import or improve new verification methods into their design flow.
The training course will be pragmatic, focusing not only on technical
aspects but also on methodologies of usage illustrated by many
real-life examples.
|
|
