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
Nov 15, 2024
Explore the benefits of Delta DFU (device firmware update), its impact on firmware update efficiency, and results from real ota updates in IoT devices....
Nov 13, 2024
Implementing the classic 'hand coming out of bowl' when you can see there's no one under the table is very tempting'¦...

featured video

Introducing FPGAi – Innovations Unlocked by AI-enabled FPGAs

Sponsored by Intel

Altera Innovators Day presentation by Ilya Ganusov showing the advantages of FPGAs for implementing AI-based Systems. See additional videos on AI and other Altera Innovators Day in Altera’s YouTube channel playlists.

Learn more about FPGAs for Artificial Intelligence here

featured paper

Quantized Neural Networks for FPGA Inference

Sponsored by Intel

Implementing a low precision network in FPGA hardware for efficient inferencing provides numerous advantages when it comes to meeting demanding specifications. The increased flexibility allows optimization of throughput, overall power consumption, resource usage, device size, TOPs/watt, and deterministic latency. These are important benefits where scaling and efficiency are inherent requirements of the application.

Click to read more

featured chalk talk

STM32 Security for IoT
Today’s modern embedded systems face a range of security risks that can stem from a variety of different sources including insecure communication protocols, hardware vulnerabilities, and physical tampering. In this episode of Chalk Talk, Amelia Dalton and Thierry Crespo from STMicroelectronics explore the biggest security challenges facing embedded designers today, the benefits of the STM32 Trust platform, and why the STM32Trust TEE Secure Manager is an IoT security game changer.
Aug 20, 2024
39,810 views