Jasper at DVCon and EJUG

The Jasper European User Group meeting (EJUG) is coming up in a couple of weeks. It will be held in the Munich Hilton (which I have stayed in many times, the S-bahn from the airport pretty much stops in the basement) on April 2nd.

The schedule for the day is:
9:00 AM – Registration and continental breakfast
9:30 AM – Jasper Overview
9:45 AM – Customer Success Stories
10:00 AM – ARM Presentation
10:45 AM – Break
11:15 AM – Port-Based Generic Mechanism for Connectivity by Ericsson
11:45 AM – Efficient IP Bring-up with Jasper
12:30 PM – Lunch
2:00 PM – Advanced Functional Verification for Quality and Productivity Increase by ST
2:45 PM – Low Power Formal Verification with Jasper
3:15 PM – Exhaustive Security Verification with Jasper
3:45 PM – Break
4:15 PM – High-Performance Sequential Equivalence Checking with Jasper
4:45 PM – Coverage Verification with Jasper
5:15 PM – Panel: Efficient Verification Problem Solving with Jasper
-Yann Oddos, Intel
-ARM
-Yousaf Gulzar, Ericsson
-Guy Dupenloup, ST
6:00 PM – Closing remarks and cocktail reception

Registration for EJUG is here.

At DVCon some of Jasper’s customers presented on various aspects of using formal techniques. Prosenjit Chatterjee, Scott Fields and Syed Suhaib from Nvidia presented A Formal Verification App Towards Efficient, Chip-Wide Clock Gating Verification. Clock gating is an important part of SoC design for controlling power. But with multiple clock domains the verification can be complex. nVidia presented a fully automated approached based on top of Jasper’s sequential equivalence checking (SEC) app. The SEC app performs various optimizations automatically to achieve deeper proof bounds or even full proofs, in many cases, taking advantage of the symmetry of the setup. Nvidia apply this methodology across the chip to illustrate its usefulness. They found multiple clock gating bugs across many projects using this approach, where over half of these were found after supposedly high simulation coverage of the design. If you want to find obscure corner cases that are not handled correctly, then formal techniques once again outperform simulation.

Shuqing Zhao, Shan Yan and Yafeng Fang from Broadcom presented Practical Approach Using a Formal App to Detect X-Optimism-Related RTL Bugs. X-optimism is a problem during RTL simulation and with SoCs the size they are, gate-level simulation is simply not practical to eliminate the issues. The JasperGold X-propagation verification app reads in the RTL, analyzes the design, and then automatically implements assertions to check for all X occurrences on targets such as clocks, resets, control signals and output ports. If the formally proved X occurrences are determined by user to be unexpected, it usually implies they were masked in RTL simulation due to X optimism. Broadcom discussed results of this approach using two case studies, a power management controller module and an audio processing module, both of which have design bugs masked due to X-optimism.

And save the date. DVCon next year is March 2-5th 2015. And DVCon Europe is October 14-15th this year (also in Munich like EJUG).

The DVCon website is here.

More articles by Paul McLellan…