JasperGold COV App, the Swiss Army Knife for Verification

At the Jasper Users Group meeting in October Rajeev Ranjan presented on the JasperGold COV App which he described as the Swiss army knife for verification. It comes in many sizes and contains many useful tools.

The primary goal of COV is to provide coverage metrics:

• stimuli coverage: how restrictive is the design behavior under the formal set up?
• property completeness coverage: how complete is the property set?
• proof coverage: what coverage is achieved by the proven properties?
• bounded proof coverage: what is the coverage and is it enough?

That last item, bounded proof, is used when only a subset of the state-space can be traversed and no violation is encountered. But it is not a full proof. A bounded proof of K cycles implies that all states reachable within K cycles of the reset state have been analyzed and all possible events with K cycles have been triggered.

It is also integrated in with the simulation database since formal doesn’t live in a verification world of its own and assertions that are covered by simulation do not need to be covered by formal and vice-versa. There is a special flow that can be used to improve simulation coverage with the unreachable coverage target detection flow, whereby JG coers items that are not hit in simulation and also confirms items that are unreachable and thus cannot be covered by simulation.

Different companies use the tool in different ways. Customers include Broadcom, ST, ARM, Applied Micro, Juniper, Nvida and others. Different usage models include:
[LIST=1]