800x100 static WP 3
WP_Term Object
(
    [term_id] => 157
    [name] => EDA
    [slug] => eda
    [term_group] => 0
    [term_taxonomy_id] => 157
    [taxonomy] => category
    [description] => Electronic Design Automation
    [parent] => 0
    [count] => 3886
    [filter] => raw
    [cat_ID] => 157
    [category_count] => 3886
    [category_description] => Electronic Design Automation
    [cat_name] => EDA
    [category_nicename] => eda
    [category_parent] => 0
)

JasperGold COV App, the Swiss Army Knife for Verification

JasperGold COV App, the Swiss Army Knife for Verification
by Paul McLellan on 01-16-2014 at 12:55 am

 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]

  • Verification coverage for bounded result (property checking, sequential equivalence checking)
  • Completeness of property set
  • Protecting against over-constraint, dead-code analysis
  • Verification coverage from full-proof analysis
  • Post-silicon debugging
  • Detect and eliminate unreachable cover targets for simulation
  • Assist simulation in reaching a hard to reach target

    Another facet is protection from over-constraints. Assumptions (constraints) limit the set of legal stimuli but assumptions can interact in complex ways resulting in conflict (not easily identifiable by eyeballing). This leads to the danger of false confidence for proven properties and so should always be used as a sanity check for all the proven properties. A special case is identifying dead code that cannot be reached, which can often lead to very fast identification of RTL bugs early in the design cycle.

    There is more in the presentation. If you are a Jasper user (not necessarily one who attended JUG) then you can download the presentations, including this one, here.


    More articles by Paul McLellan…

    Share this post via:

  • Comments

    There are no comments yet.

    You must register or log in to view/post comments.