SVA, Formal and JasperGold® Fundamentals for Designers

Length : 2 days

Digital Badge Available

Course Description

This course is intended for people with little or no experience of SVA, Formal Analysis (FA) and JasperGold^®. SystemVerilog Assertions (SVA) is a very concise and powerful language for defining behaviors (properties) which a design should have. Its concise nature makes it deceptively difficult to intuitively understand all consequences of the property being written and, hence, very easy for users to make damaging mistakes. This course introduces SVA in a very pragmatic way, including how to code SVA properties which are efficient for Formal Analysis. Formal Analysis is a completely different paradigm from the older and more widely adopted methods of verification like simulation. As such, the fundamental objectives, capabilities, limitations, setup and initialization requirements, in addition to analysis and interpretation of results, need to be well understood before we can make effective use of FA tools and specialized JasperGold Apps. Formal is capable of much more than simulation alone can deliver but optimization techniques often need to be applied to get conclusive results within realistic timescales. These techniques are extremely difficult to discover or pick up "as one goes along" without training or expert assistance. Anyone can run an FA tool but experience is needed to get conclusive results in a realistic timeframe which are completely understood. This course is intended as a shortcut to gaining that experience. The course has 60% lectures and 40% hands-on labs.

Learning Objectives

After completing this course, you will be able to:

• Define reusable, functionally correct SVA properties which are efficient for Formal tools. These shall make use of abstract auxiliary code to simplify descriptions, make code maintenance easier, reduce debug time and reduce tool proof runtime.
• Set up, run and analyze results from Formal Analysis.
• Identify designs upon which formal is likely to be successful, while understanding formal complexity issues and how to identify and overcome them.
• Identify situations where Initial Value Abstractions (IVAs) would be appropriate and how to define them.
• Set up and run the JasperGold Apps named Superlint and X-Propagation
• Use a systematic process of property development to approach a completely new verification problem.

Software Used in This Course

• JASPERGOLD 1906

Software Release(s)

JASPER1906

Modules in this Course

• Assertion-Based Verification Introduction
• SVA Boolean Assertions
• SVA Sequences
• SVA Coverage
• Property Reuse
• Liveness Properties
• Formal-Friendly SVA and Auxiliary Code
• Introduction to Formal
• JasperGold Expert System
• JasperGold Tool Flow and Usage
• Cause of Complexity and Complexity Reduction Methods
• Visualize Features Introduction
• Superlint App
• Initial Value Abstractions (IVAs)
• X-Propagation App
• Property Development Introduction
• Interface Property Development

Audience

• This course is primarily intended for designers who want to use formal as an aid to design, perform automated formal checks and preliminary verification.
• The course is also suitable for verification engineers with no previous experience of SVA, Formal or JasperGold.

Prerequisites

Other than one month's experience of using Verilog, no other experience of SVA, Formal or JapserGold is required.

Related Courses

Replace this paragraph with a bulleted list of any related courses linked to their datasheets.
Following is an example course and link.

• SystemVerilog for Design and Verification

Please see course learning maps at this link for a visual representation of courses and course relationships. Regional course catalogs may be viewed here.