Verification is overdue for an image overhaul

Verification is overdue for an image overhaul

Formal verification is the key to 40 more years of chip design

BY HARRY FOSTER
Mentor Graphics
Wilsonville, OR
http://www.mentor.com

Formal verification, or specifically formal property checking, is one of those ideas in technology that, for many people, has never fully lived up to its promise. It’s easy to get a sense of the origin and growth of the specific term in the technical literature by simply doing a search through the IEEE Xplore database. What you will find is that the references to the term “formal verification,” which is the proof of properties on designs using logic rather than testing, dates back to the early 1980s.

In fact, let’s pick on the year 1982 from our database scan. This was the year that saw the introduction of the Commodore 64 personal computer and the Lotus 1-2-3 spreadsheet, as well as the emergence of a handful of academic papers that first used the term “formal verification.” Now although there were many researchers presenting their work on the body of knowledge that we understand as formal verification today, our database scan reveals that only one paper in 1982 used the term, and it appeared in the paper’s abstract section. This was a paper by Gregor V. Bochmann, published in the IEEE Transactions on Computers, which described his research on hardware specification with temporal logic. Bochmann wrote rather innocuously in his abstract that the technique “is also useful for finding design errors.”

Now let’s fast forward a decade later and conduct our same search scan for the phrase “formal verification.” You will find is that it appears in 83 papers. By 2009 the citation count climbs to more than 600, surely evidence that formal methodologies are on the cusp of widespread adoption, right?

If only it were that simple!

Those of us who spend time speaking with our colleagues about formal verification — I visited 10 cities across Europe and Israel this spring doing just that — know that there is a gut-level bias against the methodology. Here’s an exercise: stop for a moment and jot down the words that come to mind when you encounter the phrase “formal verification” in an article such as this one. With little imagination on my part I’ll safely assume that you scribbled words like “expensive,” “incomplete,” and “complicated” rather than “exhaustive,” “efficient,” “integral” and “complementary.”

Formal verification is long overdue for nothing less than an image overhaul. Unfortunately, this project is unlikely to attract the attention of high priced marketing wizards, who understandably find consumer brands and political campaigns more compelling than EDA. That leaves those of us who are technologists to tackle this one. Any volunteers? No? Then here goes (with tongue occasionally planted in cheek).

The future is formal

Any good campaign is built on a few bold messages and predictions about the future. This is tricky in technology, which is littered with daft, forward-looking statements by some of its best known leaders, most of whom laugh about it later. Asked in 2005 if he foresaw mass-market computing, Gordon Moore replied “I thought it would be about a screen that allowed a woman in the kitchen to store recipes.”

Of course, Intel’s co-founder is also the source of one of the most famously durable and transformative predictions in the history of technology, Moore’s Law. Thanks to continually shrinking feature sizes and increasing wafer diameter, it’s reasonable to assert that in 12 years, the most advanced chips will have 100 billion transistors, a tenfold increase over what defines the cutting edge today (see Fig. 1 ). As Mentor Graphics CEO, Wally Rhines pointed out earlier this year in a User2User conference in San Jose, 100 billion is also roughly the number of stars in the Milky Way Galaxy.

Fig. 1. The number of transistors per chip continues to grow, projected to reach 1 billion ASIC maximum functions per chip at production by 2022.

In his April 18 speech, Dr. Rhines went on to describe how a 10x increase in transistors will lead to a 1000x increase in verification vectors. This is an astonishing rate, and one that leads to my own prediction: formal methodologies will inevitably be an integral complement to simulation in any efficient verification effort. There is simply no other way to keep pace with what’s coming from the fabs.

Fig. 2. Verification falling further behind: need exponential growth in capabilities to keep up. A tenfold increase in the number of transistors requires a thousandfold increase in verification.

Like any good politician or marketer, I’ll now immediately qualify that predication and add that formal methodologies will not be useful solely to those companies — we can count them on one hand — on pace to build a 100-billion-transistor chip in the foreseeable future. Whether in politics or product marketing, the best campaigns have ideas that are relevant to wide audiences. For those of us stumping for formal verification, that means reaching even those small engineering teams working on SoC designs for modestly priced consumer products. It’s these teams, with design schedules measured in months rather than years, who for so long have been most skeptical of formal methodologies. However, three relatively recent developments should help to finally lay this skepticism to rest.

For starters, formal technology has improved considerably in recent years. Today’s tools have multiple specialized proof engines that work together to automatically partition and abstract a complex design for a simpler proof. Some of the best under-the-hood features are in the areas of clock domain checking, power verification, and reset verification. The tools may not be push-button simple yet, but they are sufficiently advanced to break the dependency on a resident formal expert. In the past, such experts had to manually complete proofs because of the limitations, now overcome, of the formal tools.

Next, standards now exist to express functional properties. This wasn’t the case even six years ago. Back then, each vendor of formal tools created their own proprietary languages, which hamstrung widespread adoption of the methodology. Today, we have the IEEE 1850 Property Specification Language (PSL) and the IEEE 1800 SystemVerilog standard, which together provide a common means for writing functional properties.

Perhaps more interesting is the ecosystem that’s emerging due to the adoption of these standards. For example, companies are delivering assertion-based IP built around these standards. And there are several startups developing new tools that automatically generate assertions. This activity is almost certainly the sign of increasing confidence by design teams, who know they can adopt a standard and then are able to choose from multiple tools.

Finally, formal methodologies are well suited to the problems faced even by those companies far down the semiconductor food chain, where the average selling prices of the chips hover in the low double digits (see Fig. 3 ). Many of these problems are related to integrating various functional blocks and third-party IP. Formal verification is well suited, for example, for verifying that various off-the-shelf IP is properly stitched together via a standard AXI or AHB interface. Another boon: if the design team is using assertion-based IP and then acquires the right formal tools, the proofs are straightforward and nearly fully automated.

Fig. 3. SOC embedded processor trends: The number of processors per SoC.

Quick, somebody call Time magazine

Here’s something that’s also straightforward and nearly fully automatic: technologists of all stripes blanch at anything resembling a marketing campaign. Indeed, this is what I’ve always liked best about engineer-to-engineer communication. Logical reasoning and hard facts tend to win out over appeals to emotion. Which isn’t to say that we don’t have strong opinions — and also a collective sense of humor.

Another technology milestone from 1982 was announced on the cover of Time , which that year scrapped its Man of the Year designation in favor of naming the computer as Machine of the Year. Time publisher John A. Meyers wrote, “Several human candidates might have represented 1982, but none symbolized the past year more richly, or will be viewed by history as more significant, than a machine: the computer.”

Maybe it’s time to start a campaign to give formal verification a similar accolade on the 40th anniversary of this Time issue. Yes, that’s a joke; I know it will never happen. But I also know that we will never achieve another several decades of increasingly complex, powerful, and inexpensive computer chips without continued advances in formal verification. ■