Skip to main content

RuleBase Parallel Edition

Formal Verification

Symbolic Model Checking wins the ACM Kanellakis Award for Theory and Practice (February 8, 1999)

The 1998 ACM Kanellakis Award for Theory and Practice was awarded to Randal E. Bryant, Edmund M. Clarke, Jr., E. Allen Emerson, and Kenneth L. McMillan for their invention of "symbolic model checking," a method of formally checking system designs that is widely used in the computer hardware industry and is beginning to show significant promise also in software verification and other areas.

Symbolic model checking has its roots in the earlier concept of temporal model checking, proposed by Clarke and Emerson in 1981. In temporal model checking, specifications are expressed in a logic called CTL (Computation Tree Logic), and system designs are modeled as finite state-transition systems. An efficient search procedure based on fixed-point computation is used to determine automatically if the specifications are satisfied by the state-transition systems. The model checker will either terminate with the answer True, indicating that the design indeed satisfies the specifications, or False, indicating that it does not. In the latter case, it typically produces an explicit counterexample, that is, the description of an execution of the system that violates the specification. Clarke and Emerson were able to use temporal model checking to find some very subtle design errors in published hardware designs.

There was a drawback to this approach as originally proposed, however: the state-explosion problem. For real-world designs, the state space of the design is typically so large that the required exhaustive search becomes infeasible. This limited the applicability of temporal model checking to designs of mainly academic interest.

In 1986, Bryant developed a new representation of Boolean functions, called OBDDs (Ordered Binary Decision Diagrams). Bryant's crucial contribution was to show that by fixing the order of testing of Boolean variables in binary decision diagrams, these diagrams become very tractable computationally. McMillan then realized that OBDDs can symbolically represent sets of states in state-transition systems. In 1987, he developed a software tool called SMV (Symbolic Model Verifier) for verifying systems with over 10^20 states. Thus, symbolic model checking was born.

The practicality of symbolic model checking as opposed to other formal verification techniques stems from several reasons. First, model checking is an algorithmic method, as opposed to other formal verification techniques that require extensive user guidance. Second, symbolic model checking can in many cases avoid the state-explosion problem and handle successfully industrial-size designs. Third, for systems that are too big even for symbolic model checking to handle completely, one can still use it to verify that specific types of unwanted behavior cannot occur. These advantages are responsible for the successful introduction of formal verification into the industrial design environment.

Today, symbolic model checking is one of the most important formal techniques used in the computer and semiconductor industries, and SMV is one of the most widely used verification tools. These industries face a complexity explosion of near-crisis proportions, with six-month design cycles in which products of unprecedented complexity have to be "right" the first time in order for companies to survive. Symbolic model checking offers design teams shorter time to market and increased product integrity, which explains the rapid adoption of this technology by all leading semiconductor companies.

Several companies have integrated symbolic model checking into proprietary design tools. For example, the RuleBase system developed at the IBM Haifa Research Lab is used in a number of microprocessor development projects to verify bus protocols and other system components. The model checker SVE developed at Siemens is applied to various internal development projects and is also marketed to external customers by Abstract Hardware Ltd. and Verisys. Motorola and Intel are two other semiconductor manufacturers that make extensive use of symbolic model checking. Other commercial tools based on symbolic model checking include Lucent's FormalCheck, marketed by Cadence for hardware verification.

Industrial experience has shown that symbolic model checking is able not only to find hard-to-discover design errors, but it can do so inexpensively. An example of this was demonstrated in the verification of a storage control unit at IBM. A recently discovered bug in an arbiter had not been found by millions and millions of simulation cycles over a period of months, but was found in a few minutes by RuleBase.

While general design verification problems are still daunting today, researchers inspired by the success of symbolic model checking in the hardware domain are developing new assaults on the problem of verifying software. Success has recently been reported in checking some crucial problems of large software systems, such as aircraft collision avoidance systems. Other application domains are also opening up. For instance, a chemical engineering researcher has found symbolic model checking applicable to risk-assessment problems in the chemical industry, thus demonstrating that symbolic model checking has a potential of becoming the standard technique of analyzing all sorts of large discrete-state systems.

For their invention of symbolic model checking, Bryant, Clarke, Emerson, and McMillan received the 1998 Kanellakis Award for Theory and Practice.