Pitfalls of mixing formal and simulation: How to stay out of trouble

Driven by the need to objectively measure the progress of their verification efforts and the contributions of different verification techniques, IC designers have adopted coverage as a metric. However, what exactly is being measured is different depending on the underlying verification technology in use.

In Part 1, we outlined the textbook definitions of simulation and formal coverage, and then we briefly introduced the risks inherent in arbitrarily merging these metrics together. In Part 2, we shared a series of RTL DUT code examples to illustrate the trouble that can occur when comparing the results from simulation and formal side-by-side.

In this article, we will demonstrate how even properly merged 100% code and functional coverage results can still tempt you to prematurely conclude that your verification effort is over and it’s safe to declare victory. But the good news is that mutation analysis can exhaustively prove that both your DUT and your verification plan itself are bug free. Plus, we will summarize recommendations for properly using simulation and formal coverage together.

Full code coverage achieved—but there is still a bug

The example finite state machine (FSM) and supporting logic in Figure 1 shows a trap that many fall into—assuming that 100% code coverage means that they are done with verification. This assumption is based on a misconception of the reason we measure code coverage—the sole value of code coverage is in pointing out areas of the DUT which haven’t been verified, regardless of which engine is being used.

Figure 1 Here is a view of 100% code coverage of FSM from simulation (left) and formal (right). But could there still be a bug in the DUT? Source: Siemens EDA

In this example, the two outputs are mutex and a property has been written that passes in simulation and is proven in formal. In this verification scenario, the above results from simulation and formal show full coverage on the mutex check for the “out1” and “out2” signals.

Despite these promising results, there are two important points to consider. One is the importance of a complete test plan. Imagine that there is a requirement of “the FSM to be in only state 2 for no more than 3 cycles”. In this case, all the code is traversed, but the functional behavior is incorrect. If this requirement was not part of the test plan, then the above coverage reports would fool the user into believing that the verification was complete while the bug slipped through. However, if the requirement made it into the test plan—which was in-turn captured in the following assertion—then it would be properly tested:

a_st2_3_max: assert property (@(posedge clk) disable iff (!rstn)

\$rose(st2) |-> ##[1:3] !st2 );

In this scenario, simulation could have completely missed this functional bug if there was no test to cover this case; and in fact, for the vectors run to give the above coverage, that was the case, as the assertion passed. However, exhaustive formal analysis would have spotted the functional error and reported it as a counter-example to the user.

The larger point of this example is the cautionary note that coverage is mainly for seeing what isn’t covered, versus the focus on achieving 100% coverage at all costs; even if you have 100% code coverage, you may still have bugs that other analyses and coverage metrics will reveal.

Now let’s go a little further and see how model-based mutation coverage can help in revealing such gaps in a verification environment. Mutation coverage is generated by the verification tool systematically injecting mutations (faults) into a formal model of the DUT, and then checking whether any assertion would detect a bug at the corresponding fault point. The mutations are done electronically, in the mutation tool’s memory, while the original source code is untouched. In effect, mutation coverage measures the ability of your testbench to find bugs; if your verification environment can’t find a bug that you have deliberately created in the form of a property, it is unlikely to find bugs you have not imagined.

As shown in Figure 2, running the coverage analysis with mutations indicates precisely where there is a gap covering the requirement, and thus the need to add it to the test plan in order to make it complete.

Figure 2 The model-based mutation coverage reveals the missing requirement and related test from the test plan. Source: Siemens EDA

Recap: Using both formal and simulation code coverage together

Verification teams use coverage data from three types of engines: formal, simulation, and emulation. All contribute to test plan signoff as well as coverage closure in all aspects. Focusing on code coverage, the following table outlines some of the differences between formal and simulation code coverage:

Table 1 The data highlights the differences between formal and simulation code coverage. Source: Siemens EDA

The primary concern here is that mixing code coverage from multiple verification engines can mask holes in the testbench of the other engine. There are other subtle differences which make merging code coverage from different engines difficult. The following recommendations may help.

Recommendations

The formal and simulation coverage flows are flexible, which allows you to make use of them in whatever capacity best fits your needs. Below are a few things to consider when using code coverage from any of the verification engines:

• Ideally, close code coverage for each verification engine separately.

⁰     Focus on improving testbench completeness and robustness in each domain.

⁰     Code coverage data should be kept separate in the main coverage database for this purpose.

⁰     Additionally, in the formal domain, run both proof core (formal coverage based on the logic needed to prove a property) and mutation coverage to check testbench completeness.

• Test planning is important for determining which verification engine will verify which parts of the design.

⁰     Formal may totally verify certain modules. When mixing formal and simulation code coverage, try to keep it to instance boundaries, something that can be enabled/disabled in one domain versus the other.

⁰     When mixing code coverage, plan it as part of the test plan, late in the game.

• Know where your code coverage comes from: formal versus simulation.

⁰     Keep code coverage data from each domain separate in the main coverage database.

⁰     Reporting must also make it clear where the coverage data came from.

⁰     Only merge coverage data for final reports near the end of the project.

• Avoid writing properties or adding vectors to only trivially hit some specific part of the design to get to the 100% coverage mark.

⁰     This doesn’t typically improve verification, only trivially improves coverage.

⁰     This is why the test plan is important. Coverage holes point to an incomplete test plan and ultimately an incomplete/weak testbench.

⁰     When adding properties or vectors to close code coverage holes, verification of features and requirements of the design are your guide and will give you the highest quality of verification.

Naturally, code coverage from various verification engines will be used to make decisions regarding meeting project milestones. The verification team and project leaders are ultimately responsible for their results. When required to mix coverage for a given block from multiple verification engines, it is recommended to have a peer review on how the code coverage was generated to make sure valid tests tied to a test plan are used.

Proper merger of results

With proper understanding of the nature of the coverage metrics being recorded, output from all sources can be combined to give a holistic picture of the progress and quality of the verification effort. In this series, we focused on the most common element of this need—properly merging the results from formal analysis with the coverage from a constrained-random simulation testbench such that individual contributors and team leaders will understand exactly what the data is telling them.

Editor’s Note: This is the last article of the three-part series on the pitfalls of mixing formal and simulation coverage. Part 1 outlined the risks of arbitrarily merging simulation and formal coverage. Part 2 shared RTL DUT code examples to illustrate the trouble of comparing the results from simulation and formal side-by-side.

Mark Eslinger is a product engineer in the IC Verification Systems division of Siemens EDA, where he specializes in assertion-based methods and formal verification.

Joe Hupcey III is product marketing manager for Siemens EDA’s Design & Verification Technologies formal product line of automated applications and advanced property checking.

Nicolae Tusinschi is a product manager for formal verification solutions at Siemens EDA.

Related Content