SNPS1301149083 snug sv 2024 semiwiki 400x400 px v2
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] => 3865
    [filter] => raw
    [cat_ID] => 157
    [category_count] => 3865
    [category_description] => Electronic Design Automation
    [cat_name] => EDA
    [category_nicename] => eda
    [category_parent] => 0

Formal Verification, there’s an App for that

Formal Verification, there’s an App for that
by Paul McLellan on 05-06-2012 at 6:00 pm

The success of Apple’s AppStore has made people aware that software doesn’t have to be delivered in a big monolithic lump. Indeed, going back a bit earlier, Apple’s iTunes store made people aware that you didn’t have to buy a whole album if you only wanted a track or two.

EDA applications in today’s server-farm world suffer from another problem: you might want to buy a lot of one capability of a tool, because you use it a lot, and a little (or none) of another capability that you rarely make use of. The monolithic approach lacks this flexibility.

Jasper’s flagship JasperGold product has historically been delivered in a form that included all the capabilities, and at a price point that reflects that breadth. In some ways this works well for formal verification since different proof engines can work together: if you can’t prove something with engine A then maybe engine B can prove it. It only takes one engine to succeed. It’s a bit like solving differential equations. You just have to find some way to come up with an answer that differentiates back to the equation you started with, and it is hard to predict which approach might work.

 JasperGold is being restructured into a sort of backplane consisting of a common database and a common user-interface. Into this backplane you can plug one or more Apps.

The initial Apps that are available are:

  • Formal Property Verification (FPV) App
  • Connectivity Verification App
  • X-propagation Verification App
  • RTL Development App
  • Architectural Modeling App
  • Control/Status Register (CSR) Verification App

In the future additional Apps will be added. There are still a few products (Active Prop Property Synthesis, Post-Silicon Debug and the Intelligent Proof kits) which are still delivered as separate line-items outside of the App infrastructure.

This App approach to delivering capability fits much better with the realities of how design is done today. Very large design teams, large server farms providing compute resource, internationally distributed development.

This App approach (Approach?) makes it straightforward to run multiple applications on the same block, sharing the work product through the common database, and so reducing the total effort for the project. It is easy for a user to run multiple applications on the same block and launch parallel applications through the same user interface. Parallel jobs can be launched through the common interface with the results from all the parallel jobs being collected back into the common database. Overall, it allows for more flexible deployment of software licenses, and thus capabilities, than the monolithic approach.

More details of JasperGold Apps are here.

Share this post via:


One Reply to “Formal Verification, there’s an App for that”

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