Oz and Ziyad Look to the Future of JasperGold

At last year's Jasper User Group, the two-day event was opened by Oz Levia, VP of VIP and Formal Solutions. Oz said that it was the 10th Jasper User Group, the fourth since Jasper was acquired by Cadence (I worked for Semiwiki back then and Jasper was a subscriber, so I went to a couple of the conferences back in that era).

Jasper User Group is the world's biggest gathering of formal verification users. As a community, Oz said:

we are all making formal verification essential verification methodology, and we can all learn from each other.

Oz was very proud of what was achieved in the last year: Formal is the fastest growing segment in verification, and Cadence is established as the market leader and the thought leader in the space.

Scalability

Looking forward, Oz said, "the world's largest formal R&D team" will be focusing on scalability.

• 10% of runtime is taken up in debug
• 15% is taken in design compilation
• The other 75% is taken up in actually doing the proofs, which can be divided into convergence and performance

Looking Ahead

Oz went on to lay out some ambitious goals for JasperGold. In fact, the goals are sufficiently forward-looking that the bottom of his slides has the sort of safe-harbor statement usually reserved for earnings calls: "This slide contains forward-looking statements regarding Cadence's business or products. Actual results may differ materially from the information presented here." So I suppose that applies to this blog post, too. I don't think any real engineer thinks that a goal set for three years out is a rock-solid commitment, and they also know that if only rock-solid commitments are going to be in the presentation, then it is going to be limited to things like "We'll improve the GUI", which is so vague that it is easy to guarantee.

Oz gave big picture goals in a number of areas, comparing what Cadence achieved in the last 12 months, what we plan to achieve in the next 12 months, and where we hope to be in three years. But the formal team won't let me put this in writing. Here are the historical results for the last 12 months, but you should have been there if you wanted the 1 and 3 year goals (hint: it's October 10th and 11th this year).

Design compilation: Last 12m: 1.7X gates/sec, memory 44% smaller

Performance: Last 12m: 1.4X properties/sec

Convergence on hard property test cases: Last 12m: 35% non-converging properties now converge

Debug: Last 12m: 2-4X performance improvement on large traces

Augmenting JasperGold with Intelligent Formal Technologies

In a cunning ploy to ensure that everyone stayed to the end of the two-day meeting, the last session of all was Ziyad Hanna, the VP of R&D. He had the task of fleshing out the big picture goals that Oz had laid out earlier. As a motivation to attend next year's Jasper User Group, I should point out that Ziyad said more than this, and the slides weren't published. If you really want to get the scoop on what changes are going on under the hood, then the only way is to attend. Late news: October 10-11, 2018, is the next conference.

Ziyad started by talking about the challenges that have historically limited adoption of formal:

• Scalability
• Resource utilization (both users' expertise and productivity, and CPU and memory)
• Proof power of engines, and engine selection
• Inability to leverage repetitive analysis (learn from one run, whether complete or not, to the next)
• Lack of complete, accurate, and understandable coverage metrics

It doesn't matter much what the question is these days, the answer seems to be machine learning. Well, formal is no different. There is lots of scope for using maching learning and big data to guide how the underlying engines are used, to distribute the solutions across massively parallel compute infrastructure, and generally improve from experience.

There are various flavors of machine learning, and presently there is:

• Collective intelligence, in the JasperGold Expert System
• Reinforcement machine learning in Proof Orchestration
• CNN (convolutional neural network) in deep learning for RTL hot-spot extraction

Ziyad talked about proof engine orchestration. ProofGrid and engines have evolved beyond what most users can follow, with many engines and lots of settings. Just using lowest-common-denominator settings misses out on optimization opporutnities since it is often necessary to make little tweak settings based on proof complexity. Proof Orchestration hids a lot of this from the user and handles it automatically. It's like in the old joke, that we are leaving the push-button age, and entering the age where the buttons push themselves. This has been shipping since March of 2017, and there has been supervised learning on thousands of properties, many proof-related features, and continuous learning and optimization.

How's that working? Customer experience with engine orchestration using machine learning is producing 2-5X proof speedup, and >20% convergence.

Summary

Oz wrapped up the two days (before handing out best presentation awards). 2017 was a great year for formal, not just for Cadence and JasperGold, but for acceptance of formal and a seat at the top table. It has been a couple of decades in the making, but we have transitioned from using formal if you have a PhD and know what you are doing, to formal being an accepted part of verification and, in especially critical cases, a mandated part of signoff.

Save the date! The next Jasper User Group is planned for October 10-11, 2018.

To find out more about JasperGold and formal, start on the JasperGold Formal Verification Platform page.

Sign up for Sunday Brunch, the weekly Breakfast Bytes email.