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
Dec 7, 2021
We explain the fundamentals of photonics, challenges in photonics research & design, and photonics applications including communications & photonic computing. The post Harnessing the Power of Light: Photonics in IC Design appeared first on From Silicon To Software....
Dec 7, 2021
Optimization is all about meeting requirements. In the last post , you read about how you can use measurements to optimize a circuit. This post will discuss the use of curve fitting to optimize a... [[ Click on the title to access the full blog on the Cadence Community site....
Dec 6, 2021
The scary thing is that this reminds me of the scurrilous ways in which I've been treated by members of the programming and IT communities over the years....
Nov 8, 2021
Intel® FPGA Technology Day (IFTD) is a free four-day event that will be hosted virtually across the globe in North America, China, Japan, EMEA, and Asia Pacific from December 6-9, 2021. The theme of IFTD 2021 is 'Accelerating a Smart and Connected World.' This virtual event ...

featured video

Synopsys & Samtec Demo PCIe 6.0 IP, Connector & Cable Systems for AI Hardware Designs

Sponsored by Synopsys

This demo features Synopsys’ DesignWare PHY IP for PCIe 6.0, performing at maximum channel loss, with Samtec's connectors in a configurable, GPU-based AI/ML system.

Click here for more information about DesignWare IP for PCI Express (PCIe) 6.0

featured paper

Learn how semiconductor technologies have impacted modern telehealth

Sponsored by Texas Instruments

Remote monitoring of a patient's vital signs, temperature, pulse oximetry and more are becoming more accessible. Discover the evolving semiconductor technologies in the telehealth space.

Click to read more

featured chalk talk

TDK Magnetic Sheets For EMI and NFC Applications

Sponsored by Mouser Electronics and TDK

Today’s dense, complex designs can be extremely challenging from an EMI perspective. Re-designs of PCBs to eliminate problems can be expensive and time consuming, and a manufacturing solution can be preferable. In this episode of Chalk Talk, Amelia Dalton chats with Chris Burket of TDX about Flexield noise suppression sheets, which may be just what your design needs to get EMI under control.

Click here for more information about TDK Flexield Noise Suppression Sheets