feature article
Subscribe Now

Formal in the Cloud

OneSpin’s New Spin on Cloud Computing

The cloud is the future of everything, they say. You won’t need a computer anymore, they say. Just a phone and ubiquitous connectivity are all you need, they say (you never, ever lose your connection, do you?).

While it hasn’t completely turned our lives upside down yet, yes, the cloud has worked its way into more and more things. And we’ve seen it tip-toe into the world of EDA, although it’s not clear that it’s really sticking so far, and it has some detractors, and there are even those who went to the cloud and then left again.

So was that not such a good idea? Is the cloud for EDA going the way of push technology?

Well, not so fast. OneSpin recently announced their use of the cloud. Yes, they’re aware of the other things going on, and they appear to have done their homework and were ready for the many questions I had for them. They’re doing things slightly differently from others, and they have what they believe to be a solution to the Achilles’ heel of EDA cloud solutions – a solution that’s unique to their EDA field.

First, and key to how they’re doing this, let’s review who OneSpin is. We looked at their formal technology a long, long time ago, and they again popped their heads up a couple of years ago. But, for the most part, things have been really quiet. Then, more recently, they shuffled management, and they’re now taking a more aggressive tack in the market.

This, then, is their first big announcement of the new initiative. Their fundamental tools aren’t that different (from a high level); it’s more like they’re working harder to get their message out and they’ve got a new way to use the tool.

So why can OneSpin use the cloud when it’s not a clear win for others? Well, a lot of it relates to the fact that they do formal analysis, so what they’re doing won’t necessarily work for other types of tools. The huge objection to cloud computing is security: no one wants to upload a design into the cloud because the design contains crown jewels. With most other tools, you end up pushing significant contiguous portions of a design (if not the whole thing) up to the cloud, and that makes a lot of folks nervous.

Yes, you can obfuscate and encrypt, but it seems to leave a nasty feeling in the pit of people’s stomachs, and no matter how rational we all try to be, we’re still guided by our guts. So the explanations of why security shouldn’t be an issue (even ones like the fact that cloud providers like Amazon may have better security than internal corporate farms) satisfy the head but not the heart.

And that’s where OneSpin is different. Or wants to be viewed as different. (It is, in fact, different, but whether that settles the gut is another matter.) Formal verification consists of a series of proofs. You go through the design and prove a series of properties. Exactly what you’re proving depends on the problem you’re solving (since formal is really nothing more than a technique useful for specific kinds of verification). But that’s the key: a proof is a proof is a proof, in the abstract. By itself, it contains no design information.

So OneSpin does most of its work at the client side. It sends only individual proofs into the cloud, and those proofs are abstracted.

If you’re familiar with software design patterns, it’s a similar thing. A design property to be proved is a specific embodiment of a more general proof in the same way that a specific software object may extend an abstract design pattern. So instead of working with the specifics, the abstract equivalent is used. The tool returns only true/false information and, if true, the cases that make the proof true. It’s up to the client to translate that abstract information back into something relevant for the actual design.

This means that the only fundamental part of their tool that resides in the cloud is the “sat solver,” which proves (or not) the satisfiability of some statement. You toss the statement over and it does the proof (or disproof). No actual names from the design are used. Because each of these goes up one at a time, and because they can be sent to different servers, no one server ever has access to anything more than the one proof it’s working on – it never sees the entire design.

The servers also use no local storage, so there’s no way that the accumulation of proofs could somehow build up a complete picture of the design. In addition, all ports except the one communicating with the client are closed, so not even Amazon can talk to the engine.

Frankly, even if all of the proofs could be seen together (which they can’t), it still doesn’t provide all of the information about the design, by a long shot. You might learn some local relationships about various signals, but you wouldn’t know which ones, and you wouldn’t be able to relate them to each other, so you could never assemble the entire design. The entire design is never transmitted, whether at one time or cumulatively.

As a result, they think they’ve effectively neutralized the perceived security weaknesses of the cloud.

They also have a very different business model for this. One that keeps them from getting involved in the money side of the transactions – which can be attractive for small companies like OneSpin. It doesn’t take too much awareness of the world to know that having to deal with customer credit cards and online transactions and worrying about hacking and such is a pain. So instead, they have Amazon do that bit.

You download a free client program from their website to get things going. Then you go to Amazon to purchase the service. It’s a pay-as-you-go model, with one-hour minimum increments, priced starting at $25/hr. The setup is something that would typically be done by a project manager or CAD management team, not the actual user. In fact, once this is in place, cloud usage happens transparently to the user.

Note that they’re not abandoning their existing usage model. It’s just that time-based licenses can be less cost-effective for small companies. They’ve estimated that the cross-over point is about 600 hours, or $15,000 per year: more than that and standard licenses work best; less than that and the cloud model looks more attractive.

So users can work entirely on the client side, entirely through the cloud, or supplement the client side with extra cloud resources during peak usage.

They were in a closed beta when they announced, and by now they should be in an open beta program; they plan on a full release in September. We’ll definitely have to watch and see whether this gets more traction than other EDA cloud solutions.


More info:

OneSpin’s cloud solution

OneSpin’s cloud announcement

2 thoughts on “Formal in the Cloud”

Leave a Reply

featured blogs
Apr 22, 2021
President George H. W. Bush famously said that he didn't do "the vision thing". Well, here at Cadence we definitely do the vision thing. In fact, the Tensilica Vision DSP product line... [[ Click on the title to access the full blog on the Cadence Community si...
Apr 21, 2021
Robotics are everywhere, or so it seems. Robot combat, STEM outreach, robotic arms and advanced surgical devices are but a few applications that touch our everyday life. As a student, I was the President of the Santa Barbara City College Robotics Club and a FIRST Robotics com...
Apr 21, 2021
Introducing PrimeLib, an SoC design tool that maps the latest chip technologies & enables correct-by-construction design for SoCs at advanced process nodes. The post Advanced Nodes Drive Demand for Advanced Library Characterization and Validation Solutions appeared firs...
Apr 20, 2021
By Sherif Hany and Abdellah Bakhali Regardless of which technology node they're using, design houses… The post Give me my space! Why high voltage and multiple power domain designs need automated context-aware spacing checks appeared first on Design with Calibre....

featured video

Learn the basics of Hall Effect sensors

Sponsored by Texas Instruments

This video introduces Hall Effect, permanent magnets and various magnetic properties. It'll walk through the benefits of Hall Effect sensors, how Hall ICs compare to discrete Hall elements and the different types of Hall Effect sensors.

Click here for more information

featured paper

Understanding Functional Safety FIT Base Failure Rate Estimates per IEC 62380 and SN 29500

Sponsored by Texas Instruments

Functional safety standards such as IEC 61508 and ISO 26262 require semiconductor device manufacturers to address both systematic and random hardware failures. Base failure rates (BFR) quantify the intrinsic reliability of the semiconductor component while operating under normal environmental conditions. Download our white paper which focuses on two widely accepted techniques to estimate the BFR for semiconductor components; estimates per IEC Technical Report 62380 and SN 29500 respectively.

Click here to download the whitepaper

Featured Chalk Talk

Electronic Fuses (eFuses)

Sponsored by Mouser Electronics and ON Semiconductor

Today’s advanced designs demand advanced circuit protection. The days of replacing old-school fuses are long gone, and we need solutions that provide more robust protection and improved failure modes. In this episode of Chalk Talk, Amelia Dalton chats with Pramit Nandy of ON Semiconductor about the latest advances in electronic fuses, and how they can protect against overcurrent, thermal, and overvoltage.

More information about ON Semiconductor Electronic Fuses