Questa OneSpin StaticFormal Questa Increase Coverage – A Formal etiquette solution for accelerating code coverage closure

Questa OneSpin StaticFormal


Code coverage is a much-needed metric in most modern-day RTL design flows and coverage closure is a key step in any RTL design and verification process. It helps teams to ensure that all RTL code written is indeed exercised and verified prior to tape-out. One of the challenges in coverage closure is the time taken to get to 100% with potential waivers/exclusions. Traditionally, teams have deployed many RTL designers to review each uncovered item, to ensure it is a genuine hole and can be safely excluded. This process is expensive, time-consuming, and is prone to human errors. This is where Questa Increase Coverage is useful. It flags code coverage items that are difficult to reach by formal techniques and haven’t been hit in simulation, thus providing a valuable measure of verification complexity. This guides engineers to make their designs more easily verifiable.


Thank you for all the questions during the webinar! You can find the answers to the live questions below. If more support is needed for any of the issues you are facing, please open a support case at  

Q: What about coverage items that are still Inconclusive after the run has finished?
A: I usually recommend that users first focus on the exclusions the tool generates before diving into the inconclusive results. Anytime you are dealing with formal techniques there is the potential for longer run times and inconclusive results and there can be a diminishing ROI in chasing down all the inconclusives in a run. 
There are some simple tool options to help users reduce the number of inconclusive results.
  1. Increase the timeout 
    With the "covercheck verify -timeout" option, you can start out with a short timeout for the initial pipe cleaning of your setup. Once everything is clean, you can increase your timeout to multiple hours. If you are still seeing inconclusive results, you can do a long run over the weekend.
    It is recommended to always use the "-timeout" option for your Increase Coverage runs.
  1.  Expand multi-process usage with "covercheck verify -jobs" option
    The tool can run target multiple coverage items in parallel. This is controlled using the "covercheck verify -jobs" option. You can increase the number of jobs the tool is using, and it is also possible to farm those jobs out to your grid. See the User Guide for information on running Multi-Process Analysis for additional details.

Q: Are there any suggestions that can help with performance or run time?
  1. Use the UCDB from your simulation when running Increase Coverage: 
    You should load the UCDB from your simulation into your Increase Coverage run. This can reduce the number of targets the tool is focusing on because it will not re-target an item that has already been covered in simulation. This reduces the number of targets and shrinks the size of the problem the tool is working on. 
  1. Isolate coverage items, so the tool only runs on one set of coverage items at a time: 
    By default, all coverage checks are enabled. You can use the "coverage disable" and "coverage enable" directives to tell the tool to only target the coverage items you are interested in. You can also use this strategy divide the coverage problem into smaller segments making it easier for the tool to converge on the results. 
  1. Reduce the scope of the problem by running at the block level: 
    You can run on a sub-block using the "covercheck compile -d" option to specify the sub-block module name. You can then either add -G or -g options to change the default parameters to match the values that were propagated down through the instantiation, or you can use the "-tb_top" to specify the testbench top module. This latter option will use the parameter values passed down from the testbench and through your DUT. 

Q: How to generate adaptive exclusions?
A: To generate adaptive exclusions, you should add an -adaptive switch with the “covercheck compile” command followed by the covercheck verify command. Once the covercheck analysis is complete, you can generate the exclusion file with coverage signatures either from the terminal using the “covercheck generate exclude” command or goto ‘file->export->exclusions’ option in GUI. 

Q: Can we use API calls to parse the covercheck database file?
A: Yes, you can create a TCL script with APIs to extract information from the covercheck.db file.
Some of the calls that are extensively used are: 
  • GetResult API will returns verify results in 3 categories whether it could be “Covered” / “Uncoverable” / “Inconclusive”  
  • The other APIs GetRadius and GetProofRadius were Used to check if a shorter cover trace may be possible. 
  • GetEngines returns engines used for formal analysis. 
  • GetAssumptions returns any assumptions used. 
Please refer to the QOSF command reference doc for the full list of supported APIs. 

Q: How to use the same parameter configuration from simulation in a covercheck run?
A: So if you want to use the same parameter configuration as what you have in simulation, then, when generating a UCDB in simulation, just pass -coveragesaveparams argument to vopt command of questasim. This will store resolved parameter values for all instances in the UCDB. And when covercheck analysis is run by loading this UCDB then all the stored parameter configurations will be applied automatically.

Q: Is Questa Increase coverage available with a Questa prime simulation license?
Q: Will it be available with the current questa licenses or separate licences has to be taken?

A: You should have a separate license feature “Questa OneSpin Sol Increase Cover Ap SW – SfCca” to run the Questa Increase Coverage tool. The QuestaSim licenses will not help to run this tool.

Q: How is Questa Increase Coverage different than Questa CoverCheck tool?
Q: Would you please show the differences and features comparing this tool and the classic  CoverCheck tool from Mentor/Siemens?
A: Questa Increase Coverage expedites the pace of achieving comprehensive code coverage closure through automated exhaustive coverage analysis. This solution minimizes the exertion required for coverage closure, resulting in enhanced predictability in project timelines and heightened design quality. It facilitates greater cost-effectiveness and stands as the singular scalable solution accessible across multiple simulation flows. Questa Increase Coverage represents the next evolution in coverage closure solutions, incorporating the full array of features from Questa CoverCheck and OneSpin DV-CCA, and is being elevated with continued development expanding its scope of application to serve a broader application spectrum.

Q: Do you need to use the same version of QuestaSim and Questa Increase Coverage?
A: No. The latest version of Questa Increase coverage handles the older version of UCDBs automatically and runs the coverage analysis. 

Q: Is it usable in a multiuser environment? How to merge different exclusion files?
A: Generally you apply the exclusions generated from the Questa Increase Coverage run to the UCDB used during the run. Then the merging of UCDB files happens externally. You can opt for Questa's web-based solution VIQ for this.

Q: I can see the waveforms are from Questa Visualizer. Is Questa Visualizer needed for Questa Increase Coverage?
A: The new license file of Questa Increase coverage has SfUi and visframework features by default in it which are required to invoke Visualizer. So there is no need to have a separate visualizer license.
The same is true for the legacy licenses. However, you needed a Questa Autocheck base license for the legacy Questa Covercheck, that is where the visframework and zngui keys come from which are needed to invoke the visualizer. The specific app license just had that license, for example, covercheck will have only the zncovercheck feature in its legacy license file.


KB Article ID# KB000129473_EN_US



Associated Components

Questa Increase Coverage [CoverCheck]