OneSpin Launchpad, the App Store for Formal Verification

Formal verification is qualitatively different from most other verification. A simulation can pass or fail. But while formal verification can prove that the circuit is correct, or incorrect, it can also return “not proven” which means either that the algorithms realized that they were not powerful enough to prove a property, or (more often) that the run time got excessive and it gave up. But there are a number of different approaches to formal verification, and it is only necessary for one of the proof approaches to succeed for the property to be proven (or disproven). It doesn’t matter how many algorithms fail to complete so long as one does. As a result of this multiplicity of approaches, formal verification has increasingly been structured in the form of a base application with apps for different proof methods or different proof applications.

The idea of the app as a small code object that runs in a rich environment was pioneered originally by Java apps running browsers, but it was apps on the iPhone (then copied by Android) that really raised their visibility. However, the thing that made apps really take off was when 3rd parties were allowed to create their own apps, and app-stores made distribution of them straightforward.

In formal verification, traditionally the apps have all been developed by the formal verification companies themselves. Today that starts to change. OneSpin announced this morning their 360-DV Launchpad adaptive formal platform. This is a way to allow 3rd parties to develop apps on top of an encapsulation of OneSpin’s formal technology. There are a number of different business models that are possible, depending on what the 3rd party wants:

• OEM: app developer OEM’s OneSpin’s technology “under the hood” and has their own branding, channel etc
• OneSpin App Portfolio: the 3rd party app operates on top of OneSpin-DV verify product, is added to the app portfolio and sold as a reference sell analagous to the app store
• SaaS: OneSpin’s cloud solution can be leveraged for an instant transaction

The app is not locked in to OneSpin’s technology through proprietary APIs. It uses the SystemVerilog encryption standard, and the launchpad internals give a lot of flexibility. Standard FlexLM licensing is used.

So who are some of the people making use of Launchpad?

• Tortuga Logic’s Prospect is automated security solution. They OEM launchpad as part of their solution and prospectively look for security issues in hardware such as insecure access to protected regions, encryption keys being exported, and so on
• Agnisys ARV Formal Register Verification: this takes an English description and formally proves correct operation of the register map and its operation

The big three EDA companies have all acquired and/or developed formal solutions and OneSpin is the only other company focused on formal solutions. Even so a bit of background is probably in order, especially as it is easy to forget that there is a whole EDA world out there beyond the hills around silicon valley.

OneSpin was founded in 2005 as a spin-out of Infineon’s formal verification group. As you might guess with that history it is based in Germany. It has over 30 customers around the world, including many of the top tier electronic companies, and has around 30 employees. Their product line includes automated design analysis, advanced coverage-driven assertion-based verification, and FPGA equivalency checking.

Augmenting traditional simulation-based solutions with formal-based applications has been proven to accelerate the verification process, improve the probability of finding issues, and in some cases provide brand new solutions to difficult challenges. This has lead to a 40% CAGR in the $170M (EDAC 2014) formal verification market.

So the basic idea of Launchpad is that all the expertise and ideas for formal approaches are not inside any one company such as OneSpin (or any of the other guys for that matter). Formal apps can go further if the development is opened up to expert developers.