InFormal Chat


VC Formal SIG 2019: If You Want Formal – You Got It!

First there was Woodstock. Then came Glastonbury and Coachella. But no event in the festival calendar is perhaps so revered as the annual VC Formal SIG (Special Interest Group) event in Silicon Valley. Ok, maybe that’s a little over the top, but it was a great event. The day was chock full of headline acts each with their own unique spin on this once underground genre that has skyrocketed its way to the mainstream – formal verification.

Synopsys gave a medley of tutorials ranging from a keynote by the legendary double act of Manish Pandey and Pratik Mahajan through talks from our Synopsys specialists on security verification and functional safety. Finally there was a presentation on formal signoff techniques by yours truly.

Vijay Kadamby & Anil Raj Gopalakrishnan from old school rockers Microsoft shook the SIG audience with their efficient verification of an interrupt controller. They looked at their previous approach which generated more than 2 million assertions and decided that a new methodology was needed. By looking for symmetry in the design and using symbolic variables they were able to converge on a previously inconclusive problem and prove something which once took two days in 15 minutes – now that’s what I call upping the tempo!

Always ready to put on a show, Nvidia’s Syed Suhaib broke out into the world of machine learning application. They found that in the increasingly complex designs they are verifying, they require more sub-proofs to be able to converge on large state machines. Clever stuff. However, these individual properties lead to more resource competition and they wanted to be able to speed things up. By adopting VC Formal’s RMA capability, they were able to apply machine learning in their regressions and significantly speed up their runtimes.

Performing a little Texas shuffle on our notions of what equivalence checking means, Shaun Feng from Samsung Austin discussed new applications of VC Formal SEQ. Showing while clock gating is still an important use case, additional bugs in areas such as RTL feature changing, optimizations and pipeline changes can all be caught using SEQ. Not only that, but these issues are being uncovered in large numbers by new hires and interns.

Finally, in the style of an experimental concept album that becomes number 1, Marvell’s Saurabh Shrivastava showed us how anyone can cross the bridge from control path to datapath validation. With the integration of HECTOR technology into VC Formal DPV App, and increased amounts of datapath arithmetic in designs, more and more users are trying their hand at some DPV. This involves proving transactional level equivalence between a C model and RTL implementation of functions. In their talk Marvell wowed the audience by showing how they used the technology to verify floating point arithmetic blocks.

All in all it was a spectacular day, and one which I’m sure will be talked about until next year’s event. More details on the 2019 Bay Area SIG can be found in this fantastic write up by Bernard Murphy for SemiWiki and in closing, all that’s left to say is: For those about to Formal – We salute you!



Share and Enjoy:
  • Digg
  • Facebook
  • Google Bookmarks
  • LinkedIn
  • Twitter