Symbolic Model Checking

Formal verification means having a mathematical model of a system, a language for specifying desired properties of the system in a concise, comprehensible and unambiguous way, and a method of proof to verify that the specified properties are satisfied. When the method of proof is carried out substantially by machine, we speak of automatic verification. This book deals with methods of automatic verification as applied to computer hardware.

As mentioned in the introduction, a formal verification system has several basic elements. First, we require a model. A model is an imaginary universe, or more generally, a class of possible imaginary universes. To make our model meaningful, we require a theory that predicts some or all of the possible observations that might be made of the model. An observation generally takes the form of the truth or falsehood of a predicate, or statement about the model. Finally, to verify something meaningful about the model, we require a methodology for proving statements that are true in the theory.

In the previous chapter, we equated a CTL formula with the set of states in which the formula is true. We showed how the CTL operators can thus be characterized as fixed points of certain continuous functionals in the lattice of subsets, and how these fixed points can be computed iteratively. This provides us with a model checking algorithm for CTL, but requires us to build a finite Kripke model for our system and hence leads us to the state explosion problem. In this chapter, we will explore a method of model checking that avoids the state explosion problem in some cases by representing the Kripke model implicitly with a Boolean formula. This allows the CTL model checking algorithm to be implemented using well developed automatic techniques for manipulating Boolean formulas. Since the Kripke model is symbolically represented, there is no need to actually construct it as an explicit data structure. Hence, the state explosion problem can be avoided.

In order to apply symbolic model checking to real problems, we need expressive languages that we can use to describe our model at a suitably high level (eg., a gate level schematic is probably not a high enough level). For our purposes, this means the language must provide operations on suitable high level types (such as symbolic enumerated types), and must allow us to conveniently describe non-deterministic choices, so that we can describe high level protocols without being concerned with implementation details. The language must have a precise mathematical semantics that defines the translation from a program in the langauge to a form suitable for symbolic model checking (ie., a Boolean formula representing the transition relation). For reasons that will be clarified in chapter 7, the semantics should be syntax-directed (defining the meaning of a language construct in terms of the meanings of its syntactic parts), so that we may infer properties of a program from properties of its parts. Ideally, it should also be possible to translate at least a useful subset of the language (not including, for example, non-deterministic choice) into hardware descriptions suitable for synthesis into real hardware. Constructs should be provided to allow us to use most common styles of system design.

In this chapter, we look at an application of the SMV symbolic model checker to a cache consistency protocol developed at Encore Computer Corporation for their Gigamax distributed multiprocessor [MS91]. This protocol is of interest as a test case for automatic verification for two reasons. First, it is not a theoretical exercise, but a real design, which is driven by considerations of performance and economics, as well as the usual constraints of industrial design, such as compatibility with existing hardware and software. Second, this protocol is a good example of a system where random simulation methods are ineffective in finding all the design errors.

The Mu-Calculus [Par74] is a logic based on extremal fixed points that is strictly more expressive than CTL,¹ and can also express a variety of properties of transition systems, such as reachable state sets, state equivalence relations, and language containment between automata. A symbolic model checking algorithm for this logic allows all of these properties to be computed using OBDDs [BCM⁺90].

This chapter deals with the verification of systems that are generated out of similar or identical finite state components, using a simple rule. Systems of this type are commonplace — they occur in bus protocols and network protocols, I/O channels, and many other structures that are designed to be extensible by adding similar components. In particular, we are interested in verifying properties that hold independent of the number of components in the system. We may for example have used a model checker to verify some property of a multiprocessor with a fixed number of processors. Would that property continue to hold if we added one more processor. One hundred? One thousand? Clearly, at some point we will be unable to answer the question with the model checker alone. It would be far preferable to settle the question once and for all, regardless of the number of processors.

This chapter deals with the question of how independence of events in concurrent systems contributes to the state explosion problem, and how a partially ordered representation can avoid this problem.

What we have seen in the preceding chapters is that Ordered Binary Decision Diagrams can be used as a representation in a wide variety of automatic verification algorithms, in order to cope with the state explosion problem. This can be done in a unified way by representing the algorithms in the Mu-Calculus fixed point notation. For fairly diverse families of regularly structured systems, the CTL model checking algorithm was observed to run in time and space which increased polynomially in the size of the system, while the number of reachable states increased exponentially. These results bear out a theoretical result bounding the OBDD representation of the transition relation for such systems. Standard automatic verification algorithms would be unsuitable for these examples because their complexity is proportional to the number of reachable states.