Tutorial 2 • Using PSL with HDL for Formal and Dynamic Verification
sponsored by: $ Special Tutorial Promotion $

This tutorial provides technical and practical information on the application of Assertion-Based Verification (ABV) using Property Specification Language (PSL) for the definition, design, and verification of subsystems coded in HDL. The tutorial focuses on PSL in the design and verification process and PSL as a language including methods to define properties. The language is explained not only syntactically, but also with many examples. Dynamic verification of designs using PSL is demonstrated with several models, including a model of an ARM AMBATM AHB master connected to a pipelined memory slave interface. Formal verification with PSL is then addressed and demonstrated using a traffic light controller example. The tutorial concludes with guidelines for writing PSL, and a summary of why PSL is paradigm shift in the design and verification of digital systems.

…ABV is to Verification … as RTL is to Synthesis …