Abbrevation
FVMHD
City
Grenoble
Country
France
Start Date
End Date
Abstract

The objective of the training is to give an overview of the use of formal verification methods for hardware design&#046; After attending this training you will know:<br>What is equivalence checking and how it is working&#046;<br>What is the meaning of assertions and how you use them to express design properties (the training presents the main assertions constructors using PSL but the concepts are independent of the language)&#046;<br>How the verification by assertions is working&#046;<br>What is the correct by construction approach and why it can be an alternative&#046;<br>What are the advantages and disadvantages when using formal verification methods&#046; How to introduce formal verification in the design flow&#046; REGISTRATION FORM REGISTRATION FORM Please complete this form and fax it or mail it to: ECSI Office Parc Equation 2, Avenue de Vignate 38610 GIERES, France Ph: +33 476 63 49 34 Fax: +33 476 42 87 87 Email: office@ecsi&#046;org http://www&#046;ecsi&#046;org <b>Keywords:</b> The role of formal methods in hardware design<br>Validation of specifications, verification of a design step f Different techniques and tools: equivalence checking, model checking, theorem proving&#046;<br>Equivalence checking<br>Representation of Booleans expressions f Proving equivalence with tools&#046;<br>Assertion&#8211;based design<br>Principles of the technique (model checking) f Concepts for temporal property specification: LTL, CTL f The PSL standard f Practical use of PSL for verification by simulation, emulation, model checking&#046;<br>Theorem proving<br>Different logics, same principle f Validation of high level functional specifications f Combining symbolic simulation and theorem proving to verify RTL&#046;<br>Rule&#8211;based design<br>Expressing your design by rules f Guarantee the initial specification by refinement and proof: a protocol example f How to master the complexity by decomposition&#046;<br>Formal verification and legacy<br>Re&#8211;use IPs &#046;&#046;&#046; and still have a formally verified system&#046;<br>Introduction of formal verification methods in the design flow&#046;<br>