A Coverage-Driven Formal Methodology for Verification Sign-off
Related
Persistent Notes
They use COI coverage
In-text annotations
“I. INTRODUCTION” Page 1
“II. COVERAGE-DRIVEN FORMAL VERIFICATION FLOW” Page 1
“A. Formal Coverage” Page 1
“Legal design state space becomes unreachable due to (usually unintentional) over-constraints in the FV environment. As shown in Figure 1, the yellow area illustrates the legal state space not exercised/checked by FV due to over-constraints. It is not uncommon to have unintentional over-constraints in a FV environment since they are difficult to uncover. Without proper coverage analysis, bugs in over-constrained legal state space may be missed by FV." Page 2
“During the verification execution phase, we use assertion COI (Cone of Influence) coverage [8] to ensure the entire logic of the DUT, except dead code, is within the union of COIs from all assertions." Page 2
“Second, to eliminate unintentional over-constraint, we use stimuli reachability coverage to ensure no branch/statement/expression in the RTL is unreachable due to incorrect constraints. We also use functional coverage, as we had encountered some complex interdependent over-constraints that could not be uncovered by stimuli coverage only." Page 2
“B. Formal Verification Plan” Page 3
“C. Coverage-Driven Formal Verification Flow” Page 4
“Verification signoff for the design can be declared when the following criteria are met: 1. 100% functional coverage reached. No assertion failures evaluated in any functional cover trace. 2. 100% COI and Reachability coverage reached with waivers (for dead code, etc.) 3. All assertions are either fully proven or bounded proven with sufficient bounds. 4. No conflict in FV constraints." Page 5
“III. FORMAL AND SIMULATION CO-VERIFICATION” Page 6
“A. Formal and Simulation Co-Verification Plan” Page 6
“B. Merging FV and Simulation Coverage” Page 6
“IV. RESULTS” Page 6
“A. Design Specification Improvement” Page 6
“B. Quality of Bugs Discovered” Page 7
“C. Execution Time/Project Schedule Improvement” Page 8
“D. Formal and Simulation Co-Verification” Page 9
“V. CONCLUSIONS AND FUTURE WORK” Page 10
%% Import Date: 2025-12-31T15:10:00.930-05:00 %%