DVCon China: Formal Technology Is Set for Growth in Asia
At the recent DVCon in Shanghai, China, my colleague Jin Hou delivered the tutorial “Back to Basics: Doing Formal the Right Way”. Jin is an expert in formal and CDC methodologies, and in her career she has trained hundreds of engineers how to get up to speed with formal, and leverage its strengths as part of a complete enterprise-class verification flow. I’ve been to DVCons in the US, EU, and India, so I was eager to hear her first-hand account of the latest incarnation of this successful conference series. Below is a review of her experience.
Joe: Tell me more about your tutorial
Jin: In recent years there has been a lot activity around automated formal apps. This is a good thing not only because they help any engineer take advantage of formal’s power, but their success has also inspired interest in property checking. Consequently, this tutorial was created to show engineers who are new to formal what is involved in the planning, setup, execution, and results analysis with formal property checking verification. Wherever it made sense, I would make analogies to testbench simulation flows to explain formal methodology, and show how formal and simulation can be used in combination.
——
Joe: Did you get to survey the attendees at all? If so, what were the results?
Jin: Yes, but first let me say the tutorial was standing room only – there were at least 40 people were in a room setup for half that number!
At the beginning I asked for a show of hands for the following questions:
“How many people are using formal now?” Only 3 people raised their hands.
“How many of you are thinking of using formal in 6 months?” Just 7 hands went up.
In my 1-on-1 discussions after the tutorial concluded, an attendee told me, “Assertions are still pretty new to Chinese engineers. Except for [a major semiconductor supplier], most customers don’t have any assertion and formal experts.” However, I also heard some great news on this point: a professor from an area university told me his department was starting a course on SystemVerilog – including writing SVA — this coming academic year!
In general, it was clear to me that there is a great opportunity for formal usage to grow in China!
—–
Joe: Were there any particular comments or questions from the attendees?
Jin: The overall theme of the Q&A I received was around the benefits that property checking provided over other verification techniques. Indeed, I was directly asked “Why do you need formal?” It’s a fair question – especially since property checking with hand-written assertions (vs. automated formal apps) does impose a learning curve on its users; and it is not always obvious what formal is capable of doing better than the alternatives.
Of course we setup the tutorial to address exactly these concerns; so over the course of the presentation I showed how the formal can address many serious verification tasks long before a simulation testbench would be available. For starters, hand-written assertions themselves help designers communicate their concerns to the verification team, bridging the gaps between them. With such an “executable specification” (which, by the way, with the right syntax can be easily reused in simulation and emulation), verification tasks that would take forever in simulation can be quickly solved by formal. Perhaps the most well received example of this was when I spoke of how formal can deliver exhaustive proofs of liveness and safety properties.
[Ed. Note: “Liveness” == something good must eventually occur. “Safety” == something bad must never occur, i.e., good behavior should be always true. A well regarded, in-depth review of these valuable formal analyses is available here https://www.doc.ic.ac.uk/~jnm/book/firstbook/pdf/ch7.pdf ]
In general, the fact that you can do such significant verification with exhaustive results, before you write a single line of testbench code, means that formal should be part of any serious verification project.
—–
Joe: Looking back on the experience, how has it inspired you?
Jin: It’s given me great ideas on how we can further enhance our Verification Academy courses to help new formal users to get up to speed with the key concepts and work flows. In particular, we need to better promote “formal coverage” – what it tells you, how it helps the formal engineer measure their personal progress, and how it feeds into the overall verification project status alongside simulation code and functional coverage reporting.
—–
Joe: Thanks, Jin! Final thoughts?
Jin: While I enjoy supporting customers here in the San Francisco Bay Area, I also look forward to introducing more engineers to formal verification across China!
—–
If you went to DVCon in Shanghai — or in San Jose – this spring, please share your experiences in the comments below.
Until DAC, may your power consumption be low and your coverage be high!
Joe Hupcey III
Reference links:
DVCon Shanghai 2017 proceedings — https://dvcon-china.org/dvcon-china-history-archive
Safety & Liveness Properties, Chapter 7, Concurrency: State Models & Java Programs, Jeff Magee and Jeff Kramer, https://www.doc.ic.ac.uk/~jnm/book/firstbook/pdf/ch7.pdf
Related Verification Academy courses:
Getting Started with Formal-Based Technology
https://verificationacademy.com/courses/Getting-Started-with-Formal-Based-Technology
Formal Assertion-Based Verification
https://verificationacademy.com/courses/Formal-Assertion-Based-Verification
Formal-Based Technology: Automatic Formal Solutions
https://verificationacademy.com/courses/Formal-Based-Technology-Automatic-Formal-Solutions
Assertion-Based Verification
https://verificationacademy.com/courses/assertion-based-verification
Comments