Course Structure
The workshop is based around a 2 day agenda, or can be run in 3 days in conjunction with the 1 day
Advanced PSL and Formal Verification class.
We can also offer standard or customized versions of this workshop onsite or at the location of your choice.
Course Summary
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.
Workshop Agenda
- 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
Workshop Labs
The workshop 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
Overview & booking
