Name:Dr. Ashish Darbari
Designation:Principal Hardware Design Engineer
Title:More is Less: Efficient Formal Modelling for Exhaustive Verification of Sequentially-Deep Designs

Abstract: The ability to shorten time-to-market cycle crucially rests upon verification which, by some industry estimates, occupies around 60-70% of the overall time. The complexity of modern-day chip design poses unique challenges for verification and the ability to do “efficient” verification depends upon “efficient” processes and verification methodology. To speed up the design activity of modern day SoC platforms and IP cores, Imagination Technologies relies heavily on building re-usable design blocks.  We have perfected an efficient verification methodology which applies the appropriate verification technology enablers such as simulation, formal and emulation at a suitable level of design abstraction to enable efficient bug hunting.

Even though the details of the methodology vary as we scale in abstraction levels across the spectrum from pure hardware verification to full system level verification, a key has been ‘verification re-use’. This talk presents our approach of verification re-use by demonstrating how building a single canonical formal verification scoreboard allows the verification of a large number of library components ranging from single clock based FIFOs to more complex multi-clock synchronizers.

For three decades the conventional use model for successful application of formal model checking, dictated using formal models with fewer state bits to cope with the state-space explosion problem.In this talk, we will show how using too few state bits in a formal model could be counter-productive and how by adding just the ‘right amount’ of state in the formal models can make intractable problems tractable. We will present comparisons of three different types of formal models that we used in-house for verification. The key to our methodology has been the judicious use of abstraction and invariants; and the benefit of having formally verified these library components is increased confidence in the component itself and reduced debugging time when the library component is used as a part of larger systems.

Biography: Dr. Ashish Darbari works at Imagination Technologies as a Principal Hardware Design Engineer where he is leading the efforts to consolidate and streamline the use of formal methods for design and verification across Imagination. He has published numerous papers in top international conferences such as DAC, DATE, FMCAD and Interactive Theorem Proving (ITP) and regularly contributes to peer reviews. Dr. Darbari graduated with a Bachelor’s in EEE from BIT Mesra India. After obtaining his Diplom Informatik and Masters from TU Dresden, he completed his DPhil. from the University of Oxford. Prior to joining Imagination, Dr. Darbari worked as an intern at Intel’s Strategic CAD Labs (USA), as a Post Doc at the University of Southampton, at ARM (Cambridge), and at General Motors, R&D (Bangalore).

Slides and recording unavailable at the request of the speaker