In the news

Formal verification has long held promise as a verification tool for the SoC design chain – but the arcane nature of the applied mathematics involved has limited its use to a subset of specific areas. German specialist OneSpin Solutions has now found a way that third parties can build tools on the base of its formal verification “engines”, applying the full power of the technology while retaining full secure over its underlying formal intellectual property.

Looking to create a market in formal verification apps, OneSpin Solutions has launched a software platform that allows third party companies with limited knowledge of formal technology to develop and deliver domain specific formal based apps.

Elektroniikan suunnittelut täytyy ennen toteutusta varmentaa eli verifioida. Formaali verifiointi eli todentaminen matemaattisesti on hyvin hankalaa ja on edellyttänyt erittäin syviä tietoja työkaluista. Nyt saksalainen Onespin on tehnyt formaalista verifioimisesta hyvin helppoa.

Onespin on julkistanut 360 Launchpad -alustan. Kyse on joustavasta alustasta, jolla yritykset voivat kehittää omia formaalin verifioinnin sovelluksiaan kehitystyötä varten.

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.

EDA-företaget OneSpin Solutions tar nu ytterligare ett steg för förenkla användningen av formell verifiering. En ny plattform, OneSpin 360 LaunchPad, kan licensieras av tredjepartstillverkare och ingå som del av applikationsspecifika verifieringsappar.

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.

This week we’re saddling up and taking a ride into the Wild West, where the days are long and the code is even longer. We’re talking about the rough and tumble, SystemC slingin’, HLS wranglin’ assertion-based formal verification. Dave Kelf (OneSpin Solutions) rides with us across the dusty EDA plains of RTL design where we unveil why RTL (and above) is called the Wild West of Design, who exactly is playing sheriff in these here parts, and how design and verification at the RTL level can be corralled once and for all.

An article by Brian Bailey on an expert panel entitled "SystemC: Forever a Niche Player Or Rising Star of Chip Design?" at the DVCon in San Jose, CA during March 2015, which included Raik Brinkmann, CEO of OneSpin.

It is said that everything in EDA takes 10 years to become adopted. SystemC is more than 15 years old and remains on the horizon. How broken is it?