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 25, 2024
Cadence's seven -year partnership with'¯ Team4Tech '¯has given our employees unique opportunities to harness the power of technology and engage in a three -month philanthropic project to improve the livelihood of communities in need. In Fall 2023, this partnership allowed C...
Apr 24, 2024
Learn about maskless electron beam lithography and see how Multibeam's industry-first e-beam semiconductor lithography system leverages Synopsys software.The post Synopsys and Multibeam Accelerate Innovation with First Production-Ready E-Beam Lithography System appeared fir...
Apr 18, 2024
Are you ready for a revolution in robotic technology (as opposed to a robotic revolution, of course)?...

featured video

How MediaTek Optimizes SI Design with Cadence Optimality Explorer and Clarity 3D Solver

Sponsored by Cadence Design Systems

In the era of 5G/6G communication, signal integrity (SI) design considerations are important in high-speed interface design. MediaTek’s design process usually relies on human intuition, but with Cadence’s Optimality Intelligent System Explorer and Clarity 3D Solver, they’ve increased design productivity by 75X. The Optimality Explorer’s AI technology not only improves productivity, but also provides helpful insights and answers.

Learn how MediaTek uses Cadence tools in SI design

featured paper

Designing Robust 5G Power Amplifiers for the Real World

Sponsored by Keysight

Simulating 5G power amplifier (PA) designs at the component and system levels with authentic modulation and high-fidelity behavioral models increases predictability, lowers risk, and shrinks schedules. Simulation software enables multi-technology layout and multi-domain analysis, evaluating the impacts of 5G PA design choices while delivering accurate results in a single virtual workspace. This application note delves into how authentic modulation enhances predictability and performance in 5G millimeter-wave systems.

Download now to revolutionize your design process.

featured chalk talk

It’s the little things that get you; Light to Voltage Converters
In this episode of Chalk Talk, Amelia Dalton and Ed Mullins from Analog Devices chat about the what, where, and how of photodiode amplifiers. They discuss the challenges involved in designing these kinds of components, the best practices for analyzing the stability of photodiode amplifiers, and how Analog Devices can help you with your next photodiode amplifier design.
Apr 22, 2024
452 views