"In-depth, practical and realistic"

"Brilliant ... the team is still talking about those examples you showed us"

What is PSL (IEEE1850)?

The Property Specification Language (PSL) is an industry and 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.

PSL is integrated into VHDL in the latest release of the language.

Esperan’s PSL course gives you an in-depth introduction to the language, together with guidelines and methodologies to help you create, manage and debug effective assertions for complex design properties. The course is packed full of examples and case studies to demonstrate real life applications of the language. We also examine different approaches to coding assertions, including workarounds for the restricted language support of some tools.

This course can be run for both Verilog and VHDL engineers.

• To explain the advantages of Assertion Based Verification (ABV) using the Property Specification Language (PSL).
• To describe in detail the boolean, temporal, verification and modelling layers of PSL and show how the layers are used to build assertions.
• To demonstrate, with examples, good and bad PSL coding styles and show workarounds for simulators with language support issues.
• To describe, with case studies, a methodology for describing complex transaction-based assertions and properties using PSL.

2 days, or 3 days in conjunction with the 1 day Advanced PSL and Formal Verification class

Delegates must have a experience of either VHDL or Verilog code, and be familiar with running and debugging HDL simulations. The course assumes no prior knowledge of PSL.

The course covers:

Property Specification Language (PSL) Fundamentals

Describing the layered structure of the PSL, showing how simple HDL boolean expressions can be built up into powerful, multi-cycle assertions using the temporal, verification and modelling layers.

Sequential Extended Regular Expressions (SERE’s)

Exploring sequences in PSL; using SERE replication and composition features to define complex design protocols and applying SERE operators to typical design tasks.

Coding Guidelines and Methodologies

Demonstrating good and bad coding styles; using parameters and nesting to create compact, reusable assertions and defining a methodology for writing sophisticated transaction-based assertions.

• Assertion Based Verification (ABV)
  • What is ABV?
  • Contrasting HDL, OVL and PSL assertions
• PSL Basics
  • Language layers
  • VHDL and Verilog flavors
  • Structure & placement
  • Always and never
• Boolean Layer
  • Boolean assertions
  • Boolean flavors
  • Clocked and unclocked properties
  • Default clocks
  • Conditional assertions
• Foundation Language (FL)
  • Next cycle checks
  • FSM properties
  • Eventually
  • Until and before
  • Aborting properties
  • Cascading FL operators
• Sequential Extended Regular Expressions (SERE’s)
  • SERE introduction
  • Conditional assertions
  • Sequence repetition
  • Aborting SERE’s
  • Named sequences
• SERE Composition
  • Fusion & disjunction
  • Processor example
  • Sequence matching
  • Whilenot and within
• Advanced PSL and the Verification Layer
  • Built-in functions
  • Parameterized constructs
  • Replicated properties
  • Verification units
  • Dealing with multiple clocks
• Property Clocking
  • Correct time to clock properties
  • Multi-clocked properties
  • Counter-intuitive clock behavior
• Coding Guidelines and Avoiding Common Problems
  • Abstraction levels
  • Over and under constrained assertions
  • Overlapping
  • Never failing constructs
  • Assertion refinement with arbiter case study
• Coverage
  • What is coverage?
  • Structural and functional coverage examples
  • Coverage of the arbiter design
  • Coverage applications
• Practical PSL Application
  • FIFO
  • Transaction-Based assertion modelling using AMBA
• Introduction to Static Formal Verification
  • Static and dynamic verification
  • Model checking
  • Properties and constraints
• Conclusions and Next Steps
• Appendices
• Index

Course Labs

The course labs aim to give you practial experience of assertion writing; practice in managing and debugging PSL assertions with supporting simulators and an understanding of the methodology of applying assertions to realistic designs.
The lab sessions include:-

• Familiarization with managing and debugging PSL assertions in a simulator
• Verification of components of an AMBA bus protocol implementation using PSL