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.