Non Members - 0.00
In association with MIDAS Electronic Systems Skillnet
This course is an introduction to effective use of writing assertions for formal verification. Although the course will not focus on any particular formal verification tool, a tool will be used to demonstrate and practice the concepts introduced during the day.
Prerequisite: Knowledge of SystemVerilog assertions (SVAs) is a prerequisite for course participants. Mike Bartley will spend minimal time on that section at the start of the course.
1 Introduction to SVA
1.1 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
1.2 Writing properties for formal vs. simulation
1.3 Proving a basic property
• Using a formal verification tool to prove a basic property on a real design (e.g. FIFO)
2 Advanced SVA
2.1 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
2.2 Proving a complex property
• Using a formal verification tool to prove a complex property on a real design (e.g. FIFO)
• Interpreting the three possible outcomes: Proved, Failed, Unproven. For Unproven some techniques for trying to get proof through the tool – e.g. reduce input space, cut points, reduce data widths,
3 Debugging a failing property
• Using a formal verification tool to debug a failing property
4 Formal metrics
• Measuring coverage and completeness
• Measuring coverage with a particular Formal verification tool
Day 2
5 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 a Formal verification tool
6 Formal in the design flow
6.1 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
6.2 Formal for designers
• Designer bring-up
• Writing assertions “on-the-fly” using a Formal verification tool
• Where (which file) to write the assertions?
6.3 Formal reuse
• Reuse of assertions between dynamic and static verifications
• Running simulations with our formal assertions added using a Formal verification tool
• Reuse in assume/guarantee relationships
• Assertions as VIP
6.4 Formal in context
• Formal as part of a verification plan
• Combining formal results with other activities for a signoff decision
6.5 What type of design and size of design is suitable?
