OneSpin uses app-store approach to open up formal verification

Formal-verification specialist OneSpin aims to broaden the appeal of its technology by setting up EDA’s equivalent of an app store to showcase not only the company’s own specialized apps for verification but from other tools vendors.

The first companies to sign up for an OEM deal that lets them embed the formal-verification technology in their own products are Agnisys, with a tool for verifying register setups, and Tortuga Logic, which launched its Prospect portfolio of tools several days ago.

“The kernel is a formal engine that we’ve packaged up so that people can plug it into their apps,” said Dave Kelf, vice president of marketing at OneSpin. “Through an OEM agreement, this engine can be plugged into the apps and sold, with the engine tied in, at a price that suits their market.

“We’re trying to create a similar business model to the one that developed around the Apple iPhone with the App Store,” Kelf added.

Apps developed by OEMs can be included in OneSpin’s App Library, which provides access to a number of tools for specific formal-verification tasks.

Products based around 360 Launchpad use standard SystemVerilog assertions to access the formal provers, with encyption employed to ensure that only the app providers have direct access to the assertions. The use of standard assertions means the front-end app code need not be tied to a specific formal engine.

“With most general-purpose formal tools there is so much technology but few users able to deploy it, so you have to charge a lot for each seat. With this, by not making it general-purpose, we can find higher-volume lower-priced markets that are beyond hardware verification. The hope is that we can build an ecosystem beyond pure EDA,” Kelf explained.

“We spent a year conditioning the formal engines to be optimized enough. There is a block that selects the right engine for the right job. The heuristic block needed a lot work to make that work.”

Kelf said companies such as Tortuga gain access to formal technology more easily and with greater control than if they provided scripts for use with third-party tools. “Tortuga has technology that looks at the different ways people form attack strategies against secure hardware. They have patents on it but their problems was that they had this security stuff but no easy access to a formal engine.”

Embedded engine

OneSpin’s 360 Launchpad provides the engine used in the formal version of the Prospect tool, which sits alongside one based on simulation technology. Similarly, the engine sits inside the ARV-Formal tool launched today by Agnisys for verifying RTL register implementations against their specifications.

Anupam Bakshi, Agnisys founder and CEO, said: “Having the agreement with OneSpin enables us to package the complete solution in one bundle. OneSpin gives us flexibility of deployment and ease of use for the customer. The OneSpin tool works behind the scenes so the user does not have to set it up and run it.”

Warren Savage, president and CEO of IPExtreme, said the approach could be used by IP providers: “Formal verification technology may be leveraged to improve many aspects of IP development and integration. OneSpin’s LaunchPad opens up exciting possibilities in the IP space without the enormous technical and commercial overhead of traditional formal solutions.”