Preview of Jasper User Group 2022

5 Oct 2022 • 3 minute read

cadence connect logo This year's Jasper User Group is coming up later this month on October 19th and 20th. Once again, we are back in person (I'll be there!) on the Cadence campus. There will also be a 3-hour webinar available before the event to provide an introduction to formal techniques in general and Jasper in particular. When you register, you can pick just the conference, just the webinar, or both.

The Jasper User Group is the biggest gathering of formal verification experts in the world. Most of the presentations are by some of these experts who work at companies that are customers of Cadence. So come and learn from the best.

Lunch is provided each day, and there are also demos. Historically, this has all been in building 5, but it is in the process of being remodeled, so I'm guessing this will be in the cafeteria. All will become clear on the day. There is also a reception at the end of the first day.

The table below gives the agenda for the two days. Let me point out some highlights.

As usual, we bracket the two days with two of the most important presentations, so you have to be there at the beginning and stay until the end. The first day opens with Ziyad Hanna giving the state of the formal union and, especially, what advances we have made in Jasper over the last year.

Then the second day ends with Habeeb Farah giving the technology update. This usually has some forward-looking roadmaps that I'm not allowed to write about in my blog posts after the event. You have to be there.

The first-day keynote is by John O'Leary of Intel on CPU Datapath Verification. Intel has a long history of using formal verification. After the infamous floating point bug in 1994, which cost Intel $475M, Intel's management basically said, "Don't ever let that happen again." For more color on that, see my 2012 Semiwiki post Jasper User Group Keynotes. By 1996, Intel was proving the properties of Pentium processors. That was very early (Jasper was not founded until 2002...trivia question, what was its name when it was founded?). Of course, it is no secret that Intel is still designing processors.

The second day's keynote is by Alan Hu of the University of British Columbia, titled The Rise and Resurrection of Formal Verification Research. I'm not sure what he will cover—it seems to me that you have to at least fall before you can have a resurrection.

Full Agenda

DAY 1	Company	Presentation Title	Speaker
9:00-9:45	Cadence	Welcome and State of the Union	Ziyad Hanna
9:45-10:45	Intel	Keynote 1: CPU Datapath Verification for the Masses	John O'Leary
	Break
11:00-11:45	Arm	Formal Verification for Instruction Fetch Unit	Eduardo Zarate
11:45-12:30	TI	FSM Automatic Formal Check Methodology for Broad Deployment	Noor Elahi
12:30-2:15	Lunch/Demos
2:15-3:00	Intel	HW Security Path Validation Using Formal Methods: Intel Case Studies	Alex Levin
3:00-3:45	Arm	Towards Enabling Security Formal Verification of the Load-Store Unit of A-class Arm CPUs using SPV App	Madhu Iyer
	Break
4:00-4:45	HPE	Don’t panic if you have a bounded proof: Using Proof Structure with Assume-Guarantee to help with convergence	Jim Kasak
4:45-6:30	Reception/Posters
DAY 2	Company	Presentation Title	Speaker
9:00-10:00	University of British Columbia	Keynote 2: The Rise and Resurrection of Formal Verification Research	Alan Hu
10:00-10:45	Deep Cove Research	How to Find Black Holes…and Hidden States	Stuart Hoad
	Break
11:00-11:45	Analog Devices	Conquering the Challenges in Formal SoC Verification	Ameya Mulye
11:45-12:30	Marvell	Proof Convergence in Protocol Verification	Shahid Ikram
12:30-2:00	Lunch/Demos
2:00-2:45	Google	Bootstrapping Formal Coverage Analysis	Fernanda Braga
2:45-3:30	Intel	FV Signoff in the Context of Mainstream Formal Verification	Avner Landver
	Break
3:45-4:30	Cadence	Jasper Technology Update	Habeeb Farah
4:30-4:45	Cadence	Awards & Closing

Learn More

See the Jasper User Group page with a link to register. Or click below:

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