Automated Verification: Graphs, Logic, and Automata

1 Introduction

The recent growth in computer power and connectivity has changed the face of science and engineering, and is chang­ ing the way business is being conducted. This revolution is driven by the unrelenting advances in semiconductor man­ ufacturing technology. Nevertheless, the U.S. semiconductor community faces a serious challenge: chip designers are find­ ing it increasingly difficult to keep up with the advances in semiconductor manufacturing. As a result, they are unable to exploit the enormous capacity that this technology provides. The International Technology Roadmap for Semiconductors suggests that the semiconductor industry will require produc­ tivity gains greater than the historical 20% per-year to keep up with the increasing complexity of semiconductor designs. This is referred to as the "design productivity crisis". As designs grow more complex, it becomes easier to introduce flaws into the design. Thus, designers use various validation techniques to verify the correctness of the design. Unfortu­ nately, these techniques themselves grow more expensive and difficult with design complexity. As the validation process has begun to consume more than half the project design r~­ sources, the semiconductor industry has begun to refer to th1s problem as the "validation crisis".

Formal verification is a process in which mathematical techniques are used to guarantee the correctness of a de­ sign with respect to some specified behavior. Automated formal-verification tools, based on model-checking technol­ ogy [Clarke et a!., 1986; Lichtenstein and Pnueli, 1985; Queille and Sifakis, 1981; Vardi and Wolper, 1986] have en­ joyed a substantial and growing use over the last few years, showing an ability to discover subtle flaws that result from ex­ tremely improbable events [Clarke eta!., 1999] . While until recently these tools were viewed as of academic interest only, they are now routinely used in industrial applications, result­ ing in decreased time to market and increased product in­ tegrity [Kurshan, 1997]. It is fair to say that automated venfi­ cation is one of the most successful applications of automated reasoning in computer science [Clarke and Wing, 1996].

*Supported in part by NSF grants CCR-9988322, CCR-0 124077, IIS-9908435, IIS-9978135, and EIA-0086264, by BSF grant 9800096, and by a grant from the Intel Corporation.

2 Basic Theory

The first step in formal verification is to come up with afar­ mal specification of the design, consisting of a description of the desired behavior. One of the more widely used specifica­ tion languages for designs is temporal logic [Pnueli, 1977]. In linear temporal logics, time is treated as if each moment in time has a unique possible future. Thus, linear temporal formulas are interpreted over linear sequences, and we regard them as describing the behavior of a single computation of a system. (An alternative approach is to use branching time. For a discussion of linear vs. branching time, see [Vardi , 200 1].)

In the linear temporal logic LTL, formulas are constructed from a set Prop of atomic propositions using the usual Boolean connectives as well as the unary temporal connec­ tive X ("next"), F ("eventually"), G ("always"), and the bi­ nary temporal connective U ("until"). For example, the LTL formula G(request -+ F grant), which refers to the atomic propositions request and grant, is true in a computation pre­ cisely when every state in the computation in which request holds is followed by some state in the future in which grant holds. The LTL formula G(request-+ (request U grant)) is true in a computation precisely if, whenever request holds in a state of the computation, it holds until a state in which grant holds is reached.

LTL is interpreted over computations, which can be viewed as infinite sequences of truth assignments to the atomic propositions; i.e., a computation is a function 1r : IN ---> 2Prop that assigns truth values to the elements of Prop at each time instant (natural number). For a computation 1r and a point i E IN, the notation 1r, i I= tp indicates that a formula

<p holds at the point i of the computation 1r. For example, 1r,i I= X <p iff1r,i + 1 I= <p, and and 1r,i I= <pU1/J iff for some j ~ i, we have 1r,j I= 1/J and for all k, i :::; k < j, we have 1r, k I= <p. We say that 1r satisfies a formula <p, denoted 1r I= <p, iff 1r, 0 I= <p. The connectives F and G can be defined in terms ofthe connective U: F<p is defined as true U<p, and G<p is defined as ·F·<p.

Designs can be described in a variety of formal description formali sms. Regardless of the formalism used, a finite-state design can be abstractly viewed as a labeled transition sys­ tem, i.e., as a structure of the form M = (W W,0 R V) ' ' ' ' where W is the finite set of states that the system can be in, Wo ~ W is the set of initial states of the system, R ~ W 2 is a transition relation that indicates the allowable state transi­ tions of the system, and V : W ---> 2 JJrop assigns truth values to the atomic propositions in each state of the system. (A la­ beled transition system is essentially a Kripke structure.) A path in M that starts at u is a possible infinite behavior of the system starting at u, i.e., it is an infinite sequence u0 , u1 ... of states in W such that uo = u, and u; R u;+1 for all i ~ O.The sequence V ( uo), V ( u1) . .. is a computation of M that starts at u. It is the sequence of truth assignments visited by the path, The language of M, denoted L(M) consists of all com­ putations of M that start at a state in W0 . Note that L(M) can be viewed as a language of infinite words over the alphabet 2Prop. L(M) can be viewed as an abstract description of a system, describing all possible "traces". We say that M satis­ fies an LTL formula <p if all computations in L(M) satisfy <p, that is, if L( M) ~ models( <p) . When M satisfies <p we also ~ay that M is a model of <p, which explain why the technique IS known as model checking [Clarke eta!., 1999].

