Formal verification grows, evolves as design technique

Electronic News, Jan 13, 1997 by Gary De Palma

Three years ago, very few people in the electronics industry had heard of formal verification techniques. Today, one type of formal verification is in the market and selling well, another is premiering, and the market is buzzing about the technology's potential. In such an environment, it has become more important than ever to understand how this rising technology will be used, and how that use might change as we approach the 21st century.

Current Trends

There are two types of formal verification on the market today: equivalence checkers and model checkers. Equivalence checkers compare a later design iteration to an earlier version to confirm functional equivalence, thus ensuring that no new errors have been introduced into a design. Model checkers, on the other hand, prove that a high-level design model, such as an RTL model, behaves as described in the specification under all circumstances. Most importantly, neither requires the blizzard of test vectors normally used for verification, and so can ensure a certain level of accuracy in much less time.

Only a small percentage of designers currently use equivalence checkers. Sales growth is so strong, however, that it is clear the tool is moving toward market acceptance. As this trend gains momentum, other companies will inevitably come in to supply the technology. There are currently three smaller companies with equivalence checkers on the market: Abstract Hardware, Chrysalis Symbolic Design and Compass Design Automation. But looming on the horizon are large CAD companies like Mentor Graphics and Synopsys, who have plans to break into the arena sometime in 1997.

Model checkers are at an earlier stage, but every indication is that their future is as bright. Recent advances have enabled these tools to verify larger portions of designs, making them much more practical. Giants like Texas Instruments, Motorola, Intel, Lucent Technologies and Silicon Graphics are already among the companies looking at incorporating the technology into their design flows. Current model checker suppliers include Abstract Hardware, Bell Labs Design Automation and IBM.

Future Trends

The idea that formal verification tools will be important in the future is nothing more than an extension of current trends. What is perhaps more interesting is to speculate how both the nature and the use of the tools will change over time. On this dimension, it seems reasonable to assume there will be four major changes.

First, formal verification tools will become easier to use. Currently, the tools are mostly powerful engines, and the results, while extremely valuable, often require the assistance of a formal verification expert to be interpreted. Formal verification companies, to their credit, have made enormous strides toward more usable tools. But there is still much to be done. Only after tools like model checkers are routinely used by the same people who use simulators will formal verification enter the mainstream of design.

Second, the use of the tools will change. Both equivalence checkers and model checkers are currently used as point tools to verify particular stages in the design flow. Three or four years down the road, formal verification will increasingly be used to enhance the flow itself. Users will develop behavioral models and refine them, and formal verification will verify that the new design is a valid refinement of the original. For example, a packet which is received as good or bad in behavior will be refined to include a CRC test to measure its validity. Users will be able to prove important behavior at the behavioral level and carry this proof through the design phases. For those who find value in the point tool approach, this new design paradigm will be difficult to resist.

Third, formal verification will start to be used outside the field of integrated circuits. Mechanical designers and software developers have already expressed great interest. In mechanical design, the handling characteristics of an automobile could be verified under a set of potentially infinite possible conditions, without as many gaps in the analysis. Software bugs, for their part, cost the computer industry far more each year than their hardware counterparts. A more systematic formal approach could dramatically reduce the number of bugs in code.

Finally, the next few years will see the limited acceptance of theorem proving techniques in hardware design. Theorem proving is the most flexible of the formal verification tools, but also the most difficult to use. As its name would imply, it is capable of verifying whole theorems, confirming that a formal design specification is consistent with a specific design implementation. Theorem proving will first find acceptance in niches of the design community where it can be applied with high value and low effort, such as resource allocation in formally defined algorithms.

One way or another, formal verification is only just beginning as a design technique.