The Role of Coverage in Formal Verification, Part 3

14 Feb 2011 • 5 minute read

.special { font-family: 'Courier New' !important; }

In the last post of this series, we will address the last but not least of three key questions to be answered with coverage in formal verification:

How good are my formal constraints? (Addressed in Part 1)
How good is my verification proof? (Addressed in Part 2 and "2A")
And today's question, "How can I feel confident my verification is complete?"

By the time you come across this third question, you are already done with "Constraint development and design exploration" and well into the "Checks development and bug hunting" phase as per the following process diagram:

Your design has become stable, lots of bugs are already fixed, and many checks are already passing. As per your verification plan, you would have decided to develop set of checks and functional coverage points. It is time now to complete the setup of all desired functional coverage points. The PSL/SVA cover statement is an excellent way to describe functional coverage, as it's a declarative form that keeps the statement up at the more abstract, easier to read specification level. Consider this code example:

//psl cover_fifo_full: cover {full};

In above cover statement we want to capture an interesting scenario -- the condition of a FIFO being full. From this statement, the formal tool will automatically generate a test showing the sequence of writes to fill the FIFO. Even better, with formal you don't have to worry about how to generate this test on per cycle basis as you do in simulation. Instead, you just need to describe the scenario at a given level of abstraction and the tool will take care of "the how", i.e. it will generate a sequence of instructions to achieve the specified goal.

While creating a deep and interesting scenario could be difficult, Incisive Formal and Enterprise Verifier tools ("IFV" and "IEV") provide methods to easily combine simple scenarios into a "deep" scenario. Consider this code example:

    // psl cover_fifo_full: cover {full};    // psl cover_guide_1: cover {(~rd_en && wr_en)[*100] };
    // psl cover_guide_2: cover {(~rd_en && wr_en)[*200] };
    // psl cover_guide_3: cover {(~rd_en && wr_en)[*300] };

In above statements, in addition to "cover_fifo_full" cover, other sub-scenarios (or sub-goals) "cover_guide_1" to "cover_guide_3" have been described as well. You can effectively add these covers together and run the tool to reach them. Additionally, to create more cover statements quickly, IEV also provides multiple features to compose covers interactively. Consider this snapshot from an interactive IFV command line session:

FormalVerifier> prove Modeling check mode: Vacuity check finished Verification mode: cover_guide_1 : Pass (200) cover_guide_2 : Pass (400) cover_guide_3 : Pass (600) cover_fifo_full : Explored (532) Assertion Summary: Total : 4 Pass : 3 Explored : 1 Not_Run : 0

In this example, 3 of the 4 goals are achieved right off the bat. However, in this particular DUT reaching the "cover_fifo_full" objective is more difficult than expected, and the tool initially reports an inconclusive result (as shown in the line "Explored : 1" above). No problem: IEV allows you to use sub-goals (or "sub-scenarios" if you prefer) to achieve the final goal (scenario) for test generation. This technique is called "Guide Pointing".

The command line snippet below shows an example of Guide Pointing in action. Specifically, the sub-goals are added as guide using command "assert -add cover_g* -cover -guide". Now, in the "prove" run the cover "cover_guide_3" is used as a stepping stone - a/k/a a guide point -- to reach the final cover "cover_fifo_full".

FormalVerifier> assert -add cover_g* -cover -guide
formalverifier: *W,ALMAAS: "cover_guide_1" is already marked as an assertion. formalverifier: *W,ALMAAS: "cover_guide_2" is already marked as an assertion. formalverifier: *W,ALMAAS: "cover_guide_3" is already marked as an assertion. 0 assertions added. 3 guides added FormalVerifier> prove formalverifier: *W,MULCGD: Multiple conclusive guides found. Guidance will start from last conclusive guide "test.cover_guide_3". Verification mode: cover_fifo_full : Pass (1026) Assertion Summary: Total : 4 Pass : 4 Not_Run : 0

With this "Guide Pointing" technique, all the cover point waveforms are generated now. In general, IEV provides formal, simulation, and mixed engine-based methods for cover-based test generation.

Note that once you have developed scenarios, you can enable your checks and run the tests of scenarios to see if your checks are also validated in simulation. All simulation coverage data (code coverage, functional coverage) is generated too; and you can re-use/reference these same cover points in IES-XL simulation-oriented coverage and planning tools as well.

Let's recap: we've showed how to combine sub-scenarios so you can reach a deep scenario. The cover statements are comprised of Property Specification Language (PSL) or SystemVerilog assertions (SVA), which implicitly capture the test scenarios. Multiple, dual technology-based methods are available to test these scenarios. Using this technology you can sign off your verification with exactly same functional and code coverage goals as in simulation. In fact, formal assists you in scenario development and you could achieve much higher functional coverage goals much more quickly.

As we presented in the previous post, a conclusive proof in formal has potentially higher coverage number (i.e. reachable coverage). On some critical checks, a user might decide to go all out with conclusive proofs. IEV provides number of automated, semi-automated and manual expert level features to achieve this goal. These include engine distribution, haloing, constraint minimization and cut point-based methods for automated, semi-automated, or manual abstractions.

We will tackle these expert level topics in future posts. However, suffice to say now that what differentiates IEV from other tools is that it provides methods for composing test scenarios with both formal engines and the full power of simulation as well. This dual-technology approach takes care of the nagging question in formal, "What if my check explores?" As a bonus, you get an excellent tool for automated test waveform generation. The bottom-line: you will achieve all your verification goals via exhaustive proofs of your critical checks -- one of the few things in life you can say with mathematical certainty!

Happy verifying!

Vinaya Singh
Architect
Cadence R&D

On Twitter: http://twitter.com/teamverify, @teamverify

Reference Links: Part 1, Part 2, Part 2A of the series; plus more on the Incisive Formal Verifier (IFV) and Incisive Enterprise Verifier (IEV) tools mentioned above.