About the Speaker

Kishan Pethani is the Formal Verification Lead for the Zen6 CPU program at AMD. With over a decade of industry experience spanning IP and SoC verification, his work focuses on the applied research of model-checking techniques for high-risk design areas and formal sign-off. At AMD, Kishan has developed formal verification solutions exclusively tailored to x86 microarchitecture, empowering engineering teams to adopt formal methods in their day-to-day workflows. He is currently scaling formal verification adoption across numerous sub-unit teams globally, working in close collaboration with design, verification and EDA teams worldwide.

Formal Methods at the Silicon Frontier: Post-Silicon Debug Acceleration in Zen6

Overview

Post-silicon debug presents exceptional engineering challenges – from bug reproduction and bug-fix application to workaround testing and ensuring functional correctness – all under tight time constraints. In the Zen6 CPU program, we demonstrated practical application of advanced Formal techniques that significantly reduced bug reproduction time from weeks to days, empowered engineering teams to identify viable workarounds, and provided mathematical proof of functional correctness when those workarounds were applied. This presentation details Formal methods we employed, the challenges we encountered, and how this work enabled a meaningful shift-left in post-silicon debug – establishing Formal methods as a key strategy for addressing numerous silicon bugs.

Key Points

• Post-silicon debug is slow and exceptionally challenging – Bug reproduction and validation traditionally takes few weeks to months with significant efforts.
• How we applied model-checking techniques in the Zen6 CPU program to reproduce bugs and validate workarounds to ensure program is on schedule.
• This case-study prove how Formal methods, in collaboration with simulation and emulation, can provide significant shift-left during post-silicon debug phase.