>

 

 

Using PSL for Formal and Dynamic Verification

Course duration: 1 day

Course Curriculum.

This one-day methodology primer gives you the technical and practical information you need to apply the Property Specification Language (PSL) for Assertion-Based Verification (ABV).  This complete introduction helps you leverage PSL as an executable language for the definition of system requirements, interface specifications, RTL design, and verification of subsystems coded in Verilog and VHDL.  Whether you're committed to using PSL or simply evaluating how it fits with your verification methodology, this course will show you how PSL can be effectively used to accomplish your verification tasks.

Focusing on PSL in the design definition and verification process, and as a language including methods to define properties, your PSL-expert instructor leads you and your team through both the syntax of the language and how to apply it to real world verification tasks.  Dynamic and formal verification of designs using PSL are demonstrated with several real-world models and optional lab exercises that help cement the concepts.  This one-day course covers the following topics:

  1.

Overview of PSL Provides a detailed comparison of traditional verification methods with Assertion-Based Verification (ABV); an overview of the language properties and concepts; an example in simulation and formal verification results
2.

PSL in the Design Process explains how ABV fits within an advanced verification methodology, including system level and interface assertions. An overview of planning strategies are presented, with a detailed overview of how to write properties and assertions for a typical design.
  3.

The PSL language introduces the language, property and verification directives, operators, Sequential Extended Regular Expressions (SERE) and repetition. Provides several examples, a dictionary from English to PSL, PSL guidelines, vunit, and verification directives.
  4.

Using PSL in simulation and formal verification presents a fully implemented example of how to use PSL in an ARM AMBA AHB environment. Demonstrates processes and issues in formal verification using a traffic light controller. Demonstration of model is also provided.
  5.

Clocking issues shows you how to address single and multiple-clocks in a block, static analysis and tool supports, addressing clocking issues using an asynchronous FIFO as an example.
  6.

Upcoming PSL 1.1 features provides an overview of powerful new features released in rev 1.1. including built-in functions and actions on endpoints.
  7.

Review, reflections and questions gives you the opportunity to address specific issues and solutions for your needs.

Who should attend?

This course is ideal for verification teams that are committed to using PSL on their next project, or are evaluating how PSL might fit in their verification flows.  If you want to learn how to use PSL to efficiently verify your designs, this course is for you.

The learning environment.

This is an interactive course with optional individual labs that cement the concepts taught in the lecture portion of each session. Students may optionally use simulators that support PSL (Mentor Graphics Modelsim or Cadence Incisive NCSim) or formal verification tools (@HDL and Safelogic products).  This class can be taught using either Verilog or VHDL as the base design language.

You will receive a full printed coursebook and a copy of optional lab exercises as part of the full course delivery.  You may optionally choose to include a copy of Ben Cohen's new text Using PSL/Sugar for Formal and Dynamic Verification (ISBN 0-9705394-6-0). Contact us for more information.

How to attend this course.

You can attend a regularly scheduled public course, or schedule your own private session at your facility.  To find out more, contact us toll free now on the Verifica Hotline at 1-888-HVL-GURU (or +1.503.295.6440), or contact us by Clicking Here.

Detailed course outline.

This course is structured as multiple sessions taught over a 6 to 8 hour period. Optional interactive lab exercises are distributed throughout the course. For more information about course content and structure, or if you're interested in customization, please call us toll free on the Verifica Hotline at 1-888-HVL-GURU (or +1.503.295.6440), or contact us by Clicking Here.

 

Section 1:

Overview of PSL
 

PSL goals and history
 

Users, acceptance & roadblocks
 

PSL introduction
 

 

  • property / specification / verification

  • traffic light controller example in simulation & formal verification
 

Assertion-Based Verification with PSL

     
 

Section 2:

PSL in the Design Process
 

System requirements
 

Algorithms
 

Interfaces
 

Design Process with ABV and PSL
   

  • Design & Verification

  • Quality of properties and coverage

  • Assertion Density
     
 

Section 3:

The PSL Language
 

Property, verification directive, operators, SERE and repetition, named sequence
 

Examples and demonstrations
 

Dictionary English -> PSL
 

Guidelines
 

Advance features
 

 

  • vunit

  • verification directives
 

Lab Session
   

  • Handshake and packets

  • Parking structure

  • Home alarm system

     
 

Section 4:

Using PSL in Simulation and Formal Verification
 

AMBA AHB Example design process
 

PSL code examples
 

Simulation
 

Experience
 

Traffic light controller example in formal verification

 

 

  • Process & issues

  • Demonstration
     
 

Section 5:

Clocking Issues
 

Defining clocks in PSL
 

 

  • Typical multi-clock problems and solutions

  • Tool support

  • Asynchronous FIFO example
     
 

Section 6:

Upcoming PSL 1.1 Features
 

Syntax changes
 

Labels
 

Built-in functions
 

Actions on endpoints
     
 

Section 7:

Review, Reflections, Questions
 

PSL in the design process
 

How can PSL meet customers needs?
 

PSL in relation to SVA
     

Schedule your Verifica course today.

There is no substitute for a private course taught on-site at your facility, particularly when you have 6 or more engineers to train. Simply put, for large groups it’s always less expensive for us to come to you than the other way around. And if you want a custom course, we can arrange it. Do you need to squeeze a four day course into three? No problem. We know how to do it without compromise. And if you need a course on short notice, we can be there sooner than you think. For more information, contact us at:

Verifica – the right kind of verification training, tuned to your needs.  Contact us now.