Providing an empirical measurement on the effectiveness and progress of the formal verification, the JasperGold® Design Coverage Verification App takes in the user's register-transfer level (RTL), assertion properties, and constraint properties and outputs a textual and GUI-based report showing how aspects of the design under test (DUT) were verified by the formal analysis. These reports show lines of code ("statement coverage"), conditional statements ("branch coverage"), and functional coverage points that were exercised.
For years, formal users have struggled for ways to report their progress to simulation-centric managers. While the discovery rate of critical bugs is obviously a helpful metric, the bug rate itself is a very coarse measurement that doesn’t express the true value of the results obtained from fully proven or bounded proofs. Formal tool users themselves could also benefit from formal-specific coverage metrics to protect against the potential over-constraint problem and eliminate false confidence in design correctness, as well as have an empirical measurement of the ROI of their formal verification effort.
Key Features
- Provides coverage metrics for formal users for their formal environments, whether a proof completes or is a partial, "bounded proof"
- Identifies areas that are impossible to reach by any stimuli; in this way, identifies a bug or a "safely illegal" area for which a constraint should be written
- Easily excludes/sets waivers for clearly illegal areas
- Protects against the potential over-constraint problem to eliminate false confidence in design correctness
- Features unique ProofCore technology, which analyzes the DUT and provides metrics for how completely the assertion set verifies the DUT