Breakfast Bytes Blogs

Paul McLellan

Jasper User Group: Ziyad's State of the Formal Union

Last week was the Jasper User Group where we announced the Jasper C2RTL App. It was actually announced during Ziyad Hanna's presentation which opened the meeting. Ziyad wrote about the big picture state of formal verification. At the end of the meeting, Habeeb Farah took a deeper dive into the recent development of Cadence's formal portfolio and how much Jasper technology has improved over the last few years, which I will cover in a future post.

I wrote about C2RTL in two blog posts last week:

ziyad

Ziyad titled his presentation " Verification's Expanding Scope". He started by pointing out that this was the 14th Jasper User Group meeting (and the 8th since the Cadence acquisition) and it continues to be the largest gathering of formal verification professionals.

If you've not been asleep for the last few years, you can't have failed to notice that AI has become increasingly important, and that this has driven new dimensions of complexity:

  • On-device AI revenue growing with a CAGR of 37% forecast to reach $50B by 2025
  • Big data means fast-changing, unpredictable, low-latency, multi-level processing
  • Pervasive connectivity brings unprecedented security concerns

verification complexity

These features lead to an exponential growth in verification complexity and cost. Verification grows as 2N meaning that simulation becomes less effective. Over 40% of the cost of verification is spent in debug. Formal verification has the best fit to address the throughput and productivity in debug in IP design and SoC design.

Formal verification is in demand. Ziyad looked on LinkedIn and searched for "formal verification" and there are more than 70,000 hits. There are more than 2,000 jobs in formal open...just in the US. Jasper has had 53% growth in the last two years, with core formal at 61%, designer apps at 73%, and verification apps as 32%.

Ziyad then introduced Jasper University. This provides self-paced virtual or instructor-led classes to get certified on Jasper apps and methodology. There is third-party management of certifications (for more on that, see my post Badges—Not Just for Scouts Anymore). There are three levels: foundational, intermediate, and advanced. More certifications will be added.

How to Cope with System Design and Verification Complexity?

This example design was used through both Ziyad and Habeeb's presentations. The blocks in the design are probably connected with a coherent interconnect or fabric. The subsystems vary with all kinds of functionality including graphics cores, compute cores, DSP cores, controllers, memory controllers, and kinds of applications like neural domains. This is not a real design but it is realistic of many designs, hooking hundreds of IP together.

Formal is expanding in multiple dimensions because it has become so successful. It already uncovers 35-50% of logic bugs while consuming only 10% of verification resources. This makes it 3-5X times more effective than simulation and so it is already having a big impact on verification complexity. Many customers are reporting the same throughput with formal. But we can do more by expanding:

  • Expand by allowing engineers to tackle more problems using more apps. We see big demand for additional use cases, too.
  • Expansion from formal specialists to designers and verification engineers. Some of our customers are shifting verification engineers from dynamic verification (simulation, emulation, and prototyping) to formal.
  • Expansion of formal to specific domains such as functional safety, security, and low power.
  • Moving above RTL to verify software, C++ models (C2RTL announcement coming up!)

Ziyad went deeper into five categories of verification, but you'll need to watch the presentation to get the details. The five categories were:

  • Fabric verification
  • ISA verification
  • Security and safety verification
  • Protocol verification
  • SystemC/C++ verification

C2RTL

Ziyad then announced the Jasper C2RTL App. I covered the details of this in my posts last week, so I won't repeat everything that he said here. This is the first app that extends the power of Jasper above RTL. And Ziyad hinted about more to come:

More apps in this domain will be rolled out in the future.
...
The C2RTL app handles handwritten RTL. Handling high-level synthesis design will be for another time.

There are two parts to the C2RTL app, a range of new formal engines that handle world-level and bit-level operations, pipeline stalls, feedback, loops, and other challenges. At the language side, it supports C++ standard libraries, STL templates, Boost library, Berkeley Softfloat library, IEEE 754 floating-point, SystemC datatypes, and more.

Summary

  • Formal verification engineers are in demand like never before
  • Formal for RTL verification is growing fast
  • ROI for formal growing faster than other methods (more bugs found per person-hour and per machine-hour)
  • Jasper technology is expanding above RTL to C++ with C2RTL being the first app

The potential for formal verification's future is limitless!

 

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

Tags: