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 and its sessions including; simulation coverage, property debug, resolving inconclusives and over-constraint & reachability analysis. -
Formal Coverage vs. Simulation Coverage
This session will explore the various aspects of formal coverage. We’ll start by reviewing the major components of simulation coverage metrics including code coverage, assertions coverage and functional coverage. -
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. Then we’ll look at how Questa PropCheck can use proof coverage to help debug these types of properties. -
Formal Coverage for Inconclusive Debug
In this session, we’ll review what inconclusive properties are and why they happen. Then we'll look at some easy tool-based methods to help resolve inconclusives. Finally, we’ll explore some of the more common methods of modifying the properties and design to resolve the inconclusive property. -
Formal for Over Constraint and Reachability Analysis
In this session, we’ll review what makes a design observable and controllable. Next, we’ll look at doing reachability analysis for understanding if a design is a good candidate for applying formal techniques. This can also be used in more advanced techniques for bounded proof analysis. We’ll also explore how reachability can be used in over constraint analysis. -
Property Debug
Sometimes you will have properties which are vacuous or uncoverable. Sometimes it is obvious why this is. In many other cases though it is difficult to determine the reason these property bugs exist. In this session, you will learn how Questa PropCheck can help and the process. -
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