feature article
Subscribe Now

Decoupling Formal Technology from Formal Technology

OneSpin Lets Others Build the Apps

Formal verification technology appears in the ascendant at the moment. It’s been around forever, it seems, but it’s now finding its way into more flows than ever.

And that’s because users don’t have to deal with formal technology.

The problem with formal is that it’s hard. And, historically, an investment in formal was best matched by an investment in a PhD or two to help out. Or perhaps by hiring some specialist consultants to help out. The way we’ve started to shake off some of those shackles is through apps. The companies making formal technology realized that they had to target specific problems and then bury the formal bits below a user interface and flow that were more natural to the problem being solved.

Real Intent has been doing this for a while, for example. You’ve got your clock-domain crossing (CDC) solutions. You’ve got tools for linting RTL. You can verify constraints. And so on. Being a step removed from the underlying formal technology makes life easier for the user; the formal vendor takes care of mapping the technology to the problem.

But there’s an important catch here: it’s historically been only the formal tools suppliers that have built these apps, using their own formal technology.

Let’s say you’re a systems house building some specialized box. Perhaps an electronic rat catcher. (Connected, of course, to the internet so that rat data can be uploaded and rat analytics can be computed.) There are a number of sensors and circuits that control when the rat trapdoor closes and when it opens. And you want to be sure that the logic controlling that door is rock solid so that no unanticipated event could inadvertently open the door and release a rat to where it shouldn’t be.

Perfect job for formal. (I think. Work with me here.) But, as a small player in a specialized market (never ever call it a niche when investors are around), what are your options? You could invest in tools and a PhD, but that would probably be outside your budget. Problem is, you’re not likely to be able to talk some formal company into developing a rat-trap app for a market of, probably, one company. And a small one at that.

This is the type of opportunity that OneSpin decided would be worth addressing. They’re doing it with a… what to call it? Dev kit, perhaps… It’s called LaunchPad, and it provides non-formal companies with a way to develop apps that use formal technology. First takers: Agnisys, with a register verification app, and Tortuga Logic, with a security verification app.

The kit itself consists of resources and an API so that the developer can build the user interface and design the way the underlying formal technology is leveraged. When the app is sold, OneSpin’s formal technology is bolted in and included, and a license fee to OneSpin applies (in addition to the price the app-maker charges). If, however, the buyer already has OneSpin’s tools, then the app can be laid over those existing tools, and there’s no extra license fee (but presumably the app price still applies). Obviously there’s some OneSpin proliferation potential here. Coincidence? I think not…

Formal Gaming

There could be, however, the possibility of abuse. Let’s say that a full suite of formal tools costs $30K. (I don’t know actual pricing – I’m using numbers that OneSpin spun in a discussion that included a hypothetical example.) And let’s say that an app designed for rat-trap verification costs a mere $10K. Then let’s say that you notice that the app works by adding certain properties to the RTL specifically for rat-trap verification, annotating them so that the app can recognize which properties to verify.

Well, it’s not rocket science to realize that you could totally game the system here. If you had other unrelated properties that needed verification with a more expensive general-purpose formal tool, you could manually add the rat-trap annotation to all of your properties to fool the rat-trap app into verifying them all, not just the rat-trap ones. You’ve faked the tool out so that you got $30K worth of value from a $10K tool.

I’m calling this “mission hacking.” Pretty nice scam, eh? Well, don’t get too excited. They’re already onto it. Those properties they add for the specific app? Yeah, they’re encrypted. So your brilliant little scheme isn’t going to work. They use standard SystemVerilog encryption, with a symmetric (private) key exchange arranged between OneSpin and the app maker.

While LaunchPad works with OneSpin’s formal technology, it’s not locked to it. As an app maker, you could decide to target someone else’s formal technology. But, to do that, there are two important things that need doing.

First, you need to arrange a key exchange with that other formal technology vendor. As long as that’s squared away, then this will work – because the encryption is standard. To restate a different way, the encryption doesn’t lock the tool into OneSpin because it’s not proprietary encryption. It just prevents mission hacking.

Gentlemen, Pick Your Engines

