Join Formal Verification Expert Jin Hou for the latest course addition to the Verification Academy video library:
Handling Inconclusive Assertions in Formal Verification
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.
View the new Handling Inconclusive Assertions in Formal Verification course.