JasperGold Formal Fundamentals

• 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
• Formal Analysis Introduction
  • 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
       
• JasperGold Expert System (JGES) Introduction
  • Knowledge-Based System
  • Client-Based System
  • Viewing and using recommendations
• JasperGold Tool Usage
  • Design Level Formal Analysis (DLFA) flow phases
  • Using ProofGrid to distribute jobs to server farms
  • Using tasks in JasperGold
  • Constraint management and debugging
  • Recommendations
  • Assertion completeness
  • Where to get help
• Causes of complexity
  • Understand contributing factors to formal complexity
  • Understand what adds state to the proof and how to reduce state
  • Use the JasperGold tool features to understand formal complexity
• ·Generic Complexity Reduction Methods
  • 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
• Visualize
  • What is Visualize?
  • Visualize Flow
  • Visualize GUI
  • Visualize Features
• 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
• Interface Property Development
  • Develop blackbox 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
• RTL Signoff Apps Introduction
  • Superlint - Automated Formal checks
  • Xprop - Xpropagation
• Initial Value Abstractions (IVAs)
  • Introduction to Initial Value, Reset Vaue and Counter Abstractions
  • Impact on Formal Verification
  • IVA Application

You must have one month of experience writing properties with SVA.

Or, you must have completed the following course:

NOTE: This course is a subset of the online only course #86235 titled SVA, Formal and JasperGold Fundamentals for Designers. This course does not cover basic SVA syntax and principles.