Formal Verification Training

Formal Verification Training

Learn How to Use Formal Verification Techniques to Improve Verification

The 2-day Formal Verification Bootcamp is for design and verification engineers looking to enhance their knowledge of formal verification and to learn how to write effective assertions to find and fix bugs. The course is a mix of presentations and hands-on development exercises.

Key Topics Covered

  • Introducing System Verilog Assertions (SVA)
  • Advanced SVA
  • Debugging a Failing Property
  • Formal Metrics
  • Automated Formal Verification
  • Full Formal Verification of a Block
  • Formal in the Design Flow
  • Formal for Designers
  • Using Formal Apps

Course Presenter

mike-bartley-webDr. Mike Bartley has worked in Formal Verification since completing his PhD in Mathematical Logic.  He has worked in formal specification of both software (VDM, Z) and hardware (CSP and SVA), as well as formal mathematical proofs of implementations.  Mike began working in property checking in 1994 and has worked continuously in both formal and dynamic simulation ever since.  As well as writing and proving assertions, Mike has put together verification strategies and teams that combine both formal and simulation.  Mike is a trained teacher and has written and delivered numerous training courses for Universities and commercial organisations. Mike uniquely combines theoretical knowledge, practical experience, management understanding and training expertise.

Formal Verification Training – Course Agenda

  •  Introduction to SVA
    • Writing Basic System Verilog Assertions
      • Introduction to the language
      • The main combinatorial language constructs (syntax and semantics
      • Constraints and properties
      • Examples of constraints
        – Reading and understanding
        – Writing from fresh
      • Examples of properties
        – Reading and understanding
        – Writing from fresh
    • Proving a basic property
      • Using a tool to prove a basic property on a real design (e.g. FIFO)
  • Advanced SVA
    • Writing Complex System Verilog Assertions
      • The main sequential language constructs (syntax and semantics
      • Examples of sequential constraints
        – Reading and understanding
        – Writing from fresh
      • Examples of sequential properties
        – Reading and understanding
        – Writing from fresh
    • Proving a complex property
      • Using a tool to prove a complex property on a real design (e.g. FIFO)
      • Interpreting the three possible outcomes
        – Proved, Failed, Unproven
  • Debugging a Failing Property
    • Using a tool to debug a failing property
  • Formal Metrics
    • Measuring coverage and completeness
    • Measuring coverage with a particular tool
  • Automated Formal Verification
    • Looking at the “out-of-the-box apps” available with a particular tool (e.g. clock domain crossing, SoC connection checking, reset checks)
    • Automated HDL checks (such as Synthesizability, Race conditions, Code reusability) †
  • Full Formal Verification of a Block
    • Developing constraints for a complex design (e.g. FIFO with APB interface)
      – Over constraint
      – Under constraint
    • Developing properties for the complex design
      – Determining a “full” set of properties
    • Run the constraints and properties using the tool
  • Formal in the Design Flow
    • The AHAA model
      • Understanding the various applications of formal verification
        – Bug avoidance
        – Bug hunting
        – Bug absence
        – Bug analysis
      • Understanding when and where to apply formal during a project
    • Formal for designers
      • Designer bring-up
      • Writing assertions “on-the-fly” using a tool
      • Where (which file) to write the assertions?
    • Formal reuse
      • Reuse of assertions between dynamic and static verifications
      • Running simulations with our formal assertions added
      • Reuse in assume/guarantee relationships
      • Assertions as VIP
    •  Formal in context
      • Formal as part of a verification plan
      • Combining formal results with other activities for a signoff decision
  • Using Formal Apps

Downloads

Although the course will not focus on any particular tool, a tool will be used to demonstrate and practise the concepts introduced during the day.

Find out more

Contact one of our training consultants today to find out more about our training courses.


Alternatively contact your local sales office