feature article
Subscribe to EE Journal Daily Newsletter

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

1 thought on “Formal in the Cloud”

Leave a Reply

featured blogs
Sep 24, 2017
Recently, Renesas combined the Cadence® Interconnect Workbench, the Cadence vManager™ Metric-Driven Signoff Platform, and the Cadence Palladium® Z1 Enterprise Emulation Platform to improve their performance validation flow. They were looking for a better way to...
Sep 21, 2017
Everyone likes to browse the web a little bit differently. Some of us love images, while others are happy to browse text-based webpages all day long. This is why we’ve built a variety of different tools on Samtec.com over the years to assist you with finding the product...
Sep 01, 2017
Achronix was delighted to attend the Hot Chips event in Cupertino once again this August. This year saw a bumper turnout, with some very fascinating speakers providing some great insights into the industry. The Achronix team had a chance to meet with many talented people in t...