“Very good course, exactly how I expected to be (topics, level of “pre” knowledge on PSL). And Mike, the instructor, was really brilliant.”
(Course attendee, public class, June 2012)
„What I liked most about the instructor was his deep knowledge of the course subject.
... I would recommend this course as it extends the methodology of verification“.
(Course attendee, onsite class, May 2011)
This course gives you an in-depth introduction to the IEEE1850 Property Specification Language (PSL), together with guidelines and methodologies to help you create, manage, and debug effective assertions for complex designs and protocols.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.
After completing this course, you will be able to:
o Explain the advantages of Assertion Based Verification (ABV) using the PSL.
o Write PSL code in the boolean, temporal, verification, and modelling layers of PSL.
o Write and debug complex overlapping assertions.
o Demonstrate, with examples, good and bad PSL coding styles and show workarounds for simulators with language support issues.
o Implement a methodology for describing complex transaction-based assertions and properties using PSL.
o Explain how PSL assertions can be applied to Formal Verification
o Incisive Enterprise Simulator
o Incisive Formal Verifier
o Incisive Enterprise Verifier
o INCISIV9.2, INCISIV10.2
Note that this course can be tailored to better meet your needs – contact the Cadence training staff for specifics.
o Assertion Based Verification (ABV)
· What is ABV?
· Contrasting HDL, OVL and PSL assertions
o PSL Basics
· Language layers
· VHDL and Verilog flavors
· Structure and placement
· Always and never
o Boolean Layer
· Boolean assertions
· Boolean flavors
· Clocked and unclocked properties
· Default clocks
· Conditional assertions
o Foundation Language (FL)
· Next cycle checks
· FSM properties
· Until and before
· Aborting properties
· Cascading FL operators
o Sequential Extended Regular Expressions (SERE’s)
· SERE introduction
· Sequence repetition
· Aborting SERE’s
· Named sequences
o SERE Composition
· Fusion and disjunction
· Processor example
· Sequence matching
· Whilenot and within
o Advanced PSL and the Verification Layer
· Built-in functions
· Parameterized constructs
· Replicated properties
· Verification units
· Multiple clocks
o Property Clocking
· Correct time to clock properties
· Multi-clocked properties
· Counter–intuitive clock behavior
o Coding Guidelines and Avoiding Common Problems
· Abstraction levels
· Over and under constrained assertions
· Never failing constructs
· Assertion refinement with arbiter case study
· What is coverage?
· Structural and functional coverage examples
· Coverage of the arbiter design
· Coverage applications
o Practical PSL Application
· Transaction-Based assertion modeling using AMBA
o Introduction to Static Formal Verification
· Static and dynamic verification
· Model checking
· Properties and constraints
o Conclusions and Next Steps
o Design and Verification Engineers using the VHDL, Verilog®, or SystemC® languages
o You must have experience of simulating and verifying VHDL, Verilog or SystemC designs