Formal Coverage
Formal coverage is a hot topic these days. Simulation has a number of metrics for helping determine when verification is done. These include code coverage, assertions coverage, transaction coverage, and functional coverage to name a few.
-
Sessions
-
Formal Coverage Introduction & Overview
In this session, you will be introduced to the Formal Coverage track. -
Formal Coverage vs. Simulation Coverage
This session will explore the various aspects of simulation coverage metrics. -
Formal Coverage for Property Debug
This session will review the definition of a vacuous or uncoverable property and the main reasons why these property bugs exist. -
Formal Coverage for Inconclusive Debug
In this session we’ll review what inconclusive properties are and why they happen. We’ll then look at some easy tool based methods to help resolve inconclusives. -
Formal for Over-Constraint and Reachability Analysis
In this session we’ll review what makes a design observable and controllable by doing reachability analysis. -
Property Debug
This session will demo property debug using Questa PropCheck. -
Formal Coverage
This session will demo formal coverage using Questa PropCheck. -
Inconclusive Debug
This session will demo how to debug an inconclusive property using Questa PropCheck.
-
-
Overview
Formal coverage is a hot topic these days. Simulation has a number of metrics for helping determine when verification is done. These include code coverage, assertions coverage, transaction coverage, and functional coverage to name a few.
Like simulation, formal has metrics which can be used to determine when verification on a design block is complete. In one session we’ll compare simulation metrics to formal metrics and how the two can be combined as part of an overall verification flow leveraging the UCDB database and Verification Management analysis and tracking.
Next, you will see how proof coverage can be used beyond the traditional coverage closure methods to improve your verification results.
One session will focus on how proof coverage can be used to help debug vacuous assertions and uncoverable cover statements. Another session will focus on how proof coverage can be used to help debug inconclusive properties and some simple steps you can take based on this information.
The final session will cover 2 important topics regarding formal coverage having to do with reachability, which can help with bounded proofs, along with over constraint analysis which is an important part of an assurance driven formal flow.
-
Forum Discussion - Formal Coverage