This course is intended for people with little or no experience of Formal Analysis (FA) and JasperGold®. 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 initialisation 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 in order 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 52% lectures and 48% hands-on labs.
After completing this course, you will be able to:
- Understand how FA tools work.
- Load a design and carry out fully automatic formal analysis without the need to write properties by using Structural Property Synthesis.
- Recognise problems that cannot be solved with SVA alone.
- Use Visualize® to learn how a design works, debug counter examples and experiment with "what if” scenarios without the need to write properties or modify the design.
- Write properties which are efficient for formal.
- Understand the need for assumptions and how to describe them efficiently.
- Use JasperGold® to formally prove user defined properties.
- Use abstract techniques to reduce the time taken to reach conclusive proofs.
- Use auxiliary “helper” code in order to make properties simpler to write and easier to prove for the tool.
- Given only a functional specification, adopt a systematic approach to property development which gets good results consistently.
- Simplify properties and environments to reach conclusive results more quickly.
- Understand what is meant by “Property Set Completeness”.
- Identify what the goals of FA are and how to identify which types of designs are likely to yield a good return on time invested.
- Understand the factors which can make a formal analysis complex for JasperGold® and techniques which can be employed to reduce that complexity.
- Use Jasper Proof Accelerators.
Software Used in This Course
- Incisive® Enterprise Simulator (IES)
JG1606, IES 15.2
Modules in this Course
- Formal Analysis Introduction
- Contrast Formal with Dynamic
- Describe Formal Analysis terminology
- Describe how formal tools work
- Explain factors affecting quality of results
- Describe the limitations of Formal Analysis tools
- Recognise initialisation issues;
- Formal Analysis Goals
- Define Formal Analysis (FA) goals
- Describe the interaction of dynamic and FA in verification
- Understand different kinds of formal use models
- 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
- Phase I: Setup and Initialisation
- Phase II: X-Propagation (XPROP) & Advanced Formal Linting (AFL)
- Phase III: Formal Property Verification (FPV) & Debugging
- Focus areas
- Using ProofGrid to distribute jobs to server farms
- Using tasks in JasperGold®
- Assertion completeness
- Design Level Formal Analysis (DLFA) flow phases
- 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 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
- Black boxing
- What is Visualize?
- Visualize Flow
- Visualize GUI
- Visualize Features
- Interactive lab visualizing properties (with no design) in order to help with their development
- Property Development Introduction
- Overcoming “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 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
- 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