Jasper App For Early Design Verification Training

Length: 1 Day (8 hours)

Digital Badges

Course Description

This course is intended for RTL Designers and Verification Engineers with basic knowledge of Formal and Jasper^™. This course demonstrates how to effectively utilize various Jasper Apps (Superlint, Clock Domain Crossing (CDC), XPROP, Sequential Equivalence Checking (SEC)) for early design verification. Formal analysis differs significantly from traditional verification methods like simulation, so it's crucial to thoroughly grasp the objectives, capabilities, limitations, setup, initialization requirements, and analysis of results before utilizing Formal tools and specialized Jasper Apps.This course focuses on early design verification issues such as linting, clock and reset domain crossing, and X-propagation and how these can be addressed using Formal and Jasper Apps. It comprises 60% lectures and 40% hands-on labs.

Learning Objectives

After completing this course, you will be able to:

• Learn about Jasper Apps, which does not require much SVA and Formal knowledge 
• Set up and run Jasper Apps for early design verification 
• Use various Jasper Apps
  • CDC, SEC, XPROP and Superlint
• Analyze the result of Lint, X propagation, and Clock domain crossing issue and sequential equivalence check

Software Used in This Course

• Jasper 24.03

Software Release(s)

JASPER2403

Modules in this Course

Introduction to Jasper App for Early Design Verification

• Define formal verification
• List the various formal apps 
• Explain RTL signoff using Jasper
• Describe the formal apps used in the early design verification stage

Jasper Superlint App

• Set up and run the Jasper Superlint App 
• Run Autoformal and Lint
• Analyze the results from the automated formal checks and debug Counter Examples(CEXs)
• Analyze the result from Lint 
• Define, export, and import waivers for specific checks which are expected to fail

Jasper Clock Domain Crossing (CDC) App

• Explain Clock Domain Crossing in a formal setting 
• Outline the flow of the Jasper CDC App
• Describe Structural analysis, functional analysis, and metastability injection 

Jasper XPROP App

• Define an X value and identify its potential dangers
• Explain X in the formal context
• Utilize the XPROP App to detect, debug, and fix X-propagation issues for a variety of X-sources and destinations
• Use the –precond option to prevent real X-propagation issues from being masked by the waiving of false negatives
• Describe the features of the XPROP App

Jasper Sequential Equivalence Checking (SEC) App

• Define Sequential Equivalence Checking (SEC) 
• Identify popular SEC Use Models
• Outline the SEC flow
• Describe the components of SEC GUI
• Debug failure in the SEC App  

Audience

• RTL Designers 
• Design and Verification Engineers

Prerequisites

You must have experience with or knowledge of the following:

• Basic understanding of the design verification purpose and methods
• Sufficient background with VHDL or SystemVerilog to follow presented code fragments
• Basic of formal 

Or you must have completed the following courses:

• Jasper Formal Fundamentals

Related Courses

• Jasper Formal Expert
• SystemVerilog Assertions

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