Jasper User Group 2025: A Recap of Innovations and Insights

The Jasper User Group 2025, the annual must-attend event for the formal community, was hosted on October 29-30 at the Cadence San Jose Headquarters. If you weren't able to join us this year, here is a quick recap:

Submissions

This year, we received a record number of high-quality submissions—reflecting the rapid growth of formal verification adoption and the increasing success of Jasper in the industry. Ultimately, ten conference presentations and more than a dozen poster presentations were selected.

Keynotes

We began with two industrial keynote speeches: Ziyad Hanna, Corp VP at Cadence, spoke on "Supercharging Deep Formal by AI," and Samir Mittal, Corp VP at Micron, discussed "AI in Design of Intelligent Memory." These talks provided great insight into how AI is shaping the future of the industry and formal verification. Additionally, our academic keynote from Prof. Caroline Trippel at Stanford University on "Automated and scalable hardware side channel discovery with property decomposition and model checkers" highlighted practical research on hardware security verification using Jasper property and security verification apps.

Companies

Speakers came from companies large and small, including Ahead Computing, Ampere, Cadence Silicon Solutions Group, Condor Computing, Google, Groq, Intel, Lightmatter, Lubis EDA, Meta, Qualcomm, ST, and TI. In total, os were present at this Jasper User Group event. While at different stages of formal adoption, they shared a common belief that formal verification is critical in achieving bug-free silicon.

Presentations

The technical depth and breadth of customer presentations were outstanding. Topics spanned security-hardened IP, Wolper coloring using Proof Structure, RISC-V memory page-walker strategies, visualization-based debug techniques, liveness convergence, FP-proof methodologies, advanced CDC and power-aware flows, formal coverage scaling, and cloud-driven performance optimization. It was inspiring to see formal technologies driving impact across such diverse domains.

Jasper Apps

Customers mentioned successful applications of many Jasper apps, including Formal Property Verification (FPV), C vs RTL Transactional Equivalence Checking (C2RTL), Sequential Equivalence Checking (SEC), Formal Coverage (COV), Architecture Formal Verification (AFV), Connectivity Checking (CONN), Security Path Verification (SPV), Low Power Verification(LPV), Control Status Register Verification (CSR), and Clock Domain Crossing Verification (CDC). These and other Jasper apps continue to power real-world success and innovation.

Demos

Live demos were showcased during lunch breaks on both days, covering topics such as Jasper AI Assistant, Converging Hard Properties Using State Space Tunneling (SST) Agent, Bounded Formal Signoff Methodology, and how to Level Up Visualize Debug Productivity. Video demos on Front End Silicon Agent (FESA) to generate SVA properties from spec, Proof Agent to auto-create Proof Structure, and Visualize Agent to help identify root cause of counter-examples were also shown.

Attendance

The Cadence auditorium was full throughout both days, with 157 formal leaders, experts, and beginners in attendance. There were vibrant discussions on methodology, technology, and best practices both inside and beyond the session rooms. The energy and collaboration underscored the value of this community. We are proud to sponsor the Jasper User Group each year to support knowledge-sharing, learning, and networking across the formal ecosystem

Awards

The Best Presentation and Poster Awards were chosen by the audience. Congratulations to our winners!

In honor and memory of Jim Kasak, an exceptional contributor, presenter, and multi-time best paper award winner whose legacy continues to inspire our community, this year's Jim Kasak Best Presentation Award went to Fernanda Braga (Google) for her impressive work and presentation on the topic of "Module Coverage: Scaling Formal Coverage Analysis Through Instance and Module Aggregation."

The Best Poster Award went to Ramya Hariharan (Intel) for her dedication and success in architecture formal verification with the topic of "The Pursuit of Golden Specification: Leveraging Architecture Formal with Jasper."

Next Steps

Thanks again to all of the Cadence and industrial formal enthusiasts for making Jasper User Group 2025 an astounding success. The conference content will be available to our customers on Cadence ASK in a few weeks. Please be sure to watch out for it. Next, we'll be meeting with formal communities across France, Germany, the UK, Taiwan, Japan, and China—continuing to share best practices and drive industry-wide growth in formal verification.

Register for the Club Formal Events in Europe on November 18 (Grenoble), November 20 (Munich), and November 25 (Cambridge).