Does formal verification support code coverage?
Answered by Anshul Jain | May 20, 2020
Yes, formal verification supports as much code coverage as simulation does – and more! However, the way we use code coverage in formal verification is very different from the way we use it in simulation.
Read on for the complete answer…
Gone are the days when formal verification was not equipped with code coverage. We have come a long way in integrating code coverage as a standard feature of formal verification.
The general purpose of code coverage remains the same, i.e., find the reachability holes in the design, which arise from a lack of input stimulus and from deadcode. However, the root-cause of insufficient input stimulus is different in formal verification vs. simulation. In simulation, code coverage holes are indicative of insufficient quality and quantity of tests, whereas imperfect code coverage in formal points toward a presence of over-constraints in the setup or insufficient runtime of the formal proof.
The aforementioned difference between formal and simulation is primarily because of the fact that simulation uses a zero-plus (0+) approach and formal uses an infinity-minus (∞-) approach. In simulation, we start from zero coverage and we add tests to provide input stimulus that exercises different pieces of code and improves code coverage over time. However, theoretically, we start from infinite input stimulus (legal as well as illegal) in formal. With enough runtime, formal tools will end up covering all the code. It is when we run the checkers that formal tools will throw false counterexamples at us and we then need to add appropriate constraints to disallow illegal stimulus. Adding constraints may lead to a reduction in code coverage.
Consider the following piece of code where error and error_type are inputs to the block:
If line coverage indicates line #10 as uncovered, then
- In simulation, considering only one error scenario is exercised per test, it would mean that enough tests have not been run to cover the scenario where TIMEOUT error occurs
- In formal, it would mean that TIMEOUT type of error has been over-constrained (formal tools will also report the constraints involved)
Coming back to what else formal offers in terms of coverage, formal’s reachability coverage is helpful in determining the deadcode of the design. Due to the exhaustive nature of the technology, formal not only tells you what is reachable (hence, coverable), but also proves what is not reachable. Consider the following piece of code:
Once you run formal code coverage on the above code without any constraints, you will see line 9 reported as unreachable. Since there was no constraint in place, the entire input space (legal + illegal) was available for formal to explore. Therefore, line 9 can be marked as deadcode, exported to a waiver list and used to compliment coverage analysis in the system-level simulation environment.
What you can do with formal coverage doesn’t stop there. Formal coverage also offers help to verifiers by flagging observability issues using Cone-Of-Influence (COI) coverage. It is an inexpensive way of flagging a section of code which is not getting verified at all i.e., none of the checkers in your formal verification testbench are able to verify that section of code. Since COI coverage is only a structural check, it therefore generally adds small value. However, it can help you get the low hanging fruit.
There is still more to formal coverage. Most of the commercial formal verification tools have added more ways of flagging observability issues with the formal verification testbench in the form of proof-core coverage, mutation coverage, etc.
To summarize it all, formal verification now supports enough coverage (see the figure below) to help build confidence in the design as well as measure the quality of verification effort.
Want to explore formal coverage? — #AskOski