In particular, the notorious FDIV bug in the Intel Pentium processor, has 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).
Hence, hardware design companies are increasingly looking to new techniques, including formal verification, to supplement and sometimes replace conventional validation methods. Indeed, many companies, including industry leaders such as AT&T, Cadence, Hewlett-Packard, IBM, Intel, LSI Logic, Motorola, Rockwell, Texas Instruments, and Silicon Graphics have created formal verification groups to help with ongoing designs. In many cases, these groups began by demonstrating the effectiveness of formal verification by finding subtle design errors that were overlooked by months of simulation.
Why have formal methods been more successful for hardware than for software? We believe that the overriding reason is that applications of formal methods to hardware have become cost-effective.
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? The benefits may include an improved product (e.g., fewer errors), but those most keenly desired are reduced validation costs and reduced time-to-market (for the same product quality). The chief impediments to applying traditional formal methods are that the costs are thought to be high (e.g., large amounts of highly skilled labor) or even unacceptable (a potential increase in time-to-market), while the benefits are uncertain (a possible increase in product quality). Formal hardware verification has become attractive because it has focussed on reducing the cost and time required for validation rather than pursuit of perfection.
Of course, hardware has some intrinsic advantages over software as a target for formal methods. In general, hardware has no pointers, no potentially unbounded loops or recursion, and no dynamically created processes, so its verification problem is more tractable. Furthermore, hardware is based on a relatively small number of major design elements, so that investment in mastering the formal treatment of, say, pipelining or cache coherence can pay off over many applications. And the cost of fabricating hardware is much greater than software, so the financial incentive to reduce design errors is much greater.
However, we believe there are some lessons and principles from hardware verification that can be transferred to the software world. Some of these are listed below.
For hardware, a spectrum of tools has evolved to perform formal calculations at different levels of the design hierarchy and with different benefits and costs. At the lowest level are tools that check Boolean equivalence of combinational circuits (this is useful for checking manual circuit optimizations). Techniques based on Ordered Binary Decision Diagrams (BDDs) are able to check large circuits quite efficiently, and are now incorporated in commercial CAD tools. At a higher level, designs can often be represented as interacting finite state machines, and tools that systematically explore the combined state space can check that certain desired properties always hold, or that undesired circumstances never arise. Tools based on explicit state enumeration can explore many millions of states in a few hours; tools that represent the state space symbolically (using BDDs) can sometimes explore vast numbers of states (e.g., 10^100) in the same time, and can check richer properties (e.g., those that can be specified in a temporal logic, in which case the technique is called "temporal logic model checking"). At the highest levels, or when very complex properties or very large (or infinite) state spaces are involved, highly automated theorem proving methods can be used to compare implementations with specifications. These theorem proving methods include decision procedures for propositional calculus, equality, and linear arithmetic, combined with rewriting, and induction. In all cases, the tools concerned are highly engineered so that they can deal with very large formulas, and require little or no user interaction when applied in familiar domains.
Shortcuts can be taken when formal verification is used for finding bugs rather than proving correctness. For example, a system can be "down-scaled"--the number or sizes of components can be drastically reduced. For example, a directory-based cache-coherence protocol can be checked with just four processors, one cache line, and two data values--such a down-scaled description will still have many millions of states, but will be within reach of state exploration and model checking methods. These methods can check the reduced system COMPLETELY; in contrast, simulation checks the full system very incompletely. Both techniques find some bugs and miss others, but the formal methods often detect bugs that simulation does not. For example, cache-coherence bugs have been found in the IEEE standard FutureBus+ and Scalable Coherent Interface (SCI) protocols in just this way. Some researchers are now applying these techniques to software.
Of course, applying verification strategies to real problems is also crucial for building credibility. There is now a long string of success stories from academia and industry where finite-state verification techniques have been applied to hardware and protocols. A few documented examples include the protocol bugs mentioned above in FutureBus+ (found using symbolic model checking with a version of CMU's SMV system) and SCI (found using explicit state enumeration with Stanford's Murphi verifier), and formal verification of the microarchitecture and microcode of the Collins AAMP5 and AAMP-FV avionics processors (using theorem proving with SRI's PVS system). Several groups have also demonstrated the ability to detect bugs in the quotient-prediction tables of SRT division algorithms (similar to the Pentium FDIV bug), and some have been able to verify specific SRT circuits and tables. There have also been many unpublicized examples of problems found by industrial formal verification groups, which have helped them build credibility among designers and managers in their companies.