Length : 2 days
Course Description
This course is intended for people with little or no experience of Formal Analysis (FA) and JasperGold®. This course illustrates in a very pragmatic way on how to code SVA properties which are efficient for Formal Analysis. Formal Analysis is a completely different paradigm to 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 optimisation 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 propertieswhich 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
Software Release(s)
JG1912
Modules in this Course
- 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 simply 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
Audience
- Design and Verification Engineers
Prerequisites
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.
If you do not know any SVA then it is recommended to first do the SVA sections at the beginning of the online only SVA, Formal and JasperGold Fundamentals for Designers
Related Courses
Please see course learning maps at this link for a visual representation of courses and course relationships. Regional course catalogs may be viewed here.
Free Online Training Bytes (Videos)
Course ID: 86123
