MP Associates, Inc.

THURSDAY March 01, 8:30am - 12:00pm | Cascade

Formal Verification – Breaking Through the Knowledge Barrier
Sean Safarpour - Synopsys, Inc.

Shaun Feng - Samsung Austin R&D Center
Syed Suhaib - NVIDIA Corp.
Mandar Munishwar - Qualcomm Technologies, Inc.
Iain Singleton - Synopsys, Inc.
Kiran Vittal - Synopsys, Inc.

Formal Verification has become a mainstream verification technology and methodology. Over the previous two decades, early adopters paved the way to demonstrate how formal verification can improve quality and timelines by catching more bugs faster and with higher confidence. While the technology itself is deployed at many hundreds of companies in the form of property verification, bus protocol verification, connectivity checking, coverage closure and many other applications, there are still relatively few design or verification engineers who get the maximum value out of formal verification. The reason for this productivity gap is that advanced formal verification knowledge acquired over dozens of projects and many years is not readily accessible to the general public and limited to the confines of the experts.

In this tutorial, the top-most industry leaders in formal verification attempt to break the knowledge barrier. They will introduce, teach and provide detailed analysis on some of the most advanced formal verification techniques. Topics covered are:

- Describe abstraction both from a concept and practical perspective. Walk through case studies and describe the impact of this technique on getting proofs and unearthing deep bugs.
- How to efficiently verify blocks with common but dreaded data structures such as such as FIFOs, RAMs and caches with formal verification along with concept of symbolic variables
- How to effectively close inductive-based proofs with invariants. This technique is very powerful in getting full proofs for certain types of properties, although few are aware of how to use it.
- How to sign-off complex blocks entirely with formal verification. Unearth short comings in terms of assertions and verification holes in over-constraint analysis
- How to perform Architectural Formal Verification to prove correctness of Coherency Models. Coherency is a key requirement of a multi-processor system and it is of utmost importance to the functionality of the design. Usage of stale data due to bugs in implementation of coherency protocol may result in illegal behavior. Armed with this knowledge, verification engineers will be able to improve their overall efficiency with formal verification.

Thank You to Our Sponsor: