Using Formal for Functional Coverage

Brian Bailey’s recent article on “Fixing Functional Coverage” in Semiconductor Engineering (http://semiengineering.com/fixing-functional-coverage/) polled experts from different companies about the challenges of catching all the bugs, utilizing assertions and expanding coverage to the entire system. This blog elaborates on the four points we made in Brian’s article about how formal can help with functional coverage.

Hitting functional coverage goals is a very important task in verification because while other coverage metrics, such as code coverage, toggle coverage, expression coverage, are useful, they don’t guarantee 100% functional correctness of the design. However, reaching all functional coverage goals in simulation is challenging because one has to provide the right input vectors to trigger those coverage points. This is where formal can be used to help achieve coverage closure.

First of all, formal analysis can automatically detect dead code or unreachable states in the design so that verification engineers don’t have to try in vain to reach those coverage points, thereby saving time and effort. Many formal tools on the market offer this capability, and this is the easiest way of utilizing formal to catch design bugs and help reaching coverage goals.

Second, one can write interesting cover properties that represent certain functional behaviors in the design to see if the scenarios are reachable. The results of this analysis, input vectors, could easily be fed into simulation testbench so that those functional coverage points are hit in simulation as well. And if the result is unreachable, then there could be a bug in the design. In our formal verification projects, we also use cover properties to help us understand the required proof depth for the design. So there are multiple benefits of writing cover properties in verification.

Third, because formal is exhaustive, for an assert property written to verify the functional behavior of the design, formal tools can prove whether the property holds in the design or fails. There is no need to simulate that functional behavior once formal achieves full proof (could be bounded or unbounded). Exhaustive analysis, or 100% input coverage, is the key benefit of formal verification.

Last, formal tools also offer coverage metrics to measure the completeness of the formal testbench. Formal coverage can pinpoint over-constraining situation, and help decide when we reach an adequate proof depth for formal sign-off. It is our hope that one day formal and simulation can access the same coverage database so as to truly complement each other in achieving verification sign-off.

In summary, formal technology is a must-have in today’s verification flow, not only in its ability to verify the functionality of the design, but also in its ability to complement simulation in reaching functional coverage goals.

Tags: Brian Bailey, formal technology, formal verification, Jin Zhang, Oski Technology, verification flow

Category: Blog

This entry was posted on Wednesday, August 27th, 2014 at 6:08 am. You can follow any responses to this entry through the RSS 2.0 feed. You can leave a response, or trackback from your own site.