The second thing you have to do is to get your other formal vendor to put together an engine-picking engine. Turns out this is not trivial.

You see, it’s easy to think of formal technology as this monolithic beast. You somehow adorn your design to its liking, and then you feed the design to the beast. It chews your design up and spits out an answer.

Well, apparently it’s not quite so simple. Formal technology is about running proofs. You want to prove this fact or that fact – usually a whole series of them. So the design gets diced up into proofs (which can even be abstracted and shipped to the cloud for solving). But what’s less obvious to most of us is that there are different engines that can run these proofs, and each engine is good at a particular kind of proof.

OneSpin gives some examples of engines. A couple sound familiar: SAT (satisfiability) and BDD (binary decision diagram). Then there’s BMC and Craig (whoever he is) and PDR and then something mysterious called “Others.” Plus proprietary engines.

It’s not at all likely that an app developer will know which engine to use. So OneSpin has built an engine picker to abstract that problem away. They do provide some flexibility as to how you approach this, however. This engine-picking business isn’t all cut-and-dried. You can set it up to:

  • Force a clear decision (engine A or engine B);
  • Set preferences: First try A, and, if that doesn’t work (after some time), then try B (and then C…);
  • Run A and B (and others) in sequence to see which comes up with the best answer. A better version of this is to run A and B in parallel and take whichever answer converges first.

OneSpin_LaunchPad.png 

(Image courtesy OneSpin)

OneSpin says that this took a fair bit of head-scratching to get right. So any other company that wants to latch onto LaunchPad would need to sort that problem out for their own tools. It’s definitely doable, and OneSpin takes pains to reassure folks that using LaunchPad doesn’t lock anyone in, but it does take work to implement the adaptation to a different tool.

The general good news (for formal) is that, if app makers pick up on this LaunchPad thing, it can bring formal solutions to a far greater range of problems. The app makers need to be experts only in their own domain, not in formal technology. That has the potential to be a huge enabler.

 

More info:

OneSpin LaunchPad

One thought on “Decoupling Formal Technology from Formal Technology”

Leave a Reply

featured blogs
May 17, 2022
'Virtuoso Meets Maxwell' is a blog series aimed at exploring the capabilities and potential of Virtuoso® RF Solution and Virtuoso MultiTech. So, how does Virtuoso meet Maxwell? Now,... ...
May 17, 2022
Explore Arm's SystemReady program, and learn how we're simplifying hardware/software compliance through pre-silicon testing for Base System Architecture (BSA). The post Collaborating to Ensure that Software Just Works Across Arm-Based Hardware appeared first on From Silicon ...
May 12, 2022
By Shelly Stalnaker Every year, the editors of Elektronik in Germany compile a list of the most interesting and innovative… ...
Apr 29, 2022
What do you do if someone starts waving furiously at you, seemingly delighted to see you, but you fear they are being overenthusiastic?...

featured video

Building safer robots with computer vision & AI

Sponsored by Texas Instruments

Watch TI's demo to see how Jacinto™ 7 processors fuse deep learning and traditional computer vision to enable safer autonomous mobile robots.

Watch demo

featured paper

5 common Hall-effect sensor myths

Sponsored by Texas Instruments

Hall-effect sensors can be used in a variety of automotive and industrial systems. Higher system performance requirements created the need for improved accuracy and more integration – extending the use of Hall-effect sensors. Read this article to learn about common Hall-effect sensor misconceptions and see how these sensors can be used in real-world applications.

Click to read more

featured chalk talk

ROHM's KX132-1211 & KX134-1211 Accelerometers

Sponsored by Mouser Electronics and ROHM Semiconductor

Machine health monitoring is a key benefit in the Industry 4.0 revolution. Integrating data from sensors for vibration detection, motion detection, angle measurement and more can give a remarkably accurate picture of machine health, and timely warning of impending failure. In this episode of Chalk Talk, Amelia Dalton chats with Alex Chernyakov of ROHM Semiconductor about the key considerations in machine health monitoring, and how a new line of accelerometers for industrial applications can help.

Click here for more information about Kionix / ROHM Semiconductor KX134 & KX132 Tri-axis Digital Accelerometers