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 course, 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.
