Assertion-based Verification with PSL
Intermediate Level - 2 daysview dates and locations
The Doulos Assertion-Based Verification with PSL provides in-depth tuition in the use of Accellera’s Property Specification Language (PSL) in the context of an assertion-based verification methodology for digital electronic design.
Assertions benefit design and verification by removing ambiguity from specifications, finding bugs sooner and allowing fewer bugs through to production. The Doulos course enables successful adoption of assertions into projects by delivering an in-depth understanding of the language and a verification methodology to exploit it. The application of assertions to real project situations is demonstrated throughout, and is supported by extensive hands-on experience gained within the workshop sessions.
The Doulos Assertion-Based Verification course is presented from a vendor independent perspective but with workshops using a choice of leading HDL simulators, including ModelSimŪ, NC-SimŪ and SafeLogic MonitorŪ.
Who should attend?
- RTL design engineers and verification engineers who need to become skilled in property writing.
- Technical managers and team leaders who need a detailed understanding of writing properties in order to evaluate or manage the introduction of assertion-based based verification methods.
What will you learn?
- How properties and PSL fit into today’s verification landscape
- The roles that properties play in directed testing, constrained random testing and static formal verification
- How to exploit the benefits that properties can bring in the design and verification flow
- The syntax and semantics of the PSL language
- Guidelines on how to write effective properties and pitfalls to be avoided
- The practicalities of using PSL with an HDL simulator of your choice
- How to assess functional coverage
- A methodology for writing PSL assertions
- How to use PSL with AMBA based SoC
Pre-requisitesThe ability to read and understand simple examples of VHDL or VerilogŪ code is essential, and experience running HDL simulations is recommended. The ability to write original VHDL or Verilog code is not required.
Course materialsDoulos Course materials are renowned for being the most comprehensive and user friendly available. Their style, content and coverage is unique in the EDA training world, and has made them sought after resources in their own right. Course fees include:
- Fully indexed course notes creating a complete reference manual
- Workbook full of practical exercises to help you apply your knowledge
- Doulos Golden Reference Guide for language, syntax, semantics and tips
Structure and Content
The Verification LandscapeHow properties fit with verification • Simulation • Code coverage • Constrained random test generation • Functional coverage • Hardware verification languages • Assertion languages • Accellera standards • Formal verification • Property checking • Assertion-based verification
Properties DefinedProperties • Assertions • Simulation checkers • State space exploration • Assumptions and restrictions in static property checking • Verification coverage and corner cases • Assume-guarantee methodology • Assertion coverage • Automatic properties
Methodology and BenefitsWho writes properties? • Properties and the specification • Properties for the design and verification engineers • Observability and bug localisation • Property re-use • Debugging properties • Assertion density • Impact on documentation standards and review
The PSL LanguageThe boolean, temporal, verification and modelling layers • VHDL and Verilog flavours • Clocks • Verification directives • Verification units • Named properties • Safety and liveness properties • Simulation issues and the simple subset • The practicalities of using PSL with an HDL simulator
Temporal OperatorsLearning common temporal operators by example • always • never • next • eventually! • rose(), fell() and prev() • until • before • abort • Operator precedence • Practising the use of these operators to write common properties
SequencesSequences and Sequential Extended Regular Expressions • Sequence implication • Repetition operators • Parameterised sequences • Sequence composition operators • Practising the use of the typical form for a PSL property
Developing a MethodologyFunctional coverage • Assessing coverage • Refining assertions • Transaction based assertions
Real ApplicationsReusable assertions • Test modules • AMBA example
Further FeaturesThe Foundation Language and Optional Branching Extensions • LTL and CTL operators • Further sequence operators • Ranges • Non-consecutive and goto repetition • Endpoints • next_event • whilenot • within • forall • Macros • The Verilog modelling layer • (These features are not necessarily supported by all current verification tools)
This course is available now for team-based training at or near to your location. To find out more:
Complete an on-line form and a Doulos representative will get back to you »
Call Doulos to discuss your requirements »
Price on request
Back to top