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

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 …

This tutorial will introduce SystemC as a powerful language for advanced system design using Platform Transaction Level Modelling. It starts with an introduction to the background, history, and development of SystemC. Modelling styles will be introduced, with an emphasis on representing levels of abstraction.
The Open SystemC Initiative is promoting the introduction of standard interfaces at different levels of abstraction – such standards enable the development of tools to automate the refinement of transaction level models toward implementation. SystemC standardization activities, including SystemC transaction level modeling standards, are described.

The SystemC Verification Library (SCV) extends SystemC to support a constrained random test methodology for verification in a C++ modelling environment. An introduction to constrained random testing is included, as well as an outline of the use of SCV.

The tutorial concludes by describing how a complete verification flow is built up with SystemC for Platform Transaction Level Modelling, SCV for constrained random testing, and standardisation of abstraction levels to simplify refinement from high to low level.