InFormal Chat

 

World Cup Champion and Formal Verification at DAC 2018

What an exciting World Cup 2018! The whole world was glued to the television. People were rooting for their favorite teams and in awe of the skills demonstrated by many players. The spirit of World Cup reminds of this year’s DAC event, just a few weeks ago.

This year DAC seemed different than previous years, with a lot more papers on Formal verification. I attended only the Wednesday sessions, which had several sessions dedicated to Formal:  Novel Applications of Formal Verification; New Directions in Simulation and Formal, as well as a session on Formal verification research topics.  In the sport of “verification” Formal verification is now a formidable team!

At the World Cup, so many talented teams competed fiercely to be the champion and viewers anxiously waited to see which team would get to be crowned the champion. Did the team you were rooting for win?

At DAC, so many talented engineers submitted and presented their work and novel ideas to the attendees, hoping fellow engineers can learn and benefit from their experience. At the end of the conference, the coveted honor of the Best Presentation Award for front end verification went to a winner on Formal verification:

Convergence Techniques for C vs RTL Equivalence Checking by Xiushan Feng (AKA Shaun Feng), Li You, Rachna Nambiar Jain from Samsung Austin R&D Center and Yong Liu from Synopsys.

Shaun presented about how they used Synopsys Hector to exhaustively formally verify FPUs and encryption components in CPU designs, as well as filters or renders and instructions for shader core components in GPU designs. His presentation was technically rich: he covered different convergence techniques to work on the last 10% of difficult to converge Formal testbenches.

Shaun went on to describe each technique in detail and provided the rationale for why, when and how to use these techniques. For example:

In conclusion, Shaun summarized that using C as a reference to formally verify the RTL datapath is a powerful approach. The benefits were outstanding:  They saved 5+ DV engineer in terms of resources by reducing simulation efforts, found many bugs in corner case scenarios, faster debug and turnaround time due to short and concise traces, which all led to high-level confidence in the verification environment and the design.

As a fellow Formal technologist, I always root for Formal verification.   I couldn’t be more excited at DAC this year.  Formal technology has shown once again that it is indeed a winner in the verification sport!

 

Share and Enjoy:
  • del.icio.us
  • Digg
  • Facebook
  • Google Bookmarks
  • LinkedIn
  • Twitter