Home > Community > Blogs > Functional Verification > the role of coverage in formal verification part 3
Login with a Cadence account.
Not a member yet?
Create a permanent login account to make interactions with Cadence more conveniennt.

Register | Membership benefits
Get email delivery of the Functional Verification blog (individual posts).


* Required Fields

Recipients email * (separate multiple addresses with commas)

Your name *

Your email *

Message *

Contact Us

* Required Fields
First Name *

Last Name *

Email *

Company / Institution *

Comments: *

The Role of Coverage in Formal Verification, Part 3

Comments(0)Filed under: Functional Verification, Formal Analysis, Coverage-Driven Verification, metric driven verification (MDV), coverage driven verification (CDV), verification strategy, Model-checking, PSL, SVA, Incisive, ABV, IEV, formal, methodology, IFV, metric-driven verification, assertions, simulation, coverage

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> 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

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
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.



Leave a Comment

E-mail (will not be published)
 I have read and agree to the Terms of use and Community Guidelines.
Community Guidelines
The Cadence Design Communities support Cadence users and technologists interacting to exchange ideas, news, technical information, and best practices to solve problems and get the most from Cadence technology. The community is open to everyone, and to provide the most value, we require participants to follow our Community Guidelines that facilitate a quality exchange of ideas and information. By accessing, contributing, using or downloading any materials from the site, you agree to be bound by the full Community Guidelines.