Today, dozens of IBM engineers can spec, design, verify and test a 10 million-gate ASIC in a year; but what happens when that becomes 100 million gates? 1 billion gates? Companies such as IBM simply won't lard on engineers to partition the design and verification tasks; that would destroy the profitability models the industry's been comfortable with for 40 years.

Instead, the semiconductor world will lean on a methodology that, while not new, promises to erase many of the headaches and uncertainties posed by multimillion-gate designs. Indeed, it is rocket science.

Formal methods have been developed and studied for a generation (well, hundreds of years if you count advanced mathematical research). But only now are we seeing a confluence of commercial tool availability, acknowledgement of the method's validity and the hardware to power the tools. In fact, recent catastrophic failures of complex systems demand such a radical shift in design, proponents argue.

Take the 1996 Ariane 5 rocket explosion several years ago. A software bug in the inertial reference systems fouled the rocket's guidance system and caused a spectacular, multimillion-dollar crash. It was a bug that could not be found, even with a nation full of verification and test engineers working with enough workstations to fill Manhattan.

Take the Pentium floating-point-divide bug of 1994. That problem "galvanized verification efforts, not because it was the first or most serious bug in a processor design, but because it was easily repeatable and because the cost was quantified [at over $400 million]," wrote formal-method missionaries David Dill of Stanford and John Rusby of SRI International (Menlo Park, Calif.).

"These bugs are having a market impact," notes Patrick Lincoln, a formal guru at SRI. "Either they're resulting in dramatic failures or they're preventing people from adopting systems."

Patrick Lincoln's sail is set for verification and validation shores at SRI, as he helps implement formal methods in tools and design flows.

SRI is one of a handful of outfits considered at the forefront of transforming formal methods in either commercial tools or acceptable workflows in the design environment. Its resume so far is impressive. The research concern took on a paper published by Allied Signal regarding its Algorithm Z for the Boeing 777.

"They published a paper that included a proof that [Algorithm Z] was correct and would tolerate a certain number of faults," Lincoln said. "With our tools, we found the proof was flawed and the algorithm did not satisfy what they claimed-and it could make [a] plane crash. Z is reasonable for other reasons, but their claims were false."

In another challenge, Rockwell gave SRI a version of its M5 processor design to test formal methodology, inserting bugs here and there to challenge SRI. "They didn't have much faith in formal methods," Lincoln said. "We found the bugs they planted, found bugs they [Rockwell] had found earlier and found other aspects of their chip design that were problematic. It showed them that our approach could be used before fabrication."

The approach puts far more leverage in the hands of design engineers than ever before. While contemporary engineers have the ability to verify certain portions of designs early in the process, formal methodology lets one verify a much larger picture of the design.

In aerodynamics, for example, engineers run designs through Navier-Stokes models to figure out whether the bird will fly. "Why aren't we doing the same thing for digital hardware and software artifacts?" Lincoln asked. "The complexity [in ICs] is so much greater. That's what we're trying to produce here . . . test and analysis at design time."

It's clear that formal methods have applicability in aircraft design not simply because those designs are so complex but because the cost of failure is enormous-often meaning the financial solvency of an airline whose plane crashes. But what about a toaster? The answer isn't as simple as it might appear.

"The cost of the failure of the control system isn't great," Lincoln said. "It'll turn itself off every 13th time. Nobody's going to get sued over that, so today the tools are probably not cost-effective. But more and more an embedded software bug could mess up the stove, cause a fire, and somebody could get sued. It starts to have an impact."

Added Stanford's Dill, "The decision to use a new methodology is driven by economics: Do the benefits of the new method exceed the costs of converting to it and using it by a sufficient margin to justify the risks of doing so? Formal hardware verification has become attractive because it has focused on reducing the cost and time required for validation rather than pursuit of perfection."

A lingering question, of course, is, When do the tools become cost-effective?

SRI and others are working to bring down the cost. SRI in particularly has a "dial-down" feature on its software that allows an engineer to use formal "lite," if you will, in certain instances, according to Lincoln.

At the academic level, change has to be in the wind. "A lot needs to occur in the college curriculum. You need to understand the math you need here. Engineers need to look at finite-element analysis. We need to teach EEs about logic, what these things can and can't prove."

"We're not attempting to replace humans here. Instead, we're putting formal tools in [the] hands of engineers."

BACK TO THE FUTURE