Formal Verification is widely used in the verifiction process of most IC design flows, it consists on the use of formal tools to prove design specifications by using mathematical and statistics algorithms.
This course is focused to graduate or undergraduate electrical engineer students or any related area that wants to learn Formal Verification for any ASIC Formal Verification related job position.
In this course you will learn:
- Formal Verification Flow
- Liveness and Safety Assertions
- Dead-End
- Optimized assertions for Formal
- Formal Tools description and usage
- Formal Test Plan
- and more!
Course Instructor
Course Introduction
I. Formal Background
1.1 What is formal verification?
1.2 Formal verification background
1.3 Formal Tools
II. Assertions in Formal
2.1 Functional compatibility
2.2 Optimize SVA
III. Formal analysis
3.1 Formal Property Checking
3.2 State space
3.3 Cone of Influence
3.4 Challenges and Goals
IV. Formal Flow
4.1 Usual focus area
4.2 Jasper Flow
V. Non-Deterministic Constant
5.1 Definition
VI. Safety and Liveness
6.1 Relaxed checks
6.2 Forward progress
6.3 Safety
6.4 Liveness
Lab 1. Formal Verification of a gray counter
VII. Dead-End and Conflicts
7.1 Dead-End
7.2 Conflict
VIII. Complexity
8.1 Introduction
8.2 Flowchart
IX. Abstraction and Reduction
9.1 Constant propagation
9.2 Initial Value Abstraction
9.3 Reset Value Abstraction
9.4 Stopat
9.5 Counter abstraction
9.6 Reductions
X. Test Plan
10.1 Differences with functional
10.2 Template
XI. TCL Files (Cadence – Jasper Apps)
11.1 FPV
11.2 Superlint
11.3 COV
11.4 SEC
11.5 CSR
11.6 CONN