JasperGold® Formal Fundamentals

• 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 initialisation issues
  • Understand different kinds of formal use models and goals   
• Jaspergold Expert System (JGES) Introduction
  • Knowledge-Based System
  • Client-Based System
  • Viewing and using recommendations
• Formal Friendly SVA Coding
  • Identify SVA which is likely to be inefficient
  • Create Auxiliary Code (HDL helper code) to assist when writing properties
  • Recognise problems that cannot be solved by SVA alone
  • Replace inefficient SVA code with a combination of simple properties and simple auxiliary code
• 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 simply an environment
  • Functional, value and bitwise splitting of properties to improve performance
  • Structural Changes
  • Blackboxing
• 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
  • Oneshot properties in SVA
• RTL Signoff Apps Introduction
  • Superlint
  • Xprop
• Initial Value Abstractions (IVAs)
  • Introduction to Initial Value Abstractions
  • Impact on Formal Verification
  • IVA Application
• Functional Property Development
  • State the difference between blackbox and whitebox properties
  • Describe DUV domains
  • Bounded proofs
  • Use abstract techniques to verify datapaths
  • Use Jasper Proof Accelerators
  • Liveness, safety, strong and weak properties and implications of their use

• Design and Verification Engineers

You must have one month’s experience writing properties with SVA.

Or you must have completed the following course:

• SystemVerilog Assertions
• Verification with PSL

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