Three engineers with more than 60 years of combined industry experience with formal verification will share insights on formal sign-off methodology, cache coherence verification, as well as real-world formal experience verifying NVIDIA Denver CPU. Speakers include one of the pioneers of formal verification, Robert Kurshan, CPU and Tegra Formal Verification Team Manager NVIDIA, Syed Suhaib, and Oski CEO, Vigyan Singhal.
- Formal sign-off is used to verify a design block using formal verification without simulation. Vigyan Singhal will present on End-to-End checkers, and explain what they are, how to write them efficiently to achieve formal sign-off.
- Syed Suhaib will share insights on real-world formal experience verifying the recently announced NVIDIA Denver CPU.
- Robert Kurshan will talk about formal verification of cache coherence. This is a well-known sweet spot for formal verification, however what it means and entails is widely misunderstood. His talk will cover history, and discuss actual requirements and practical options for verifying memory consistency with your favorite model checker.
11:45 AM Arrival and Networking
12:00 PM Welcome and Lunch
12:45 PM Formal Sign-off with End-to-End Checkers
Vigyan Singhal, CEO, Oski Technology
1:30 PM Experience with Formally Verifying the Denver CPU
Syed Suhaib, CPU and Tegra Formal Verification Team Manager, NVIDIA
2:10 PM Coffee Break
2:15 PM Formal Verification of Cache Coherence
Robert Kurshan, a pioneer in formal verification
3:15 PM Wrap-up and Prize Drawing
3:30 PM Computer History Museum Tour (Self-Guided)
Robert Kurshan was a fellow at Cadence from 2001 until his retirement this month. Before that, he was a Distinguished Member of Technical Staff at Bell Labs after receiving his Ph.D in mathematics in 1968, from the University of Washington. Bob is an author of over 80 technical publications, holds 27 patents in communications, digital filtering and verification, and is the author of the book “Computer-Aided Verification of Coordinating Processes (COSPAN)”, which was the basis of the birth of formal verification research in UC Berkeley in 1992. In 2005, Bob won the ACM Kanellakis Theory and Practice Award for his work in automata-theoretic verification. He began working in formal verification since 1983. COSPAN has been applied directly to a number of projects inside AT&T, Lucent, NCR, Intel, and Cadence. FormalCheck, a formal verification tool from Bell Labs/Cadence, which used COSPAN as the engine, won the Innovation of the Year Award from EDN in 1998. Currently, COSPAN is utilized by Cadence for commercial hardware verification in its formal products and for constraint-solving in its simulator products.
Syed Suhaib is the CPU and Tegra Formal Verification Team Manager at NVIDIA. He drives the formal verification effort across various projects for next-generation designs, starting from test plan development, to application of various formal verification technologies. He is also involved with development of efficient methodologies and frameworks that are most effective for verification. Syed has a Ph.D in formal methods and modeling of communication protocols for intellectual property composition from Virginia Tech.
Vigyan Singhal is responsible for overall leadership of Oski Technology. He has worked in the semiconductor and EDA industries for more than 20 years, having founded two venture-funded start-ups – Jasper (acquired by Cadence) and Elastix (acquired by eSilicon). Vigyan started his career as a Research Scientist at Cadence Berkeley Labs. He has authored more than 70 publications, of which 3 won best paper awards. Vigyan has a PhD in EECS from the University of California at Berkeley where he was a Regents Scholar, and has a BTech in Computer Science from IIT Kanpur where he graduated at the top of his class.