Never miss a story from Breakfast Bytes. Subscribe for in-depth analysis and articles.
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.
Welcome and State of the Union
Keynote 1: CPU Datapath Verification for the Masses
Formal Verification for Instruction Fetch Unit
FSM Automatic Formal Check Methodology for Broad Deployment
HW Security Path Validation Using Formal Methods: Intel Case Studies
Towards Enabling Security Formal Verification of the Load-Store Unit of A-class Arm CPUs using SPV App
Don’t panic if you have a bounded proof: Using Proof Structure with Assume-Guarantee to help with convergence
University of British Columbia
Keynote 2: The Rise and Resurrection of Formal Verification Research
Deep Cove Research
How to Find Black Holes…and Hidden States
Conquering the Challenges in Formal SoC Verification
Proof Convergence in Protocol Verification
Bootstrapping Formal Coverage Analysis
FV Signoff in the Context of Mainstream Formal Verification
Jasper Technology Update
Awards & Closing
See the Jasper User Group page with a link to register. Or click below:
Sign up for Sunday Brunch, the weekly Breakfast Bytes email.