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.

(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