Jasper Formal Fundamentals Training

Length: 2.5 Days (20 hours)

Become Cadence Certified

Course Description

This course is intended for people with little or no experience in Formal Analysis (FA) and Jasper^TM. This course pragmatically illustrates how to code efficient SVA properties for formal analysis. Formal analysis is an entirely different paradigm from older and more widely adopted verification methods, such as simulation. As such, the fundamental objectives, capabilities, limitations, setup, initialization requirements, and analysis and interpretation of results must be well understood before we can effectively use Formal tools and specialized Jasper Apps. Formal is capable of much more than simulation alone and can deliver optimization techniques that often need to be applied to get conclusive results within realistic timescales. These techniques are complicated to discover or pick up "as one goes along" without training or expert assistance. Anyone can run a Formal tool, but experience is needed to get conclusive results in a realistic, wholly understood timeframe. 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 that are efficient for formal tools
• Set up, run, and analyze results from Formal Analysis, having identified designs upon which formal is likely to be successful
• Understand formal complexity issues and how to overcome them
• Create a complete formal environment from scratch given only a DUT functional specification
• Understand the basics of Formal coverage

Software Used in This Course

• Jasper 24.03
• VIPCAT 11.30.095

Software Release(s)

JASPER2403, VIPCAT 11.30.095

Modules in this Course

Introduction to Formal Analysis

• Contrast Formal with Dynamic
• Describe Formal Analysis terminology
• Describe how Formal tools work
• Explain factors affecting the quality of results
• Describe the limitations of Formal Analysis tools
• Recognise initialization issues
• Understand different kinds of formal use models and goal

Formal Friendly SVA Coding

• Identify SVA which is likely to be inefficient
• Create Auxiliary Code (HDL helper code) to assist when writing properties
• Recognize problems that cannot be solved by SVA alone
• Replace inefficient SVA code with a combination of simple properties and simple auxiliary code

Property Development Introduction

• Overcoming the "blank page syndrome"
• Who writes properties and when?
• Guidelines for writing properties
• Categories of properties
• Property development process
• Need for both checks and coverage

Overview of Formal Analysis Use Models

• Explain how Formal Verification differs from Simulation
• Use Formal Analysis for design exploration
• Use Formal Analysis to prove user-defined functional properties
• Use Formal Analysis to perform Deep Bug Hunting (DBH)
• Apply each of the different Jasper Apps to obtain verification closure

Jasper Apps Usage: Formal Analysis Flow (DLFA)

• Identify focus areas for Formal Analysis
• Formal Analysis flow phases, setup, initialization, stopats, etc.
• Using ProofGrid to distribute jobs to server farms
• Intro to ProofMaster in Jasper
• Debug hand-off
• Constraint management and debugging
• Recommendations
• Where to get help

Visualize

• What is Visualize?
• Visualize Flow
• Visualize GUI
• Visualize Features

Jasper Expert System 

• Knowledge-Based System
• Client-Based System
• Viewing and using recommendations

Interface Property Development

• Develop black-box protocol properties
• Enumerate a finite set of fundamental behaviors for features extracted from a verification plan
• Enumerate a finite set of protocol categories with which common protocols are associated
• Identify the subset of fundamental behaviors exhibited by a given protocol category
• Use these fundamental behaviors to drive the development of the protocol properties
• General vs. specific properties and why specific properties may be undesirable

Basic Complexity Handling

• Understand contributing factors to formal complexity
• Understand what adds state to the proof and how to reduce state
• Use the Jasper tool features to understand formal complexity
• How to simplify an environment
• Functional, value and bitwise splitting of properties to improve performance
• Structural changes
• Blackboxing
• Complexity tool aids - Complexity Manager and Formal Profiler

Complexity Reduction Methods

• Understand what Abstraction, Reduction, and Overconstraint are.
• Differentiate between abstraction, reduction and overconstraint
• Use abstraction mechanisms to reduce the time taken for a formal proof greatly
• Apply IVAs to choose arbitrary configurations
• Apply Reset Value Abstractions (RVAs)
• Apply counter abstractions
• Use overconstraint in a good way to gain confidence in the design
• Apply overconstraint

The Verification Completeness Problem

• Review verification methodologies
• Examine the case study highlighting the verification completeness problem
• State techniques for minimizing risk of verification holes
• States the merits of each verification technique

Coverage in Formal

• Identify the importance of Coverage
• Define the concepts of stimuli, checker, and formal coverage
• Analyze the Cone of influence (COI) and Proof core measurement
• Describe Mutation
• Demonstrate an overview of Jasper Coverage app 

Audience

• Design and Verification Engineers

Prerequisites

• You must experience writing properties with SVA.

  Or, you must have completed the following course:

  SystemVerilog Assertions.

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.