Wait, didn’t Cadence just acquire Jasper. Why is there a Jasper at DAC post?
So the big event is lunch on Tuesday, on Treasure Island. For out of towners that is the island in the middle of the bay bridge (actually just half of it). Food trucks, awesome views of the bay, and really cool street performers. There will be street magic, a live band, a juggler, and a very unique bubble blower that will blow bubbles with people inside them! Full details and registration here.
Of course there is stuff going on in the booth too. Booth 2033. Two seminars, presented several times a day.
Low power: 3 Ways Jasper Can Reduce Your SoC’s Power Consumption Now
Low power optimization techniques significantly impact the structural and behavioral elements of your original design. Such changes can be very difficult to verify in simulation, whereas formal analysis enables exhaustive verification. In this seminar we will show three methodologies that leverage Jasper’s Formal Apps to automatically generate assertions and data that verify that the power description matches UPF/CPF power intent & guidelines, and verify that the power intent does not create any new hazards. Specifically, clock gating, retention optimization & partial retention verification, and the fundamental enabling of more power domains & increased complexity will be shown in context of case studies where these flows have saved substantial schedule time and power budget on real world projects.
5 Ways Formal Can Offload (and even replace) Simulation Today
Since formal analysis was productized over a decade ago, engineers, CAD managers, and EDA vendors have often speculated how and when this technology would proliferate. This isn’t just an academic question given the very compelling fact that formal analysis provides exhaustive results for any problem it’s applied to. Wouldn’t it be great if the many uncertainties around the completeness of verification could eventually be eliminated with this powerful technology? In this seminar we will show how formal is the “right tool for the job” in five popular use cases that were once the exclusive province of simulation. For example, in some cases – like SoC Connectivity checking — formal can displace simulation completely. However, in flows like X-Propagation verification, simulation and formal can be used side-by-side to achieve the necessary confidence level. References to real world customer reports will be included.
Also, Broadcom and NVidia are presenting as part of the designer track.
Formal and static methods, which analyze a design directly rather than depending on large numbers of simulation vectors, are becoming increasingly important in the world of modern design. In the first part of this session, real-world practitioners who have been successful with formal verification describe case studies and use them to supply useful advice for those who wish to achieve similar results. Then we move on to describe some new and powerful uses for static and formal techniques in conjunction with other tools and methods, providing new insights into IP integration, clock domain crossings, power issues, and clock/reset design.
But wait, there’s more. A couple of Design Insight Tutorials.
DAC INSIGHT: Using Formal to Achieve Coverage Closure
Whether using simulation or formal methods, achieving verification closure requires the design team to answer the following questions with a high degree of confidence:
1. Does the verification environment sufficiently analyze the design to confirm the DUT meets the product specification?
2. Which parts of the design and use cases have been fully verified, and which need more attention?
Answers to these questions require analysis not only of stimuli coverage, but also of observation coverage, that is, the extent to which responses to stimuli are actually observed by the verification environment.
The exhaustive nature of formal methods encompasses both stimuli and observation analysis and coverage. In contrast, dynamic methods apply stimuli and measure only stimuli coverage. Dynamic methods cannot measure observation coverage, making verification closure tedious, time-consuming and uncertain.
This session will cover various coverage metrics for formal verification and provide a recommended methodology towards how formal verification technology and the associated metrics can be leveraged to accelerate the overall coverage closure process; and in the process reduce – and in some cases make redundant – corresponding dynamic simulation efforts.
DAC INSIGHT: Formally Addressing Hardware Security
Complex SoC’s, such as those for cell phones, game consoles, medical devices, vehicles, and servers contain secure information that’s valuable for unauthorized parties to exploit. Unfortunately, manual inspection by experts doesn’t scale, and simulation-based or emulation approaches rely on the inconsistent hacking abilities of verification engineers. Inevitably many corner cases are left unchecked, leaving open pathways for attackers. This session will focus on formal methods to tackle security verification challenges and make hardware impervious to attackers. Specifically, it will demonstrate how formal verification can be used exhaustively prove that attackers cannot breach the hardware authentication logic and registers, and/or read or alter the secure data through illegal logic paths. All of the above will be demonstrated in the context of several real-world case studies.
Details on the Jasper website here.
More articles by Paul McLellan…
Next Generation of Systems Design at Siemens