Handling Inconclusive Assertions in Formal Verification
In this track, you will be introduced to techniques to help formal tools solve inconclusive assertions. You will also learn tool options to help convergence, introduce techniques for reducing assertion and design complexity.
-
Sessions
-
Editor Insight
This editor insight session provides an introduction and motivation for our new track, which is focused on handling inconclusive assertions in formal property checking. -
Easy Solutions
In this session you will be introduced to easy solutions for handling inconclusive assertions by exploring tool options, and how to know where formal is stuck at. -
Assertion Complexity Reduction
In this session you will be introduced to the techniques that reduce the complexity of assumptions and checkers for formal verification, including under-constraining, over-constraining, assertion decomposition, adding “helper” assertion, assume-guarantee, and Questa® QFL assertion libraries. -
Design Complexity Reduction
In this session, you will be introduced to techniques to reduce the complexity of designs for formal verification, including understanding what formal is analyzing, easy ways to reduce design complexity, counter remodeling and memory remodeling examples. -
Advanced Topics
In this session, you will be introduced to the techniques of separating functions, data-independence, non-determinism, and bug hunting that are very useful for formal verification.
-
-
Overivew
Assertion-based formal verification can fully verify the functions of a design if all of the associated assertions can converge. Formal verification doesn’t need testbenches and can start much earlier in the process. It can consider all possible input stimulus sequences to find error traces of assertions or prove the assertions if no stimulus sequence can violate the assertions. The proof capability of formal doesn’t exist in simulation. More and more companies are adopting formal verification.
However, due to the complexity of designs we have today, almost inevitably the user will encounter non-convergence problems which occur when the tools are unable to find either proofs or error traces for some assertions. Capacity limitations are a well-known characteristic of today’s formal verification tools. Fortunately, designers and verification engineers can learn methods for analyzing these non-convergence problems and improving their verification results.
In this track, the instructor Jin Hou will introduce the techniques to help formal tools solve inconclusive assertions. She will show how to use tool options to help convergence, introduce techniques for reducing assertion and design complexity. She will also introduce advanced ND and DI techniques for reducing formal complexity, how to verify different functions separately, and bug hunting methods. Using these techniques, the user can get more results from formal tools.
-
Forum Discussion - Assertions
-
Is there a dummy simulation that I could use to compare runtime of different machines
Nov 06, 2024 SystemVerilog -
How to write a assertion to check a 2D array that all its elements with the value zero
Oct 16, 2024 SystemVerilog -
RESET assertion ,assertion where reset is asserted asynchronously and de asserts synchronously
Oct 15, 2024 SystemVerilog -
Write a SystemVerilog Checker for DUT behavior(Sequence pattern generator DUT)
Oct 09, 2024 SystemVerilog