Get email delivery of the Cadence blog featured here
Exhaustive and comparatively efficient, formal verification is a powerful option to other verification methods because it can detect bugs much earlier in the design cycle. Anyone with a love for math, like John Havlicek, can understand the unique advantages of this methodology. Havlicek, who has a B.S. degree and a Ph.D. in mathematics, is a principal product validation engineer at Cadence who spends his days working on simulation-based and formal verification of DDR memory controller and PHY IP. He has played an essential role in popularizing formal verification, and is a co-author of SVA: The Power of Assertions in SystemVerilog. I talked with him recently about what led him on the formal path. Listen in.
How did you develop your interest in formal verification?
I started out trying to be a mathematician; however, it’s really tough to be an academic mathematician. Mathematics is an intellectual art. It’s like being a starving artist among many great artists.
I became attracted to formal methods while pursuing doctoral studies in computer sciences at the University of Texas at Austin. Formal methods are very mathematical – it was one aspect of computer science that really resonated with me. I learned about model checking and temporal logic for defining properties. Then I did an internship at Motorola, working in an internal tools group where we had an internal model checker, on-the-fly constraint solver, and assertion language. As the strategy changed from internal tools to purchasing EDA tools, my role shifted to advocating our assertion language for industry standards, working on methodologies, and assisting with deployment and liaison with vendors.
I joined Cadence in May 2012. We’re now using for our IP many of the assertion features that I helped to develop as industry standards.
What are the challenges of using formal analysis for DDR IP? And the advantages?
DDR IP is highly configurable. Unlike chip projects that have a life span—they tape out and you’re done—the IP is continuously being delivered to customers with various selections of features. The code base is managed with scripting layers—that’s a big challenge because the scripting layer is not anything formal analysis can consume. We can’t actually do formal analysis at the level of the code base of the IP. That’s a huge coverage problem.
What I’ve done is to analyze by hand the dependencies and actually find representatives of the distinct versions of the code for the block I’m looking at. There may be hundreds of delivery configurations, but my analysis based on the template variables may say there are half a dozen distinct versions of the block, so I run formal on these.
Formal analysis has the ability to stress behaviors of critical blocks much better than simulation can, especially when your simulations are run with larger models. We run simulations with the whole memory controller and PHY IP hooked up together, with various Denali memory models, and bus functional models. It’s a memory subsystem. If you’re trying to exercise corner cases in an arbiter, that’s a heavy simulation platform to try to do that. Formal extracts the block of interest and it can pound that block intensively.
You chaired the SystemVerilog Assertions Committee several years ago. What was that experience like?
After a few years of working in the SystemVerilog Assertions Committee, I developed a reputation for having a transparent agenda. I prioritized technical merit, listened to criticism, built consensus, and was very successful in getting proposals passed. That led to my election as chair. Chairing comes with the responsibility to manage meetings, track assignments, call votes, and report to the board. I served in that position for several years before passing on the torch.
What kinds of hurdles do engineers have to overcome in order to accept formal analysis? How did you help increase the popularity of formal analysis?
One of the biggest hurdles is in learning a new perspective in the way you think about your design and verification. With the old perspective, I’d put something together, run some vectors through it. I’d think about interference cases and run those. When you’re doing formal, you’re not thinking about driving particular vectors through. You need to think about all of the cases that need to be considered. Anything you do not forbid will be exercised.
Another hurdle is assertion literacy. You have to write down the expected correct behavior in a way that can be understood by the formal tool—in synthesizable RTL and assertions, not in an object-oriented programming language.
We wrote the SVA book to help with all these challenges.
If you were not an engineer, what would you be?
A mathematical scientist. I do thrive on having a sense that what I’m doing has a positive impact on other people. There is a lot of good that comes from giving something away (such as open standards). Working on SystemVerilog and SystemVerilog Assertions and succeeding in making it a good language that many engineers use is a positive reflection on the value of what I’ve been spending my time on.
When you're not verifying DDR IP, how do you like to spend your free time?
I love outdoor activities. Hiking and backpacking are longtime favorites, but recently I've been trying some new stuff, like skydiving, scuba diving, and open-water swimming (In the photo with this post, John is pictured at San Francisco's Aquatic Park, ready for a swim.)
Additional Formal Verification Posts
Tracking Progress on Formal Testbenches at ARM Austin
Imagination Dispels 10 Myths About Formal Verification
Broadcom Design and Verification Engineer: My First 100 Days in Formal Land