Eight tips for performing effective unreachability analysis
Sanjana Bhattacharya is a corporate applications engineer in Synopsys’ Verification Group supporting multiple VC Formal applications. Formal technologies are increasingly popular in verification because they are good at finding bugs early in the development process and can be used for an exhaustive analysis of certain aspects of a design.
One popular application of formal verification techniques is to automatically detect ‘dead’ code, a process known as unreachability analysis. This is especially useful when a straightforward simulation-based approach has reached 75 – 80% of the coverage target for the design and yet the verification team is struggling to cover the remaining 20 – 25%. There is no point in trying to hit a coverage goal that is unreachable because the uncovered code itself is actually unreachable. However, manually showing this is the case can take a lot of time and effort and is prone to errors. Finding an automated way to detect dead code makes it much easier to progress towards the coverage target.
Synopsys has a formal verification tool called VC Formal, which includes an application called VC Formal Coverage Analyzer (VC FCA) that does unreachability analysis. The tool is integrated with Synopsys’ VCS and Verdi debug platform, so it can process the VCS simulation coverage database, extract the uncovered items, and then do an unreachability analysis on them to generate an exclusion file. The simulation coverage database and the formally generated exclusion file can be loaded into a coverage viewer tool, such as URG or Verdi Coverage, to see how the coverage score has improved.
The application of formal methods usually takes a lot of computing power, and so (VC FCA) is best applied at the block level. However, used with simulation, the technique can be applied effectively to SoC level designs as well. Here are eight practical tips about using unreachability analysis on larger designs to improve coverage.
1 – If a simulation coverage database for the full block is available…
Use it as much as possible. Use VC FCA to extract the uncovered items from the coverage database and then focus on them. This reduces the number of coverage targets that FCA must work on.
2 – If you need to analyze all the supported coverage metrics…
VC FCA supports line, cond, fsm_state, fsm_trans and toggle coverage metrics. Compile the design with all metrics. At runtime, enable each metric separately for faster convergence.
If performance is still a concern, apply these guidelines:
- Perform toggle coverage analysis separately.
- Analyze each metric separately.
3 – Take care with toggle coverage
Avoid using the -cm_tgl mda switch of VCS. In many circumstances, a simulation script will use all possible switches to exhaustively test all design scenarios. Users should check whether toggle coverage monitoring is necessary for multi-dimensional arrays (MDAs). If not, this switch should be removed before running VC FCA.
Avoid enabling toggle coverage for input ports, unless absolutely necessary.
4 – If a simulation coverage database is not available…
avoid running VC FCA on the full block level and instead target sub-blocks of interest, based on design knowledge. Try to do unreachability analysis in the early stages of the design development, before other forms of verification have started.
5 – Make intelligent use of the “cm_hier” switch of VCS
The coverage analysis can be broken down to modules of interest using the “cm_hier” switch of VCS. This can be done with or without the simulation coverage database.
If the simulation coverage database is available, load it into a coverage viewer such as Verdi coverage or URG and identify the modules for which simulation has achieved a poor coverage score. Target those modules first for unreachability analysis using the “-cm_hier” switch of VCS.
The exclusion files generated for each module can be fed to the coverage viewer, along with the simulation coverage database, to see how the coverage score has improved.
6 – If there are memory models in the design…
make modules that are known to be unfriendly to formal analysis, such as RAMs and memories, into black boxes.
7 – If you can run the tool on a server farm…
do so.
8 – Expect longer run times
It is time consuming to run an unreachability analysis on big designs, so be prepared to let VC FCA run for at least 24 hours for best results.
Author
Sanjana Bhattacharya is a corporate applications engineer in Synopsys’ Verification Group supporting multiple VC Formal applications. She has seven years of experience in assertion-based verification, product quality assurance and deployment of formal methodologies.
