VC Formal Coverage Analyzer

Integrated Formal Analysis for Coverage Closure

Projects are increasingly relying on coverage metrics to help determine when chips are ready for tape-out. However, coverage goals are not always attainable. VC Formal Coverage Analyzer provides an integrated mechanism for using robust formal techniques to determine which structural coverage metrics are attainable, and to automatically exclude metrics which cannot be reached.

Formal Analysis for Coverage Closure

Getting a project to tape-out on schedule requires achieving many signoff criteria. For constrained-random simulation, the most crucial of these requirements is closing coverage. Coverage metrics provide a measurement of the correctness and completeness of a simulation test environment. Verification experts know that any areas of the design with poor code coverage results have simply not been tested by the testbench whatsoever. These coverage holes are a red flag to verification teams. However, the next step–identifying which uncovered targets are actually achievable— has been extremely painful. Certain aspects of the code are present strictly for extreme error scenarios, and are almost impossible to achieve, but of course it is still critical to verify them for correct operation. A lack of coverage for items in such regions could be a true hole requiring improvements in the simulation test environment. Other aspects of the code are dead code, composed of things that simply cannot be executed, such as unused functionality within re-used code. A lack of coverage here is obviously expected, as these areas in the code are simply unreachable. The problem is manually identifying which is which. Modern verification teams have struggled with this problem for years, but are now having much larger challenges due to the extreme size of today’s chips and the significant amount of code reuse, which tends to increase the unreachable code that could be excluded. This manual exclusion process can take weeks to months, depending on the complexity involved.

VC Formal Coverage Analyzer performs this painful process automatically by integrating with the simulation engine, coverage reporting and debug solutions. This tight integration makes this process seamless and easy to use. Reachable versus unreachable coverage items are automatically identified and provided to the verification team. By automating this process, the verification team can focus on the truly reachable critical aspects of chip operation that need further testing, and comfortably exclude aspects that are proven unreachable–all through the power of formal verification (See Figure 1). 

Features and Benefits

  • Best-in-Class Formal Engine
    • VC Formal Coverage Analyzer is optimized to perform analysis at the fastest speeds on large databases.
  • Comprehensive Structural Coverage Analysis
    • VC Formal Coverage Analyzer automatically extracts and applies formal unreachability analysis to line, condition, toggle and FSM state transition coverage goals (See Figure 3).
  • Automatic Exclusion and Coverage Metric Adjustment
    • VC Formal Coverage Analyzer generates an exclusion file containing all unreachable coverage goals for review that can imported into VCS® and Verdi® so final coverage metric reporting is adjusted automatically, and can be used with subsequent simulation runs.