Dr. Surinder Sood (ARM)

The rising complexity of digital designs causes a bottleneck in the formal verification process. When the formal assertions have lesser bounds and do not converge, the problem becomes more apparent. This makes it challenging to complete verification sign-off based solely on formal verification of the relevant design. We have devised a method that improves the proof bound of a given property and works well for identifying corner case bugs in the design. This method is predicated on the refinement idea, which is most frequently applied in contract based verification. We apply the proof by decomposition approach to a target property, using which we find refinement properties in our proposed methodology. Later on, we compose the refinement properties so that they aid the target property to converge.

Key Points:

• Formal verification contracts
• convergence
• SMT solving

Surinder sood holds Phd in design verification and validation of hybrid systems from The University of Auckland, New Zealand. He has an overall experience of 20 years. Most of the time he has spent in verification of hardware components to system on chips. He has worked on different verification techniques while verifying such designs. His research interests include formal verification of digital and hybrid systems. He has also done work in security vulnerability verification of digital hardware, and also performance estimation of SOCs while doing SOC verification. He has worked with many prestigious organizations like Intel, AMD, Samsung electronics, ST Microelectronics and SanDisk. Currently he is working for ARM as a principal engineer and is a Senior member of IEEE-Circuit and Systems Society.