The Role of Coverage in Formal Verification, Part 2 Continued…

Recall that three main questions need to be answered to attain coverage in formal verification:

• Part 1 of this series addressed, "How good are my formal constraints?"
• In Part 2 we showed debugging of over-constraining with help of examples, addressing the question, "How good is my verification proof?"
• In a subsequent post we will address the third key question "How can I feel confident my verification is complete?"

In this continuation, we are addressing a different facet of question 2, "How good is my verification proof?"  Let's start with a short recap of concepts introduced earlier in the series, using the now familiar process diagram as a guide:

* Recall how in Part 1 we showed how automatically generated dead-code and FSM-state checks were used to generate "reachable" coverage during "constraint development and design exploration" and "checks development and bug hunting" phases. The point: at the end of these phases we know that the "constraints" are in good shape.

* With the constraints all set, a sufficiently large number of legal traces can be generated.  Conversely, we also know that no illegal traces will be generated as the checks are not failing.  Hence, proofs at this stage are also in good shape.  Rephrasing in official formal verification jargon, "the proofs are sound for all reachable coverage behavior."

* In fact, at this stage a coverage number can now be provided for all proven checks.  Additionally, some functional coverage points are automatically generated for the checks; where Incisive Enterprise Verifier (IEV) automagically extracts trigger and witness trace covers for the checks.  For example, if you had a check like this:

//psl A1: assert always ( {req} |=> {req[*1:5]; ack && !req}) @(posedge clk);

IEV will automatically generate trigger "cover  ({req} @ (posedge clk))" and witness "cover {req;req[*1:5]; ack && !req} @(posedge clk)".  Even better: you can have the tool display the corresponding waveforms showing the check enabled and finished once so you can completely confirm that there is no basic flaw with check itself.

* Proven checks cannot fail on allowed behaviors from constraints.  In terms of coverage, proven checks could be given "reachable coverage" numbers.  For example, if 2% line of RTL is unreachable and rest 98% (100-2) lines of code are reachable then one could claim that "reachable coverage" is fully done.  Of course, one must examine the unreachable code and manually qualify it as being OK. Once unreachable code is blessed, we could assign 100% "reachable coverage" number to all proven checks.

Clearly if all of the above bases are touched, feelings of confidence and inner peace with respect to the question, "How good is my formal proof?" will well up inside you.

HOWEVER:

Before you pop open the champagne, there is one possible remaining "gotcha" -- what about checks that come up inconclusive or "Explored"?

Since proofs provide mathematical certainty, the best initial courses of action are almost always to either give the tool a bit more time to run, try some different formal algorithms, or apply some basic abstractions to improve the chance of getting a proof.  Granted, you might still be left with explored checks no matter what you try -- but all is not lost!  We can easily shift over to the simulation world and leverage the Incisive Enterprise Simulator XL (IES-XL) embedded inside IEV to apply simulation-centric coverage-driven verification approaches. You would also need planning tool to manage your checks, formal and simulation runs.  How is this done?  Stay tuned for the next installment of this series ...

Until then, happy verifying!

Vinaya Singh
Architect
Cadence R&D

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

Reference Links:
Part 1 and Part 2 of the series; plus more on the Incisive Enterprise Verifier (IEV) tool mentioned above.