Formal Assertion-Based Verification
In this track, you will learn how to get started with direct property checking including: test planning for formal, SVA coding tricks that get the most out of the formal analysis engines.
-
Sessions
-
Introduction to Formal Assertion-Based Verification
In this session we will learn about various formal verification techniques; what they are, how to utilize them, and benefits received from advanced formal technologies. -
Basic Formal Closure (Black Boxing and Cutpoint)
At some point formal engines will begin to struggle under the weight of the state space. This session will show two simple techniques to safely limit the states the engines need to process, enabling more in-depth results. -
Formal Model Checking
In this session we'll share some basic tips for getting started with direct property checking, how to setup the analysis for rapidly reaching a solution, and how to answer the question, “Do I have enough assertions?" -
Questa PropCheck
This session will demo the Questa PropCheck tool and will review features including the details window, properties window, along with source, waveform and schematic debug features.
-
-
Overview
The automated formal apps reviewed in the “Automatic Formal Solutions” course have introduced a new generation of D&V engineers to the power of formal verification without the pain. This success has inspired renewed interest in creating formal testbenches for DUT-specific verification challenges that are well suited to formal. Specifically, formal tools statically analyze a design’s behavior with respect to a given set of properties, exhaustively exploring all possible input sequences in a breadth-first search manner to uncover design errors that would otherwise be missed.
In this course the instructors will show how to get started with direct property checking including: test planning for formal, SVA coding tricks that get the most out of the formal analysis engines AND ensure reuse with simulation and emulation, how to setup the analysis for rapidly reaching a solution, and how to measure formal coverage and estimate whether you have enough assertions. Finally, a session on creating formal-based verification IP will show how to create libraries of reusable, optimized properties for formal analysis.
You are encouraged to first view Getting Started with Formal-Based Technology by Harry Foster that introduces basic concepts and terminology that should be useful by any engineer wishing to mature their formal-based technology skills.
-
Forum Discussion - Assertions