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 Fosteris 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.
I am one of those who are passionate about verification. I'm nearly always disappointed to see that the exciting new verification tools only work with 100% digital ICs.
I’ve always worked with mixed signal SOCs with digital circuitry in the analog feedback loop. Placing such digital circuitry in a black box with the analog circuitry allows one to use digital verification tools but leaves holes in the verification plan. Here are some mixed-signal building blocks with high-risk digital content. In particular, I’m talking about analog front-end sub-circuits with digital controls that are generated by signal processing the output of the A/D converter. For example:
* Automatic Gain Control
* Digital PLL (discrete incremental control over sampling frequency and phase)
* Adaptive Analog Filters
* Built-in Analog Self-Test
* Automatic Calibration and Offset Cancelation
A workaround is to create a "real" testbench to verify the mixed-signal SOC. In addition, create a "spoof" testbench which quarantines the mixed-signal content to make the SOC look like a 100% digital IC.
The real testbench includes assertions for verifying power-up sequencing, bias currents, reference voltages and the validity of digital controls. It also assigns variables such as gain, frequency, phase or other analog quantities versus time, for which assertions are written.
I haven't found a way to objectively measure and quantify the completeness of mixed-signal verification -- with or without assertions. I long for the day when verification tools are written to assist the mixed-signal verification engineer with the real SOC testbench.
I welcome further comments about mixed-signal verification. Has anyone found solutions to the problems I've described?
Contact me via my web page or LinkedIn profile if you have questions of your own, or need help with RF, Analog and mixed-signal SOC verification.
R. Peruzzi Consulting, Inc.
David Patterson, known for his pioneering research that led to RAID, clusters and more, is part of a team at UC Berkeley that recently made its RISC-V processor architecture an open source hardware offering. We talk with Patterson and one of his colleagues behind the effort about the opportunities they see, what new kinds of designs they hope to enable and what it means for today’s commercial processor giants such as Intel, ARM and Imagination Technologies.