One of the major approaches to automated verification is the automata-theoretic approach, which underlies many model checkers, e.g. , SPIN [Holzmann, 1997]. The key idea underlying the automata-theoretic approach is that, given an LTL formula <p, it is possible to construct a finite-state au­ tomaton Acp on infinite words that accepts precisely all com­ putations that satisfy <p. The type of finite automata on infinite words we consider is the one defined by Biichi 1962. A Biichi automaton is a tuple A = (I: , S, S0 , p, F), where I: is a finite alphabet, S is a finite set of states, S0 ~ S is a set of initial states, p : S x I: ---> 2 8 is a nondeterministic transition func­ tion, and F ~ S is a set of accepting states. A run of A over an infinite word w = a1a2 · · ·,is a sequence s0s1 ···,where so E So and s; E p(s;-I, a;) for all i ~ 1. A run s0 , s1 , ... is accepting if there is some accepting state that repeats in­ finitely often, i.e., for some s E F there are infinitely many i's such that s; = s. The infinite word w is accepted by A if there is an accepting run of A over w. The language of infinite words accepted by A is denoted L(A) . The following fact establishes the correspondence between LTL and Biichi automata [Vardi and Wolper, 1994] (for a tutorial introduction for this correspondence, see [Vardi, 1996]):

Theorem 1 Given an LTL formula <p, one can build a Biichi automaton Acp = (I:, S, So, p,, F) , where I: = 2 Prop and lSI :::; 2°CI'f'll, such that L(Acp) is exactly the set of computa­ tions satisfying the formula <p.

This correspondence reduces the verification problem to an automata-theoretic problem as follows [Vardi and Wolper, 1986]. Suppose that we are given a system !VI and an LTL formula <p. We check whether L( M) ~ models( <p) as fol­ lows : (I) construct the automaton A~cp that corresponds to the negation of the formula <p, (2) take the cross product of the system M and the automaton A~cp to obtain an automaton AM,cp, such that L(AM,cp) = L(M) n L(A~cp), and (3) check whether the language L(AM, cp) is nonempty, i.e., whether AM,cp accepts some input.

Theorem 2 Let M be a labeled transition system and <p be an LTLformula. Then M satisfies <p iff L(AM,cp) = 0.

If L(AM,cp) is empty, then the design is correct. Otherwise, ~he d~sign is incorrect and the word accepted by L(AM,cp) IS an mcorrect computation. Model-checking tools use algo­ rithms for checking emptiness of Biichi automata [Emerson and Lei , 1985; Courcoubetis eta!., 1992] to check emptiness of L(AM,cp ). In case ofnonemptiness, the incorrect computa­ tion is presented to the user as a finite trace, possibly followed by a cycle. Thus, once the automaton A~cp is constructed, the verification task is reduced to automata-theoretic problems, namely, intersecting automata and testing emptiness of au­ tomata, which have highly efficient solutions [Vardi , 1996]. Furthermore, using data structures that enable compact repre­ sentation of very large state space makes it possible to verify designs of significant complexity [Burch eta!. , 1992].

The linear-time framework is not limited to using LTL as a specification language. ForSpec is a recent extension of LTL, designed to address the need of the semiconductor in­ dustry [Armoni et a!., 2002]. There are those who prefer to use automata on infinite words as a specification formal­ ism [Vardi and Wolper, 1994]; in fact, this is the approach of COSPAN [Kurshan, 1994]. In this approach, we are given a design represented as a finite transition system Manda prop­ erty represented by a Biichi (or a related variant) automaton P. The design is correct if all computations in L(M) are ac­ cepted by P, i.e., L(M) ~ L(P) . This approach is called the language-containment approach. To verify M with respect to P, we: (I) construct the automaton p c that complements P, (2) take the product of the system M and the automaton p c to obtain an automaton AM,P, and (3) check that the automa­ ton AM,P is nonempty. As before, the design is correct iff AM,P is empty. Thus, the verification task is again reduced to automata-theoretic problems, namely intersecting and com­ plementing automata and testing emptiness of automata.

3 Concluding Remarks

Over the last few years, automated formal verification tool s, such as model checkers, have shown their ability to provide a thorough analysis of reasonably complex designs [Goer­ ing, 1997]. Companies such as AT&T Cadence Fujitsu HP IBM, Intel, Motorola, NEC, SGI, Sie~ens, and Sun are ~sin~ model checkers increasingly on their own designs to reduce time to market and ensure product quality, cf. [Beer et a!. , 1994].

There has recently also been an fruitful interaction between model checking and planning in AI. On one hand, the usage of satisfiability technology to solve planning problems [Kautz and Selman, 1992] has been adopted into model checking

[Biere et al., 1999; Copty et al., 2001]. At the same time, symbolic techniques from model checking have been adopted into A1 planning [Cimatti and Roveri, 2000]. Finally, tempo­ ral logic and the automata-theoretic perspective has shown to be useful for planning with temporally extended goals [Bac­ chus and Kabanza, 1998; 2000; Giacomo and Vardi, 1999; Calvanese et al., 2002].