"Great course... it certainly raised the enthusiasm of the design team (for PSL)."

What is PSL?
The Property Specification Language (PSL) is an industry and IEEE (IEEE1850) standard language for specifying design properties (assertions), functional coverage and constraints. PSL can be embedded in HDL code and used in both simulation and Formal Verification, enabling a sophisticated and complete Assertion Based Verification (ABV) methodology.

This Advanced PSL and Formal Verification course builds upon Esperan´s 2 day Verification with PSL course to demonstrate advanced PSL features and introduce a methodology for using PSL in both Formal Verification and simulation. This course may be taken stand-alone for delegates with existing PSL knowledge, or as an add-on to the Verification with PSL course.

• To demonstrate the full capabilities of PSL Verification Units (vunits) and the modeling layer in general.
• To introduce the concepts, terminology, benefits and limitations of Formal Verification.
• To describe a methodology using PSL in both simulation and Formal verification.
• To provide practical experience of using PSL in Formal Verification and hybrid verification.

1 day. This class can also be combined with the 2 day Verification with PSL class to create a 3 day PSL for Formal Verification training.

Delegates should have attended the Esperan 2 day Verification with PSL course or have advanced working knowledge of HDL's, PSL and simulation techniques.

The course covers:

PSL Verification Units and the modeling layer

Capabilities of Verification Units; Modeling layer and its application; Flexible verification methodologies using Verification Units; Using vunits to bind PSL or SystemVerilog Assertion modules to legacy designs of any language.

Introduction to Formal Verification

Basics of Formal Verification; Formal Analysis terminology; Introduction to how Formal tools work; Preparing a design for Formal Verification.

Formal Verification Methodology

Recommended approaches when using formal verification; Using a hybrid combination of Formal verification and Simulation; Understanding the limitations of Formal Verification. Features to define complex design protocols

Interacting FSM Case Study

How bugs escape; Generating random stimulus; Checking randomisation of stimulus; Effects of random seed choice; Locating hard to find corner case bugs; Effects of parameterisation;

• Verification Units
  • Types of Verification Units
  • Binding
  • Inheritance
  • Name space (scoping) rules
  • Modeling Layer
  • Using PSL to improve SystemVerilog's bind command
• Introduction to Formal Verification
  • Contrasting Formal and Dynamic Verification
  • Formal Analysis terminology
  • How Formal tools work
  • State factors affecting quality of results
  • Limitations of Formal Analysis tools
  • Initialisation issues
• Formal Verification methodology
  • Merits of Formal and Dynamic verification
  • Properties in different contexts
  • Getting the best return on investment in Formal
  • Design Level Formal Analysis (DFLA)
  • Guidelines for writing properties
  • Dealing with the "size" problems
  • Understanding Liveness constraints
  • Parameterisation
• FSM Case Study
  • Examining the verification of interacting FSM’s
  • Design Description
  • Verification Challenges
  • Demonstrating different verification techniques
  • Random Stimulus
  • Concerns about randomness
  • Effect of random seed choice
  • Effect of parameterisation
  • Parallel simulations
  • Advantages of Formal Verification
  • Hybrid verification
• Conclusions and Next Steps
• Index

Course Labs

The labs sessions include:

• Preparing a design for Formal Verification
• Debugging formal tool counter examples
• Using a Design Level Formal Analysis (DFLA) Methodology
• Writing HDL and PSL to meet a specification
• Formally verifying an HDL design containing PSL properties without simulation
• Initialisation of Formal Verification with a simulator database