At first blush, the 2009 EE Times Global Salary & Opinion Survey seems like yet another confirmation of the appalling reputation of formal verification. The math-focused methodology is at or near the bottom of the survey's lists of “most interesting” and “most promising” technologies. But as I see it, the survey data also contains more than a few seeds of good news for the few of us out there who care more about algorithms and proofs than applications and processors.
One benefit of my job as Mentor Graphics’ chief verification scientist is that I get to spend lots of time on the road talking to engineers. Though, unless I'm in the company of other verification-obsessed colleagues, I often feel like something of an unwanted party crasher. Invariably, when I first enthuse about mathematical proofs of algorithms I start to notice people averting their eyes and shuffling their feet uncomfortably.
Yet, in my recent travels, I've also noticed that any initial reticence about the methodology quickly gives way to real interest in how to best apply it. This spring, I spent several weeks in Europe giving a series of seminars on assertion-based verification , one lynchpin of formal verification.
The 10-city tour included stops in Herzliya, Israel and Oulu, Finland. The rooms generally were full and the discussions were animated. While I joke that the audiences were drawn to my glib wit and good looks, in fact, they came because engineers everywhere grok that three inexorable trends are pushing formal verification to the fore: the technology and tools have matured remarkably (see here ); standards such as IEEE 1800 (see here ) and IEEE 1850 (see here ) now exist to express functional properties; and most importantly, an increasing use of SoCs and reusable IP presents no shortage of problems best addressed by formal proofs. I say more about each of these trends in an article I wrote for the DAC Knowledge Center in advance of the conference, held June 13-18 in Anaheim (see here ).
Granted, I live and breathe verification methodologies in general, and I am particularly fond of formal verification. And the old saw does hold true: when you have a hammer, everything looks like a nail, or in my case, like an opportunity for model checking or mathematical reasoning. Still, on second glance at the survey, I see lots of reason for optimism.
Formal verification is second only to Linux on the list of technologies in which those surveyed expect to be involved in the near future, especially in China and India. That's no surprise when you consider the kinds of products being built by these two giants on the world stage. China and India dominate when it comes to designing and building consumer electronics, arguably the most dynamic tech sector. More than one third of Chinese engineers and one in five Indian engineers work on consumer electronics, according to the survey. Among engineers in North America, Europe, and Japan, just 7 percent, 8 percent, and 13 percent work in this sector, which includes high-end cameras, cell phones, tablets, and nearly every other IC-based device that generates media buzz, and more importantly, market growth. As just one example, Semico Research Corp. predicts the worldwide market for high-end cell phones will grow by 13 percent from 2009 to 2013 while the markets for desktop PCs and workstations will shrink.
As is true of most devices with ICs, consumer electronics are also marked by an increasing reliance on SoCs and off-the-shelf IP, precisely the sorts of building-block technologies that lend themselves to formal proofs. For example, formal verification is perfect for verifying the various BUS interfaces that stitch together third-party IP blocks and produce functionality. And if you use assertion-based IP, you don't even have to possess moderate expertise in writing assertions. With the right tool the formal verification process can be push-button simple.
I often wish I could push a button and change the popularity of using formal property checking. But for the time being, I accept that it's in the same category as eating more vegetables and exercising regularly. That is, everyone agrees it's important, though many find it difficult to fully commit to it.
Then again, given the right incentives, people do change. When it comes to diet and exercise, the promise of health benefits years hence may be too abstract to produce a shift in behavior. But if you sign up for a 10K race, or even just schedule a summer beach vacation that you know will involve lots of time strolling in your bathing suit, that may be all the motivation you need to regularly rouse yourself for early morning workouts.
As it happens, the EE Times survey shows the beginnings of a similar near-term incentive when it comes to formal verification. Engineers in China and India, who lead the world in use of formal verification and development of consumer electronics, also stand head and shoulders above their global colleagues when it comes to salary increases. According to the survey, 45 percent of Chinese engineers and 40 percent of Indian engineers had annual salary increases that were “more” or “much more” than their raises five years ago. Far fewer North American (25 percent) and European (34 percent) engineers could say the same thing. Ok, I know what you’re thinking. Mark Twain summed it up nicely when he said, “There are three kinds of lies: lies, damn lies, and statistics.” But it is still nice to dream of the possibilities…
So what do I say to those who avert their eyes and shuffle their feet when the topic of formal verification comes up? How about this: embrace formal property checking, get a bigger raise, buy that pricey gym membership, and get ready to look good on that long-delayed tropical vacation. Yes, that's a joke — and a laughable example of logical reasoning and inference for anyone who is even half serious about model checking and proofs. But am I serious when I say that no matter what any survey says, formal verification is in fact among the most interesting and promising engineering topics today and in the near future.
About the author:
Harry Foster is chief verification scientist for Mentor Graphics' Design Verification Technology Division.
Foster currently serves as chair of the Accellera Formal Verification Technical Committee, and chair of the IEEE 1850 Property Specification Language (PSL) working group. He holds multiple patents in functional verification, and has co-authored six books on verification. He is also the original creator of the Accellera Open Verification Library (OVL) assertion monitor standard, and was the 2006 recipient of the Accellera Technical Excellence Award for his contributions to industry standards.