Adaptive formal verification platform opens up testing to third parties

Paul Boughton

German design tool expert OneSpin Solutions has developed an adaptive formal technology platform that allows third-party companies with limited knowledge of formal technology to develop and deliver formal-based verification tools, writes Nick Flaherty.

360 LaunchPad is a complete formal environment that can be used by developers without in-house formal technology or expertise. It allows domain experts to efficiently create formal-based solutions targeting their field on a proven underlying verification foundation. LaunchPad may be delivered as part of a verification app by the developer or the app can be included in the OneSpin App Library to operate with the company’s formal product line.

“LaunchPad is a missing link in the widespread adoption of formal verification, and will extend the reach of powerful formal techniques into new areas,” says Dr Raik Brinkmann, OneSpin Solutions’ president and CEO. “The pre-existing platform makes it easier and quicker for domain experts to develop a robust verification solution suitable to their market segment, without the need for acquiring in-house formal knowledge or technology.”

To date, Agnisys and Tortuga Logic have integrated LaunchPad into their systems realisation and security software solutions, respectively. Both have executed Original Equipment Manufacturer (OEM) agreements with OneSpin. For example, security verification expert Tortuga Logic has delivered LaunchPad as part of its Prospect product line.

“Rigorous verification is a critical aspect to fully and exhaustively testing the security facets of a modern semiconductor,” notes Jason Oberg, Tortuga Logic’s president and CEO. “With OneSpin’s LaunchPad, we were able to catapult Prospect, our hardware security solution, into the marketplace with a robust and reliable formal platform, introducing a specific verification solution for a complex, growing need.”

The use of focused verification apps targets powerful, formal-based technology at certain design challenges. These apps provide in-depth, specific verification solutions in an automated fashion, often eliminating the need for end users to write assertions while improving ease-of-use.

Traditionally, apps are built into formal verification tools and, therefore, must be developed and delivered by the formal verification tool vendor who is required to have expertise in the targeted problem area. LaunchPad eliminates this requirement by encapsulating a complete formal platform in a manner that allows its easy integration into a variety of specialised systems by engineers without a formal technology background.

Specialised, formal-based apps can be delivered by application domain experts, increasing the scope of formal verification to a range of disciplines previously closed to the technology.

Through the use of SystemVerilog-based standards to create an easy integration methodology, LaunchPad can be applied quickly and in an open manner. Because LaunchPad only works with the integrating app, the business model to the end-user can be set to match the app itself.

“ARV-Formal combines OneSpin’s LaunchPad and the Agnisys’ Automatic Register Verification app to ensure register operations in an RTL design under test are formally proven to match the specification,” said Anupam Bakshi, president and CEO of Agnisys. “This enabled us to create a powerful register verification solution very quickly, and could pave the way for a new spectrum of verification solutions.”

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