9512.net

甜梦文库

甜梦文库

当前位置：首页 >> >> # Software Tools for Technology Transfer manuscript No. (will be inserted by the editor) Cove

Software Tools for Technology Transfer manuscript No. (will be inserted by the editor)

Coverage Metrics for Formal Veri?cation

Hana Chockler?1 , Orna Kupferman??2 , Moshe Vardi???3

1 2 3

Northeastern University Hebrew University Rice University

The date of receipt and acceptance will be inserted by the editor

Abstract. In formal veri?cation, we verify that a system is correct with respect to a speci?cation. Even when the system is proven to be correct, there is still a question of how complete the speci?cation is, and whether it really covers all the behaviors of the system. The challenge of making the veri?cation process as exhaustive as possible is even more crucial in simulation-based veri?cation, where the infeasible task of checking all input sequences is replaced by checking a test suite consisting of a ?nite subset of them. It is very important to measure the exhaustiveness of the test suite, and indeed, there has been an extensive research in the simulation-based veri?cation community on coverage metrics, which provide such a measure. It turns out that no single measure can be absolute, leading to the development of numerous coverage metrics whose usage is determined by industrial veri?cation methodologies. On the other hand, prior research of coverage in formal veri?cation has focused solely on state-based coverage. In this paper we adapt the work done on coverage in simulation-based veri?cation to the formal-veri?cation setting in order to obtain new coverage metrics. Thus, for each of the metrics used in simulation-based veri?cation, we present a corresponding metric that is suitable for the setting of formal veri?cation, and describe an algorithmic way to check it.

1 Introduction Today’s rapid development of complex hardware designs requires reliable veri?cation methods. In formal veri?cation, we verify the correctness of a design with respect to a desired behavior by checking whether a labeled state-transition graph that models the design satis?es a speci?cation of this behavior, expressed in terms of a temporal logic formula or a ?nite automaton [CGP99]. Beyond being fully-automatic and reliable, an additional attraction of formal-veri?cation tools is their ability to accompany a negative answer to the correctness query by a counterexample to the satisfaction of the speci?cation in the design [CGMZ95]. On the other hand, when the answer to the correctness query is positive, most formal-veri?cation tools terminate with no further information to the user. Since a positive answer means that the design is correct with respect to the speci?cation, this seems like a reasonable policy. In the last few years, however, there has been growing awareness of the importance of suspecting the design of containing an error also in the case veri?cation succeeds. The main justi?cation for such suspicion are possible errors in the modeling of the design or of the behavior, and possible incompleteness in the speci?cation. Several sanity checks have been suggested for further assessment of the modeling of the design and the speci?cation [Kur97]. One direction is to detect vacuous satisfaction of the speci?cation [BBER01,KV03,PS02], where cases like antecedent failure [BB94] make parts of the speci?cation irrelevant to its satisfaction. For example, the speci?cation “every request is eventually granted” is vacuously satis?ed in a design in which no requests are sent. A similar direction is to check the validity of the speci?cation (a speci?cation is valid if it holds for all designs). Clearly, vacuity or validity of the speci?cation suggests some problem. It is less clear how to check completeness of the speci?cation. Indeed, it is only rarely that there is a priori complete speci?cation for the system under design (e.g., the IA-32 architecture). Typically, speci?cations are written manually, and their completeness

Key words: formal veri?cation – model checking – coverage metrics – algorithms

? Address: College of Computer and Information Science, Boston, MA 02115, U.S.A. Email: hanac@ccs.neu.edu. ?? Address: School of Engineering and Computer Science, Jerusalem 91904, Israel. Email: orna@cs.huji.ac.il. Supported in part by by NSF grant CCR-9988172. ??? Address: Department of Computer Science, Houston, TX 77251-1892, U.S.A. Email: vardi@cs.rice.edu. Supported in part by NSF grants CCR9988322, CCR-0124077, IIS-9908435, IIS-9978135, and EIA-0086264, by BSF grant 9800096, and by a grant from the Intel Corporation.

2

Hana Chockler et al.: Coverage Metrics for Formal Veri?cation

depends entirely on the competence of the person who writes in formal veri?cation have been helpful in detecting design them. The motivation for a completeness check is clear: an errors that escape the veri?cation process [BBER01,HKHZ99, erroneous behavior of the design can escape the veri?cation PS02]. The main lesson to be learned from several years of efforts if this behavior is not captured by the speci?cation. In research in coverage in simulation-based veri?cation [Pel01, fact, it is likely that a behavior not captured by the speci?caTK01] is that coverage is a heuristic that measures the extion also escapes the attention of the designer, who is often haustiveness of the veri?cation effort, but no single measure the one to provide the speci?cation. can be absolute. Consequently, research in simulation-based coverage has identi?ed numerous coverage metrics; their usThe challenge of making the veri?cation process as exage is determined by practical veri?cation methodologies. Prior haustive as possible is even more crucial in simulation-based research of coverage in formal veri?cation [HKHZ99,KGG99, veri?cation. Each input vector for the design induces a difCKV01,CKKV01,CK02] has focused solely on state-based ferent execution of it, and a design is correct if it behaves as coverage. In contrast, in simulation-based coverage one ?nds required for all possible input vectors. Checking all the exmany other coverage metrics, including several metrics of ecutions of a design is an infeasible task. Simulation-based code coverage, which measure that all syntactic aspects of the veri?cation is traditionally used in order to check the design design have been covered [Pel01,TK01]. Our goal in this pawith respect to some input vectors [BF00]. The vectors are per is to adapt the work done on coverage in simulation-based chosen so that the veri?cation would be as exhaustive as posveri?cation to the formal-veri?cation setting in order to obsible, but still, design errors may escape the veri?cation protain new coverage metrics. Thus, for each of the metrics used cess. Since simulation-based veri?cation is a heuristic that in simulation-based veri?cation, we present a corresponding replaces the infeasible task of checking all input vectors, it metric that is suitable for the setting of formal veri?cation. is very important to measure the exhaustiveness of the input In addition, we describe symbolic algorithms for computing sequences that are checked. Indeed, there has been an exteneach of the new metrics. sive research in the simulation-based veri?cation community on coverage metrics, which provide such a measure [TK01]. Coverage metrics are used in order to monitor progress of the The adoption of metrics from simulation-based veri?caveri?cation process, estimate whether more input sequences tion is not straightforward. To see this, consider for examare needed, and direct simulation towards unexplored areas ple code-based coverage and a check whether both branches of the design. Essentially, the metrics measure the part of the of an if statement have been executed during the simulation. design that has been activated by the input sequences. For exA straightforward adoption would check the satisfaction of ample, in code-based coverage metrics, the design is given the speci?cation in a mutant design, one for each branch, in as a program in some hardware description language (HDL), which the branch is disabled. Such a mutant design, howand one measures the number of code lines executed during ever, has less behaviors than the original design, and would the simulation. In Section 3, we survey the variety of metclearly satisfy all universal speci?cations (i.e., speci?cations rics that are used in simulation-based veri?cation (see also that apply to all behaviors, as in linear temporal logic or uni[ZHM97,Dil98,Pel01,TK01]). Coverage metrics today play versal branching temporal logic, in which the only allowed an important role in the design validation effort [Ver03]. path quanti?er is universal [GL94]) that are satis?ed by the Measuring the exhaustiveness of a speci?cation in formal original design. In general, the problem we are facing is the veri?cation (“do more properties need to be checked?”) has need to assess the role a behavior has played in the satisfaca similar ?avor as measuring the exhaustiveness of the intion of a universal speci?cation – one that is clearly satis?ed put sequences in simulation-based veri?cation (“are more sein the design obtained by removing this behavior. The way quences need to be checked?”). Nevertheless, while for simulation-we suggest to do so is to check whether the speci?cation is based veri?cation it is clear that coverage corresponds to acvacuously satis?ed in a mutant design in which this behavior tivation during the execution on the input sequence, it is less is disabled: a vacuous satisfaction of the speci?cation in such clear what coverage should correspond to in formal veri?caa design (we assume that the speci?cation is not vacuously tion, as in model checking all reachable parts of the design satis?ed in the original design) indicates that the speci?caare visited. Early work on coverage metrics in formal veri?tion does refer to this behavior; on the other hand, a noncation [HKHZ99,KGG99] suggested two directions. Both divacuous satisfaction of the speci?cation in the mutant design rections reason about a ?nite-state machine (FSM) that modindicates that the speci?cation does not refer to the missing els the design. The metric in [HKHZ99], later followed by behavior. Accordingly, some of the new metrics we suggest [CKV01,CKKV01,CK02], is based on mutations applied to reduce coverage to queries about vacuous satisfaction. On the the FSM. Essentially, a state s in the FSM is covered by other hand, a code-based metric that checks whether a particthe speci?cation if modifying the value of a variable in the ular assignment in the code has been executed may also be state renders the speci?cation untrue. The metric in [KGG99] reduced to a metric that checks the satisfaction of the speci?is based on a comparison between the FSM and a reduced cation in a mutant design in which the assignment is changed. tableau for the speci?cation. See [CKV01] for a discussion Accordingly, some of the metrics we suggest follow the apof pros and cons of this metric. proach in [HKHZ99] and reduce coverage to queries about Coming up with an exhaustive speci?cation is of great imsatisfaction of the speci?cation in mutant designs. Unlike preportance and challenge in formal veri?cation. Sanity checks vious work, however, the mutant designs we consider are not

Hana Chockler et al.: Coverage Metrics for Formal Veri?cation

3

arbitrary, and capture the different metrics of coverage used in simulation-based veri?cation. We describe symbolic algorithms for computing the new coverage metrics for speci?cations given by means of LTL formulas. We ?rst show that both vacuity and falsity coverage can be reduced to model checking of mutant speci?cations and/or mutant designs, and then show how symbolic model-checking algorithms can be extended to symbolically maintain mutants that correspond to uncovered parts of the system. We analyze the complexity of our algorithms in terms of the size of the ROBDDs used, and the number of symbolic operations required.

2 Preliminaries 2.1 Simulation-Based Veri?cation In simulation-based veri?cation, the implementation of a hardware design is executed in parallel with a reference model described at a different level of abstraction or with monitors and assertions that check for certain behavior of the implementation [KN96]. The execution is done with respect to a selected set of ?nite input sequences, referred to as tests. Thus, assuming the implementation has a set I of input signals, a test is a ?nite sequence t = i0 , i1 , . . . , in ∈ (2I )? of input assignments. Implementations of hardware designs can be described by different formalisms. We consider two formalisms with respect to which coverage metrics are naturally de?ned. The ?rst formalism is that of hardware description languages (HDL). A typical HDL program speci?es the input and output variables of the various modules of the design, and, using control and assignment statements, the interaction of the modules among themselves and with an environment that provides the input signals. Reasoning about rich HDL such as Verilog involves dif?cult technical details.1 We consider here the simpli?ed model of control ?ow graph (CFG). Each HDL statement corresponds to a control state and induces a node in the CFG. We refer to CFG nodes as locations. Assignment statements have a single successor, and control statements, such as if or while, have several successors, corresponding to the possible locations to which the control can jump. Transitions from a control statement to its successors are labeled by an expression that guards the transition. Recall that the design interacts with an environment that supplies its input signals. When the design is described as a CFG, the interaction induces a traversal of the CFG. Formally, given a CFG G with a set V of locations, and a test t = i0 , i1 , . . . , in ∈ (2I )n+1 of input assignments, 0 0 the execution of G on t is a sequence i0 , l0 , . . . , lm0 , o0 , I n n 1 1 i1 , l0 , . . . , lm1 , o1 , . . . , in , l0 , . . . , lmn , on ∈ (2 × V + × 0 2O )n+1 such that l0 is the initial location of G, for all 0 ≤ i i ≤ n, the location lmi corresponds to a read and write asseri+1 tion, oi is the new assignment to the output variables, and l0

For a description of a formal model of a real-life HDL see, for example, [FLLO95].

1

i matches the control ?ow of the CFG from location lmi upon i+1 i+1 reading ii+1 . The locations l1 , . . . , lmi+1 then correspond i+1 to the control ?ow of the CFG from l0 until the next input assignment is read. We often ignore the input and output variables and refer to the interaction as a word in V ? obtained by projecting the execution above on V . The second formalism is that of sequential circuits. We refer to a circuit as a tuple S = I, O, L, F, G, c0 , where I and O are the sets of input and output signals, respectively, L is a set of latches2 , c0 ∈ 2L describes the initial values of the latches, and F and G are families of the next-state and output functions. Thus, each latch l ∈ L has a function fl : 2I × 2L → {0, 1} in F, and each output signal o ∈ O has a function go : 2I × 2L → {0, 1} in G. A con?guration c ∈ 2L of the circuit describes the value of each latch. The circuit starts its interaction with the environment in con?guration c0 . When the circuit is in con?guration c and it reads a set i ∈ 2I of input signals, it moves to con?guration c′ in which the value of each latch l is fl (i, c), and in which it sends to the environment the set of output signals o with go (i, c) = 1. Accordingly, the execution of a circuit S on a test t = i0 , i1 , . . . , in ∈ (2I )n+1 , is a sequence i0 , c0 , o0 , i1 , c1 , o1 , . . . , in , cn , on ∈ (2I ×2L ×2O )n+1 that satis?es the conditions above. Both HDL and circuits enable a description of the design at different levels of abstraction [Hos95], yet abstraction is most naturally supported when the design is modeled as a symbolic ?nite state machine (FSM). We assume that the design is de?ned with respect to a set X of state variables, and it is speci?ed by predicates on X and X ′ – a primed version of the variables in X. Formally, an FSM is a tuple F = I, O, X, θin , θnext , G , where I and O are the input and output variables, X is the set of state variables, inducing the state space 2X , θin is a predicate on X describing the set of initial states, θnext is a predicate on X × X ′ describing the transition relation (there is a transition from state u to state v iff θnext (u, v ′ )), and G is a family of predicates that associates with each input or output variable s a predicate τs on X describing the set of states in which s holds. Likewise, predicates on X are used to describe other sets of interest, for example, the set of fair states when the design comes with an unconditional fairness constraint. Formally, a fair FSM F is a tuple F = I, O, X, θin , θnext , G, α , where α is a predicate on X describing the accepting condition. A behavior π is accepted by F if it satis?es α. The simplest accepting condition is B¨ chi condition [B¨ c62] (called impartiality in [MP92]), u u where α is a predicate on X and a behavior π satis?es α if it visits a state satisfying α in?nitely often. A non-symbolic FSM for the design is usually created manually by the designer in early stages of the design. Symbolic FSMs are automatically extracted from HDL programs, which is where abstraction plays an important role [Hos95]. The HDL program typically contains too many variables. The designer then selects a subset X ′ ? X of the state variables, and the predicates that de?ne the FSM are viewed as predi2

We use the term “latch” to refer to a generic sequential circuit element.

4

Hana Chockler et al.: Coverage Metrics for Formal Veri?cation

cates over X ′ to obtain an abstract FSM. Note that an FSM may be nondeterministic, thus its interaction with the environment may produce several outputs. 2.2 Model checking, vacuity, and coverage In linear-time model checking, we check whether a design has a desired behavior by checking whether a B¨ chi automau ton for the negation of the speci?cation has accepting runs on an FSM describing the design [VW86]. The speci?cation can be expressed as an LTL formula [Hol97], as a ForSpec formula [AFG+ 02], or as a B¨ chi automaton [HHK96,Kur98]. u A speci?cation ? in linear temporal logic can be translated to a nondeterministic B¨ chi automaton A?? that accepts all u words that do not satisfy ? [VW94]. Given an automaton A?? , we check that the product of F with A?? , which is a fair FSM F × A?? , does not contain accepting paths. Sanity checks for model checking address the problem of errors in the modeling of the design and the desired behavior, which are not discovered by model checking, for example, incompleteness of the speci?cation. These problems may cause “false positive” results of model checking and conceal errors in the design. Two such checks are vacuity and coverage, which we brie?y review below (for the full details, see [BBER01,KV03,HKHZ99,CKV01]). Intuitively, an FSM F satis?es a formula ? vacuously if F satis?es ? yet it does so in a non-interesting way, which is likely to point on some trouble with either F or ?. In order to formalize this intuition, we ?rst say that a subformula ψ of ? does not affect ? in F if for every formula ξ, the FSM F satis?es ?[ψ ← ξ] iff F satis?es ?, where ?[ψ ← ξ] denotes the formula obtained from ? by replacing ψ with ξ [BBER01]. As shown in [KV03], when ψ has a single occurrence in ?, instead of checking the replacement of ψ by all formulas ξ, one can check only the replacement of ψ by the formulas true and false. Thus, ψ does not affect ? in F whenever F satis?es ?[ψ ← true] iff F satis?es ?[ψ ← false]. Now, an FSM F satis?es a formula ? vacuously iff F |= ? and there is some subformula ψ of ? such that ψ does not affect ? in F . Equivalently, F satis?es ? vacuously if F |= ? and there is some subformula ψ of ? such that F also satis?es ?[ψ ← ⊥], where ⊥ is either false or true, depending on the polarity of ψ in ?. It is easy to see that vacuous satisfaction can be detected by a naive algorithm that model checks F with respect to formulas obtained from ?. More sophisticated algorithms are suggested in [PS02,KV03,Cho03,AFF+ 03]. Coverage in model checking was introduced in [HKHZ99, KGG99]. The metric in [HKHZ99] is based on mutations applied to an FSM. For an FSM F = I, O, X, θin , θnext , G , a state w ∈ 2X and an output variable q ∈ O, a mutant FSM ? Fw,q is obtained from F by dualizing the value of q in the state w. Thus, if τq is the predicate describing the set of states satisfying q in F , then the predicate τw,q , which describes the ? ?w,q , is satis?ed by w iff τq is not set of states satisfying q in F satis?ed by w. For all states v = w, the predicate τw,q is satis? ?ed by v iff τq is satis?ed by v. For an FSM F , a speci?cation ? that is satis?ed in F , and an output variable q, we say that

? ? q-covers w iff Fw,q no longer satis?es ?. By [HKHZ99], a state is covered if it is q-covered for some output variable q. It is easy to see that the set of states q-covered by ? can be computed by a naive algorithm that performs model check? ing of ? in Fw,q for each state w of F . More sophisticated algorithms are suggested in [HKHZ99,CKV01,CKKV01]. Chockler et al. also suggest the following re?nement of coverage metrics [CKKV01]. Instead of performing local mutations in F , we can perform local mutations in the in?nite tree TF obtained by unwinding F . A state w of F can appear many (possibly an in?nite number of) times in TF . Flipping the value of q in one occurrence of w in TF can have a different effect from ?ipping the value of q in all or some of the occurrences of w in TF . These differences are captured by the notions of node, structure, and tree coverage. Node coverage of a state w corresponds to ?ipping the value of q in one occurrence of w in the in?nite tree. Structure coverage corresponds to ?ipping the value of q in all the occurrences of w in the tree. It may seem that node coverage de?nes more ?ne-grained mutations than structure coverage. As shown in [CKKV01], the two metrics are incomparable: a state may be node-covered and not structure-covered, and vice versa. Tree coverage generalizes node and structure coverage and corresponds to ?ipping the value of q in some occurrences of w in the tree. Thus, w is q-tree-covered by ? if there exists a subset of occurrences of w in the in?nite tree obtained by unwinding F such that ?ipping q in this subset falsi?es ? in F . Chockler et al. describe a framework in which node, structure, and tree coverage can be computed by a symbolic algorithm; minor changes are required to capture the different types of coverage [CKKV01]. We describe their algorithm in more detail in Section 5. In this paper we introduce new types of mutations and new types of coverage metrics in model checking in order to capture better the different notions of coverage used in simulation-based veri?cation. Coverage in model checking is performed by applying mutations to a given FSM and then examining the resulting mutant FSMs with respect to a given speci?cation. Each mutation is generated in order to check whether a speci?c element of the design is essential for the satisfaction of the speci?cation. As we explain in more detail in Section 4, mutations correspond to omissions and replacements of small elements of the design, which can be given as an HDL program, an FSM, or a sequential circuit. Once we have a mutant FSM, there are two coverage checks we can perform on it. 1. Falsity coverage: does the mutant FSM still satisfy the speci?cation? 2. Vacuity coverage: if the mutant FSM still satis?es the speci?cation, does it satisfy it vacuously? Falsity coverage is the metric introduced in [HKHZ99], and we extend it here to handle mutations richer than these studied in the literature so far. Vacuity coverage is new. As we demonstrate in Example 1, it often provides information that falsity coverage fails to detect. In particular, in mutations that are based on omission of elements from the original de-

Hana Chockler et al.: Coverage Metrics for Formal Veri?cation

5

w0

w2 grant 2 w3 w4 grant 2

w1 grant 1

Fig. 1. The abstract FSM F .

sign (as we are going to see in Section 4, such mutations are popular in metrics adopted from simulation-based veri?cation), falsity coverage is useless for universal speci?cations. Indeed, having less behaviors, the mutant design is guaranteed to satisfy all the speci?cations satis?ed by the original design. Example 1. Consider the FSM F described in Figure 1, which abstracts a design with respect to the output signals grant1 and grant2 . Let ? = G(grant1 → F grant2 ). Thus, ? requires that (in all execution paths) each grant to the ?rst user is followed by a grant to the second user. It is easy to see that ? is satis?ed in F . Recall that the goal of coverage metrics is to check whether all the elements of the design play some role in the satisfaction of ?. Let us see which parts of F are covered by ?. We refer only to structure coverage in this example. – The positive value of grant2 in w4 is essential to the satisfaction of ?: One way to see this, is to observe that changing it to false creates the behavior {} · {grant1 } · {}ω in which grant1 is not followed by grant2 . The state w4 is falsity covered by ? with respect to mutations that ?ip the value of grant2 . – The value of grant1 in w1 is not essential to the satisfaction of ?. On the other hand, the designer had a reason to set it to true in w1 , as it is essential to the nonvacuous satisfaction of ?: Indeed, omitting the state w1 or ?ipping the value of grant1 there results in a mutant in which grant2 does not affect the satisfaction of ?. The state w1 is vacuity covered by ? with respect to mutations in which w1 is omitted and with respect to mutations that ?ip the value of grant1 . – One may also question negative values of variables. For example, while the negative value of grant2 in w0 is not essential to the satisfaction of ?, it is essential to its nonvacuous satisfaction: Indeed, ?ipping the value of grant2 in w0 to true results in a mutant in which grant1 does not affect the satisfaction of ?. the state w0 is vacuity covered by ? with respect to mutations that ?ip the value of grant2 . – Consider now the value of grant2 in the state w2 . All the paths of F that pass through w2 describe a behavior in which two grants – in both w2 and in w4 , are given to the

second user, after at most one grant was given to the ?rst user. The speci?cation does not require such a behavior, nor does it require a correspondence between the number of grants that each user gets. The labeling of w2 indeed does not play a role in the satisfaction of ?: ?ipping the value of grant2 in w2 or omission of w2 do not falsify ? in F , nor it causes ? to be satis?ed vacuously. This information may hint on a possible impreciseness or incompleteness in the de?nition of ?. For example, if the intention of the designer had been that each grant1 should be followed by a grant2 in the next step, the correct speci?cation should have been G(grant1 → Xgrant2 ), in which case w2 would have been falsity covered with respect to mutations that ?ips the value of grant2 . Moreover, if the intention of the design had been to require a correspondence between the number of grants that each user gets, the coverage information would lead to a re?nement of the speci?cation, after which an error would be discovered. Another possibility is that F contains redundancies, in which case the state w2 can be omitted from the FSM without violating ?. Recall that the positive value of grant2 in w4 is essential for the satisfaction of ?. An execution that reaches w4 stays there forever, and the second user is kept being granted. One may wonder whether all these grants are essential. This is where the difference between structure-based and node-based coverage appears: while w4 is structure-covered by ? with respect to the mutation that ?ips the value of grant2 in w4 , it is not node-covered by ? with respect to the same mutation, for both the falsity and vacuous coverage. Indeed, node-coverage checks whether the positive value of grant2 plays a role in all the visits to w4 .

3 Coverage Metrics in Simulation-based Veri?cation In this section we brie?y survey coverage metrics in simulationbased veri?cation – metrics we are going to adopt for the setting of formal veri?cation in the next section. Each of the metrics is “tailored” for a speci?c representation of the design or a speci?c veri?cation goal. The reader is referred to [TK01] for a detailed survey. All metrics refer to a set of input sequences (or tests) t ∈ (2I )? with respect to which the design is simulated. 3.1 Syntactic coverage metrics Syntactic coverage metrics assume a speci?c formalism for the description of the design and measure the syntactic part of the design visited in the process of execution of a given input sequence. Commonly [Mar99,TK01], high coverage according to syntactic-based metrics is considered a precondition to moving to other more sophisticated (and time consuming) coverage metrics.

6

Hana Chockler et al.: Coverage Metrics for Formal Veri?cation

Code coverage Code-based coverage metrics refer to the HDL program that describes the design or to its CFG. Measuring code coverage requires little overhead and it is easy to interpret the coverage information. This makes code coverage the most popular metric [UZ98,TK01]. The most widely used code-coverage metrics are statement and branch coverage. Essentially, an object is covered if it is visited during the execution of the input sequence. Again, the fully-formal de?nition depends on the particular HDL used, but a semi-formal de?nition is given in terms of the computation of the CFG as follows. Let G be a CFG. For an input sequence t ∈ (2I )? such that the execution of G on t, projected on the sequence of locations, is l0 , . . . , lm , we say that a statement τ is covered by t if there is 0 ≤ j ≤ m such that the control location lj corresponds to τ . We say that a branch l, l′ between two control locations is covered by t if there is 0 ≤ j ≤ m ? 1 such that lj = l and lj+1 = l′ . More sophisticated metrics measure the way expressions in the guards labeling the CFG’s transitions are satis?ed. For example, expression coverage checks whether a Boolean expression has been satis?ed by all its satisfying assignments (e.g., whether a1 == a2 has been satis?ed by both an a1 = a2 = 0 and an a1 = a2 = 1 assignment). Circuit coverage Circuit-structure based coverage metrics refer to the circuit that describes the design. Thus they identify the physical parts of the circuit that are covered. Measuring circuit coverage is usually easy and it is easy to interpret the coverage information. Unlike code coverage, however, it is not easy to use the coverage information in order to generate new tests that direct simulation towards the unexplored areas of the design. The most widely used circuit-coverage metrics are latch and toggle coverage [HH96,KN96]. Essentially, a latch is covered if it changes its value at least once during the execution of the input sequence. Similarly, an output variable is covered if its value has been toggled. Formally, for a circuit S and an input sequence t ∈ (2I )n+1 such that the execution of S on t is i0 , c0 , o0 , i1 , c1 , o1 , . . . , in , cn , on , we say that a latch l ∈ L is covered by t if there is j ≥ 0 such that l ∈ c0 iff l ∈ cj . Similarly, an output variable o ∈ O is covered by t if there are 0 < j1 < j2 such that o ∈ o0 iff o ∈ oj1 iff o ∈ oj2 . Note that toggle coverage requires that the value of an output variable should be changed at least twice during the execution of t. Hit count The notion of hit count, introduced in [Ver03], replaces binary coverage queries with quantitative measurements (how many times an object has been visited). Intuitively, the more times we visit an element, the bigger is our con?dence that its functionality is tested. 3.2 Semantic coverage metrics

phisticated than syntactic coverage metrics. We consider the following metrics. FSM coverage Due to the large size of FSMs for complete systems, FSM-based coverage metrics refer to more abstract FSMs constructed manually by the designer, or automatically extracted from the design by projecting its symbolic description on a subset of the state variables as explained in Section 2.1 [TK01]. Similarly to code coverage, a state or a transition of the abstract FSM is covered if it is visited during the execution of the input sequence. The fact that coverage is checked with respect to an abstract FSM makes the interpretation of the coverage information harder (linking the uncovered parts of the FSM to uncovered parts of the HDL program is not trivial) and has led to the use of more sophisticated metrics. In particular, limited-path coverage metrics check that important sequences of behavior are exercised [SA99]. Transition coverage can be viewed as a special case of path coverage, for paths of length 1. Assertion coverage In assertion coverage, also called “functional coverage” in [TK01,Cad03], the user provides a list of assertions referring to the variables of the design. The assertions describe some conditions that may be satis?ed during the execution or a state of the design during the execution. They may be propositional (“snapshot tasks”) or temporal (describing a behavior along several clock cycles). A test t covers an assertion a if the execution of the design on t satis?es a. The assertion-coverage metric measures what assertions are covered by a given set of input sequences. Mutation coverage In mutation coverage, the user introduces a small change (aka “mutation”) to the design, and checks whether the change leads to an erroneous behavior [DLS78, Bud81,ZHM97]. The coverage of a test t is measured as the percentage of the mutant designs that fail on t, that is, the percentage of the mutations that t “catches”. The list of interesting mutations can be written manually or automatically following some mutation criteria. For example, a local mutation can be ?ipping a value of one output variable in a circuit. Budd and Angluin [BA82] de?ne the neighborhood Φ(P ) of a program P as a set of all possible mutants obtained from P by a (prede?ned) local mutation. Similarly, we can de?ne a neighborhood of an FSM F (for example, all FSMs obtained from F by merging two states) or a circuit S. In mutation coverage the goal is to cover the whole neighborhood of the design, that is, to ?nd a set of input sequences such that for each mutant design there exists at least one test that fails on it (this notion is similar to the notion of local correctness in [BA82]). As discussed in Section 2.2, mutation coverage is the metric that inspired most of the work on coverage in model checking. 4 Coverage Metrics in Model Checking

Semantic coverage metrics measure the part of the functionality of the design exercised by the set of input sequences. Semantic coverage metrics require user help and are more so-

In this section we discuss how the coverage metrics from simulation-based veri?cation can be adopted in model check-

Hana Chockler et al.: Coverage Metrics for Formal Veri?cation

7

ing. Thus, for each of the metrics described in Section 3, we de?ne a metric that can be used in the context of model checking. 4.1 Syntactic coverage In syntactic coverage, we assume that we are given the syntactic representation of the design (an HDL code or a CFG) with respect to which we measure the coverage. Since in the process of model checking we visit the whole reachable part of the design, metrics that measure the part of the design exercised during the simulation cannot be applied directly to model checking. Essentially, we adopt these metrics by replacing the question whether a part of the design has been visited during the simulation by the question whether the part plays a role in the success of the veri?cation process, where playing a role means that the part is essential for the satisfaction or the non-vacuous satisfaction of the speci?cation. The latter is checked by reasoning about the behavior of a mutant design in which the part is modi?ed or omitted. Code coverage Let G be a CFG and ? a speci?cation that is satis?ed in G. We say that a statement τ of G is covered by ? if omitting τ from G causes vacuous satisfaction of ? in the mutant CFG. Similarly, a branch l, l′ of G is covered if omitting it causes vacuous satisfaction of ?. Note that falsity coverage would be meaningless here, since omitting a statement or a branch of CFG results in a design with fewer behaviors, which is guaranteed to satisfy the universal speci?cation. Indeed, omission of a statement in the CFG leads to a design in which this statement is unreachable, and thus all the executions that contain this statement no longer exist. Omission of a branch in the CFG leads to a design in which all the executions in which the branch is taken no longer exist. In both cases, no new executions are added, and executions that stay in the mutant design are not changed. Thus, the mutated design is simulated by the original design (its set of behaviors is a subset of the set of behaviors of the original design), Therefore, the mutant design satis?es all universal speci?cations that are satis?ed by the original design [GL94]. In expression coverage, we check whether omitting the behaviors in which the variables have a particular satisfying assignment for a particular expression leads to vacuous satisfaction of ?. For example, if the expression is a1 == a2 and it guards a block B of statements, we check whether the mutant design obtained by skipping B in case a1 = 0 and a2 = 0 satis?es the speci?cation vacuously, and similarly for a1 = 1 and a2 = 1. Circuit coverage Recall that latch and toggle coverage metrics check whether the value of a speci?c latch or variable in the circuit changes during the execution of an input sequence. We replace this question by the question whether disabling the change causes the speci?cation to be satis?ed vacuously. Thus, a latch l ∈ L is covered if the speci?cation is vacuously satis?ed in the circuit obtained by ?xing the value of l to its initial value. Similarly, an output variable o ∈ O is covered if

the speci?cation is vacuously satis?ed in the circuit obtained by allowing o to change its value only once. Thus, if the initial value of o is 0, the circuit is obtained by ?xing o to 1 as soon as it changes its value to 1, and if the initial value of o is 1, the circuit is obtained by ?xing o to 0 as soon as it changes its value to 0. Hit count Recall that the distinction between structure, node, and tree coverage enable us to choose whether to perform a mutation on every visit of the model checker to the mutated element, on exactly one visit, or on a subset of the visits. We de?ne hit count in model-checking coverage as the minimal number of visits in which we have to perform the mutation (or omit the element) in order to falsify the speci?cation in the design or to make it vacuously satis?ed. 4.2 Semantic coverage Among the semantic coverage metrics, mutation coverage has already been adopted to the setting of model checking. As discussed in Section 2.2, we suggest a strengthening of the adopted metrics by checking the effect of the mutation not only on the satisfaction of the speci?cation, but also on its vacuous satisfaction. Below we describe the adoption of the other semantic coverage metrics. FSM coverage In FSM coverage we are given an abstract FSM F and we check the in?uence of mutations and omissions in this FSM on the result of model checking of the speci?cation ? in the design. In state coverage, for a state w of F we check the in?uence of omission of w or changing the values of output variables in w on the (non-vacuous) satisfaction ? of the speci?cation in the design. Clearly, a mutant FSM Fw obtained from F by omitting w has fewer behaviors than F , thus for omissions of a state we only check vacuity cover? age. On the other hand, a mutant FSM Fw,o obtained from F by ?ipping the value of the output variable o ∈ O in w can also falsify the speci?cation, thus we check falsity and vacuity coverage. In path coverage, we check the in?uence of omitting or mutating a ?nite path on the (non-vacuous) satisfaction of the speci?cation in the design. A path π of length c in F is a sequence of states w1 , . . . , wc of F such that for all 1 ≤ i ≤ c ? 1 we have θnext (wi , wi+1 ). Let us ?rst de?ne coverage for omissions of a path. A path π is covered by ? if the mu? tant FSM Fπ obtained from F by omitting all behaviors that contain π satis?es ? vacuously. On the other hand, we can also introduce mutations that replace π with a mutant path ? π π in the FSM. Then, the mutant FSM Fπ,? is obtained from ? ? π F by replacing π with π . The mutant FSM Fπ,? can falsify ? ? or can satisfy ? vacuously, thus for mutations that replace a path with another, mutant, path we check both falsity and vacuity coverage. We note that all possible mutations in the FSM can be introduced consistently on each occurrence of the mutated element, on exactly one occurrence, or on a subset of occurrences, thus resulting in structure, node, or tree coverage, respectively.

8

Hana Chockler et al.: Coverage Metrics for Formal Veri?cation

w, u0 , s0 s0 w0 s1 w2 s2 w3 s3

...

w, w, s w, w′ , s ?ipping q

. . .

Fig. 2. The automaton M .

fair path w, u, s ∈ P We demonstrate path coverage on the FSM in Figure 1. Assume that we want to check the effect of omitting the path π1 = w0 , w2 , w3 on the (non-vacuous) satisfaction of ? = G(grant1 → F grant2 ). The executions that contain π1 are + ω the ones that are de?ned by the ω-regular expression w0 w2 w3 w4 (we use + to denote a positive number of repetitions of the state). Note that this is not the same as removing the transitions w0 , w2 and w2 , w3 from the FSM, as removing these + ω transitions would also remove the executions w0 w1 w2 w3 w4 . The mutant FSM is the product of F with the automaton M that rejects paths that contain w0 , w2 , w3 as a subpath. The automaton M is presented in Figure 2 (the unlabeled edges complement the labeled ones to the full alphabet; that is, the self-loop in s0 is labeled with Σ ? \ {w0 }, and similarly for other unlabeled edges). The speci?cation ? is satis?ed non-vacuously in the mutated FSM. Indeed, replacing grant1 with true we get the ω speci?cation GF grant2 , which does not hold in the path w0 ; replacing grant2 with false we get the speci?cation G(grant1 → F false), which is satis?ed only in paths that do not have states labeled with grant1 , and thus is falsi?ed in all paths containing w1 . Therefore, the path π1 is uncovered with respect to omissions. Let us now check the effect of replacing the path π2 = w0 , w0 with the path π2 = w0 , w4 . It is easy to ? see that all paths in the mutated FSM now reach a state where grant2 holds. Indeed, the only path in the original FSM that ω does not reach a state where grant2 holds is w0 , and this path does not exist in the mutated FSM. Thus, ? is satis?ed vacuously in the mutated FSM (grant1 can be replaced with true without violating the speci?cation), and therefore the mutation that replaces π2 with π2 is covered. ? Assertion coverage An input to assertion-coverage check is an FSM F , a speci?cation ? that is satis?ed non-vacuously in F , and a list of LTL assertions a1 , . . . , ak . An assertion ai is ? covered by ? in F if the mutant FSM Fai obtained from F by omitting all behaviors that satisfy a satis?es ? vacuously. We note that this de?nition is similar to the de?nition of FSM path coverage. The only difference is in the description of the mutation: in FSM path coverage we omit behaviors that contain a given ?nite path π, whereas in assertion coverage we omit behaviors that satisfy a given assertion.

Fig. 3. A cycle is reachable in the augmented automaton

can be reduced to model checking (possibly of mutant speci?cations and/or mutant designs). Let F be an FSM, ? a spec? i?cation that is satis?ed in F non-vacuously, and F a mutant ? does not satisfy ?, we say that F is falsity covered ? FSM. If F ? by ?. If F satis?es ?, it still may be vacuity covered by ? ? if it satis?es ? vacuously. Formally, F satis?es ? vacuously ? |= ? and there exists ψ ∈ cl(?) such that F satis?es ? if F ?[ψ ← ⊥]. Thus, like falsity coverage, we check whether a ? mutant design F satis?es a speci?cation, only that here the speci?cation is also mutated. Mutation coverage The algorithm we present for falsity-coverage computation is based on the coverage algorithm described in [CKKV01]. That algorithm computes symbolically falsity coverage for mutations that ?ip the value of a variable q ∈ O in one state w of the FSM. The idea is to look for a fair path in ? the product of the mutant FSM F and an automaton A?? for the negation of ?. The state space of the product is 2X × S, where X is the set of state variables of F , S is the state space of A?ψ , and the transitions of the product are induced by the transition relations of F and A?ψ . In order to compute the set of covered states, it is suggested in [CKKV01] to add |X| new variables that encode the state w in which the value of q is ?ipped. It is now possible to de?ne symbolically an augmented product, with state space 2X × 2X × S, where the ?rst component of a state w, u, s is the state w that is being considered, and the two other components are as in the usual product automaton. The value of the ?rst component is chosen nondeterministically at initialization and is kept unchanged. The copy of the augmented product with ?rst component w checks whether the mutation of F in which q is ?ipped in w contains a fair path (in which case ?ipping q in w violates the speci?cation). Thus, when the augmented product is in a state w, w, s , the set of successor states contains all triples w, u, t such that u is a successor of w and ? t ∈ δ(s, σ ), where σ is the label of w in Fw,q . The above de? ? scribes structure coverage, where the value of q is ?ipped in all visits. Likewise, we can de?ne an augmented product in which the value of q in w is ?ipped only one time (node coverage) or some of the times (tree coverage). We can now use a symbolic algorithm in order to ?nd the set P of all triples w, u, s from which there exists a fair path in the augmented product automaton (see Figure 5 for the intuitive explanation of reachability of a cycle in the augmented product).

5 Coverage Computation In Section 4 we described new coverage metrics for model checking. In this section we discuss how to compute these metrics. We ?rst show that both vacuity and falsity coverage

Hana Chockler et al.: Coverage Metrics for Formal Veri?cation

9

The covered states are those w such that w, u0 , s0 ∈ P , for some initial states u0 of F and s0 of A?ψ . In particular, triples of the form w, u0 , s0 in P , for initial states u0 of ? F and s0 of A?ψ , correspond to a path of Fw,q that violates the speci?cation. Hence, the set of states that are covered by the speci?cation can be calculated symbolically by intersecting P with the initial state set of the product automaton and projecting the result on the ?rst component. Vacuity coverage Recall that checking whether a system satis?es a speci?cation vacuously involves model checking of a mutant speci?cation. We adjust the symbolic algorithm in [CKKV01] to this setting by adding a new variable x that encodes the subformula ψ ∈ cl(?) that is being replaced with ⊥. The variable x is an integer in the range 0, . . . , |cl(?)|, thus it can be encoded with O(log |?|) Boolean variables. The value 0 of x stands for “no replacement”, thus it checks the satisfaction of ? in the system. As with mutations, the values of these variables are chosen nondeterministically at initialization and are kept unchanged. For example, if ? = y1 ∨ y2 , and 1 encodes y1 and 2 encodes y2 , then the value 1 of x corresponds to the replacement of y1 with false (which is the ⊥ value for y1 in ?) resulting in the formula (y1 ∨ y2 )[y1 ← false] = y2 . In the automaton A?? , each state variable corresponds to a subformula (cf. [BCM+ 92]), thus the nondeterministic choice of the subformula leads to a mutant automaton A??[ψ←⊥] . The state space of the augmented product now consists of triples x, u, s , where x encodes the subformula replaced with ⊥, and u and s are the components of the product automaton. The successors of x, u, s are the triples x, u′ , s′ such that u′ , s′ is a possible successor of u, s in a product between the system and the automaton A??[ψ←⊥] , where ψ is the subformula encoded by x. The subformulas that affect the value of ? in the systems are these encoded by a value x for which there are initial states u0 and s0 of the system and the automaton, respectively, such that there is a fair path from x, u0 , s0 . Let P be the set of triples from which a fair path exists in the augmented product (as above, P can be found symbolically), and let P ′ be the intersection of P with the initial states of the system and the automaton, projected on the ?rst element. Note that x ∈ P ′ iff the subformula associated with x affects the value of ? in the system. Thus, ψ is satis?ed vacuously in the system if 0 ∈ P ′ and P ′ = {1, . . . , cl(ψ)}. In order to get a symbolic algorithm for vacuity coverage, we combine the above algorithm with the one of [CKKV01]. For example, if we want to ?nd the set of states w such that ?ipping the value of q in w causes the speci?cation to be satis?ed vacuously, we augment the state space of the product of F and A?? by variables that encode both the state in which we do the mutation and the subformula that is being replaced with ⊥. Thus, the state space of the augmented product now consists of 4-tuples w, x, u, s , where w is the state in which we ?ip q, x encodes the subformula replaced with ⊥, and u and s are the components of the product automaton. The successors of w, x, u, s are the 4-tuples w, x, u′ , s′ such that u′ , s′ is a possible successor of u, s in a prod-

uct between the system q ?ipped in w and the automaton A??[ψ←⊥] , where ψ is the subformula encoded by x. As above, the initial values of w and x are chosen nondeterministically at initialization and are kept unchanged. The states that are not vacuity covered are states w such that for all the assignments x, there are initial states u0 and s0 of the system and the automaton, respectively, such that there is a fair path from w, x, u0 , s0 . Thus, if P is the set of 4-tuples from which a fair path exists in the augmented product (as above, P can be found symbolically), then the set of mutations that are not covered can be obtained from P as follows. Let P ′ be the intersection of P with the initial states of the system and the automaton, projected on the ?rst two elements. Note that a pair w, x is in P ′ if ?ipping q in w violates the speci?cation obtained by replacing the subformula associated with x by ⊥. Consider now a the set of mutations de?ned by (?x)P ′ (w, x). It contains states that lead to failure of φ regardless of what subformula ψ of φ is replaced by ⊥, which means that these mutations do not lead to vacuous satisfaction and therefore they are not covered. As we specify below, if we want to check vacuity coverage for other types of mutations, we replace the variables that encode w by variables that encode other types of mutations. Code coverage Recall that in code coverage we need to check whether the omission of parts of the code causes the speci?cation to be satis?ed vacuously. Accordingly, for code coverage, it is simpler to de?ne the mutations with respect to the HDL code. Let k be the number of elements in the code we want to check (e.g., the number of lines). We introduce a new variable mut, which is an integer in the interval [1, . . . , k]. The value i of mut indicates that the mutation is in element li , which we want to omit, and we need O(log k) Boolean variables to encode it. The HDL code is instrumented using source-to-source translation in (see [BKM02] as an example of such instrumentation) so that li in the code is replaced by the statement “if (mut = i) then li else skip”. The instrumented code represents all the mutant designs3 . The product of the FSM induced by the instrumented code and A?? subsumes all the mutations of the code. It is now possible to apply the symbolic algorithm described above (instead of the variables that encode w, we now have the variables that encode mut) for detecting the mutations that lead to vacuous satisfaction. In expression coverage, we do something similar. Let e1 , . . . , em be the expressions we want to check, and let Vi = i i {v1 , . . . , vn } be the Boolean variables over which ei is de?ned. Assume that n bounds the number of variables in every expression. Let “if ei then Bi ” be the statement that contains ei as a guard (handling of “while” or “until” statements is similar). Recall that we want to check, for each ei and for each satisfying assignment f ∈ 2Vi , whether skipping Bi when the variables have value f causes the speci?cation to be satis?ed vacuously. Accordingly, we add a variable mut (encoded by O(log m) Boolean variables) that indicates the

The user may wish to include 0 (no mutation) in the range of mut, in which case the instrumented code represents also the original design.

3

10

Hana Chockler et al.: Coverage Metrics for Formal Veri?cation

expression to be checked, and n variables u1 , . . . , un that encode assignments to n variables. As usual, the variables get their value nondeterministically at initialization. The HDL code is now instrumented so that “if ei then Bi ” in the code i is replaced by “if (mut = i) or (ei ∧ 1≤j≤n vj = uj ) then Bi else skip”. It is now possible to apply the symbolic algorithm described above for detecting the expressions and assignments that lead to vacuous satisfaction. Circuit coverage In latch coverage, we want to restrict the product of F and A?? to paths in which the value of a latch is not allowed to change, and check whether this causes vacuous satisfaction. Thus, we augment the product with variables that encode the examined latch and (for the vacuity check) the subformula of ? that we replace with ⊥. When the augmented product is in state l, x, u, s , it proceeds to states l, x, u′ , s′ such that u′ , s′ is a possible successor of u, s in a product between the system with l that is not changed and the automaton A??[ψ←⊥] , where ψ is the subformula encoded by x. The values of l and x are chosen nondeterministically at initialization. Let P be the set of 4tuples from which a fair path exists in the augmented product, and let P ′ be the intersection of P with the initial states of the system and the automaton, projected on the ?rst two elements. Note that a pair l, x is in P ′ if disallowing l to change violates the speci?cation obtained by replacing the subformula associated with x with ⊥. Thus, the set of latches de?ned by (?x)P ′ (l, x) contains latches that are not covered. Now, toggle coverage is similar, only that we allow the value of an output variable to be changed only once. For that, we need an additional new Boolean variable f lag that indicates whether the variable has already changed its value once. That is, the state space of the augmented product consists of 5tuples o, f lag, x, u, s ∈ O × {0, 1} × cl(?) × 2X × S. When f lag = 0 and the value of o changes, then f lag is assigned 1. Then, the augmented product continues as in the case of latch coverage, with the value of o unchanging. FSM coverage State and transition coverage can be computed using the techniques of mutation-based metrics. We now describe the computation of path coverage. We start with mutations that omit all behaviors that contain a given ?nite path π = w1 , . . . , wc . Let Mπ be a monitor that ?lters away paths that contain π as a sub-path. That is, Mπ is a fair FSM that accepts paths ρ such that π is not a sub-path of ρ. Since Mπ only cares for the values of control variables that encode the states (and not, for example, for the values of output variables in these states), the set of input variables of Mπ is the set of control variables X of F , and Mπ does not have ? output variables. For a given path π, the mutant FSM Fπ is the product FSM F × Mπ , which contains only the computations of F that do not have π as a sub-path. Then, π is ? vacuity covered by ? if Fπ satis?es ? vacuously. For a set of paths {π1 , . . . , πk }, we can compute the set of covered paths symbolically using the techniques as described above for vacuity coverage. The state space of the augmented product consists of 5-tuples mut, x, u, r, s , where mut encodes

the path πi ∈ {π1 , . . . , πk }, x encodes the subformula of ? that we replace with ⊥, and u, r, and s are the components of the product F × Mπmut with A??[ψ←⊥] . The successors of mut, x, u, r, s are the 5-tuples mut, x, u′ , r′ , s′ such that u′ , r′ , s′ is a possible successor of u, r, s in a product ? between the fair FSM Fπmut , which is F × Mπmut and the automaton A??[ψ←⊥] , where ψ is the subformula encoded by x. The vacuity uncovered paths are these encoded by values of mut such that for all the assignments x, there are initial states u0 , r0 , and s0 of the FSM and the automaton, respectively, such that there is a fair path from x, mut, u0 , r0 , s0 . As above, the set of 5-tuples P from which a fair path exists in the augmented product can be found symbolically, and the set of vacuity covered paths can be computed from it. In a similar way we can de?ne mutations of paths that replace a ?nite path π with a path π of the same length, redi? recting the system to another execution. If a mutated path is of length 1, the mutation redirects one transition. For a path π replaced with a mutant path π , we use a monitor Mπ,? . In the ? π ? product Fπ of F with Mπ,? , all the occurrences of π are reπ placed by π . Note that for mutated (rather than omitted) paths ? we can compute both falsity and vacuity coverage. The computation of falsity coverage is similar to falsity coverage of CFG described above, where the state space of the augmented product consists of 4-tuples mut, u, r, s , with mut encoding the mutated path, and u, r, and s are the components of ? the product automaton of Fπ with A?? . Vacuity coverage is computed similarly to the case of omission of paths.

Assertion coverage For an LTL assertion a, a monitor for a is the automaton A?a . Given assertions a1 , . . . , ak , the mutant FSM is the product F × A?a1 × . . . × A?ak . Falsity and vacuity coverage of a set of assertions is computed similarly to FSM path coverage, where the variable mut encodes the assertion amut for 1 ≤ mut ≤ k.

Hit count For a state w ∈ 2X of F , an output variable q ∈ O, and a speci?cation ? that is satis?ed in F , the q-hit count of w in F for ? is the minimal number of occurrences of w in the in?nite tree obtained by unwinding F in which q has to be ?ipped in order to falsify ? in F . The computation of hit count may be hard in the general case. We restrict the computation of hit count to the following easier question: “given a threshold t, is the q-hit count of w in F for ? at least t?” The tree coverage computation algorithm of [CKKV01] can be modi?ed in order to decide whether the hit count is below or above the threshold. We introduce a new variable count that counts the number of occurrences of w in which q is ?ipped. We now proceed as in tree coverage, except that whenever we visit a state w and we choose to ?ip q we also increment count until we hit the threshold t. When we compute the set of covered states, we return only these whose projection on count is greater than t. This can also be applied to other types of coverage.

Hana Chockler et al.: Coverage Metrics for Formal Veri?cation module example(o1 , o2 , o3 ); reg o1 , o2 , o3 ; initial begin o1 = o2 = o3 = 0; end always @(posedge clk) begin assign o1 = o1; assign o2 = o2 | o3; assign o3 = ?o3; end endmodule

Fig. 4. The Verilog description of the design.

11

000

001 clk

o1

011

010 o2 clk

100

101 o3

111

110

clk

Fig. 5. The FSM with three latches.

6 A Detailed Example In this section we demonstrate our metrics with respect to a simple design and some speci?cations. The design is described as a part of a Verilog program, an FSM, and a circuit. The design has three registers, which encode the state space. The design is described by means of a Verilog program in Figure 4. Figure 5 shows the FSM (each state is labeled by the truth values of o1 , o2 , and o3 ) and the circuit for this design. Let us compute coverage with respect to the speci?cation ? = G(o2 → F o3 ). That is, ? requires that in all execution paths, each positive value of o2 is eventually followed by a positive value of o3 . We start with code coverage. The line “assign o1 = o1;” is uncovered by this speci?cation with respect to both omissions and mutations. Indeed, omitting this line from the code or assigning a different value to o1 does not falsify ?. Observing the circuit, it is easy to see that the register o1 is latch uncovered (where the term “latch” refers to a generic sequential circuit element — a register, in this case) . Indeed, ?xing o1 to 0 for the whole execution does not affect the satisfaction of ?. In FSM coverage, we compute falsity and vacuity coverage for omissions and mutations of states and paths. Note that all states in which o1 = 1 are unreachable, and thus uncovered with respect to all speci?cations. On the other hand, the state 011 is covered with respect to ? and mutations of o3 . Indeed, ?ipping the value of o3 in 011 causes

the state 011 to merge with the state 010. Then, o3 never becomes positive after o2 becames positive, and therefore ? is violated. Now we compute coverage with respect to the speci?cation ψ = G?o1 ∧ F (o2 ∧ Xo3 ). That is, ψ requires that in all executions o1 is negative everywhere and there exists a state where o2 is positive and o3 is positive in the successor state. We start with code coverage. While omitting each of the lines with an assignment statement for o2 and o3 falsi?es the speci?cation, it is easy to see that certain modi?cations of the code do not render ψ untrue. For example, replacing the line “assign o2 = o2 | o3;” with the line “assign o2 = ?o1;” results in the FSM in which o2 is positive starting from the second state, and ψ still holds. Thus, the above line is code uncovered with respect to mutations of the code. We can also see that all transitions are covered with respect to omissions. Indeed, removing a transition results in an empty FSM, which satis?es all speci?cations vacuously. On the other hand, there are uncovered transitions with respect to mutations. For example, the transition from 011 to 010 can be replaced by a self-loop in 011 without falsifying the speci?cation. Let us now study latch coverage for this speci?cation. Fixing the value of o1 to its initial value through the execution does not affect on the satisfaction of ψ. On the other hand, ?xing either o2 or o3 falsi?es ψ. Thus, o1 is latch uncovered and both o2 and o3 are latch covered with respect to ψ. In toggle coverage, we allow a latch to change its value once during the execution. Then, both o2 and o3 are uncovered with respect to ψ, as ?xing their value after they become positive does not falsify ψ. The properties ? and ψ together cover a large part of the design. At the same time, some parts are uncovered by both speci?cations. For example, both speci?cations are still satis?ed in a mutant design in which the states 001 and 010 are merged into the single state 010. One possible way to solve this problem is to add a speci?cation X?o2 . Another possibility is that the designer overlooked the fact that merging the states 001 and 010 results in a smaller correct design.

7 Complexity of Computing Coverage In Section 5 we described ways to compute the coverage metrics suggested in Section 4. In this section we measure the complexity of computing these metrics. All metrics can be computed symbolically, so the complexity estimations are in terms of the number of ROBDD4 (Boolean) variables and the number of symbolic operations required for the computation. The computation is based on the symbolic model-checking algorithms. The number of the ROBDD variables required for encoding the state space of the veri?ed FSM is logarithmic in the size of the state space. For different coverage algorithms we need a different number of additional ROBDD variables. Let n be the number of ROBDD variables required for encoding the state space of the FSM F , and m the number of ROBDD variables required for encoding the state space of

4

Reduced Ordered Binary Decision Diagram.

12

Hana Chockler et al.: Coverage Metrics for Formal Veri?cation metric mutation coverage vacuity coverage code coverage circuit coverage FSM path coverage assertion coverage hit count complexity 3n + 2m 3n + 3m 2n + 2m + log k 2n + 3m + log l 3n + 4m + log p 3n + 4m + log k 3n + 2m + log t

A?? . In order to encode the transition relation, symbolic algorithms use two copies of the ROBDD variables that encode the state space. One untagged copy for the current state, and one tagged copy for the next state. Mutation coverage Recall that the algorithm for computing mutation coverage computes the set P of all triples w, u, s from which there exists a fair path in the augmented product automaton. The set of mutation covered states is then easily extracted from P , as this is the set of those w such that w, u0 , s0 ∈ P , for some initial states u0 of F and s0 of A?ψ . We need 2n+ m ROBDD variables in order to encode the triples, thus the straightforward implementation yields 4n + 2m variables. We note, however, that the values of the ?rst n variables, which encode the mutated state of F, are chosen non-deterministically at initialization and are kept unchanged during the execution. Therefore, there is no need to keep two copies of these variables. Thus, the total number of ROBDD variables is 3n + 2m, and the complexity of the computation is O(|F |3/2 |A?? |). As has been shown in [KGG99,Kat01], the techniques of early quanti?cation and variable interleaving in the ROBDD can be used in order to further reduce the number of required variables. Vacuity coverage Vacuity coverage is computed similarly to mutation coverage. Here, the set P consists of 4-tuples w, x, u, s where w is the state in which we ?ip q, x encodes the subformula replaced with ⊥, and u and s are the components of the product automaton. As above, the initial values of w and x are chosen nondeterministically at initialization and are kept unchanged. Thus, we need only one copy of the ROBDD variables that encode the mutated state and the mutated subformula, and therefore, the total number of ROBDD variables needed for the computation is 3(n + m). The complexity of the computation is therefore O((|F | · |A?? |)3/2 ). Code coverage Let k be the number of elements in the code we want to check (e.g., the number of lines). Encoding the omitted line of code requires log k ROBDD variables, and so the mutated FSM can be encoded using n + log k variables. The complexity of model-checking of the mutated FSM is then O(|F | · k · |A?? |). Circuit coverage Circuit coverage is a special case of vacuity coverage, where we study the effect of mutations that ?x the value of one latch during the whole execution on the (nonvacuous) satisfaction of the speci?cation. The set P consists of 4-tuples l, x, u, s , where l encodes the latch that is kept unchanged, x encodes the subformula replaced with ⊥, and u and s are the components of the product automaton. The ?rst two components are chosen non-deterministically at initialization and are kept unchanged. Thus, the number of ROBDD variables needed for the computation is O(|L|·|F |·|A?? |3/2 ), where L stands for the number of latches. Toggle coverage is computed similarly to circuit coverage, with the addition of the single Boolean variable that indicates whether the latch has already changed its value once.

Fig. 6. The complexity of calculating different coverage metrics in terms of the number of variables required for the symbolic algorithms

FSM coverage For path coverage, we compute the set P of 5-tuples mut, x, u, r, s , where mut encodes the path πi ∈ {π1 , . . . , πk }, x encodes the subformula of ? that we replace with ⊥, and u, r, and s are the components of the product F × Mπmut with A??[ψ←⊥] . Thus, compared with mutation coverage, we need additional m + log k ROBDD variables, so the total number of ROBDD variables is 3n + 4m + log k, leading to the complexity of O(k|F |3/2 |A?? |2 ). Assertion coverage Assertion coverage is computed similarly to FSM path coverage, where the variable mut encodes the assertion amut for 1 ≤ mut ≤ k, and thus has the similar complexity. , Hit count Let t be the threshold of the hit count. We need O(log t) new variables to encode the variable count that increases from 0 to at most t. The algorithm computes the set of 4-tuples count, w, u, s from which there exists a fair path in the augmented product automaton, where w encodes the mutated state. The value of w is chosen non-deterministically at initialization and is kept unchanged during the execution. The value of count is increased non-deterministically on transitions in which we choose to ?ip the value of the q. Thus, we need n + O(log t) additional variables, and therefore the complexity of hit count computation for tree coverage is the complexity of mutation coverage computation multiplied by the threshold t. Summary In Figure 6, we summarize the complexity of computing different coverage metrics in terms of the number of ROBDD variables required by the symbolic algorithms. We denote by n and m the number of variables required for encoding the state space of F and A?? , respectively. Also, l denotes the number of latches in the circuit, k denotes the number of assertions for assertion coverage or the number of lines in the code for code coverage, p stands for the length of the path in path coverage, and t is the threshold of the hit count.

8 Conclusions and Future Work We showed how work done on coverage in simulation-based veri?cation can be adapted to formal-veri?cation. We also described symbolic algorithms to compute coverage in the

Hana Chockler et al.: Coverage Metrics for Formal Veri?cation

13

formal-veri?cation setting. We have not discussed the issue of how the coverage information that the algorithm generates should be presented and used. One straightforward possibility is to simply list the parts of the design that are not covered. A better possibility, which is a subject of future research, is to develop algorithms that use this information in order to generate new speci?cations that should be checked. In simulation-based veri?cation, the choice of the most suitable coverage metrics is done individually for each application. Most researchers agree that high code coverage (almost or exactly 100%) is desirable (cf. [Pel01]). As for more complicated metrics, it is up to the designer to choose the most appropriate ones. We believe that this should also be the case in formal veri?cation. While it is (almost always) clear that the speci?cations should cover the whole code of the system, more subtle metrics are useful for hinting on unchecked parts, but high coverage is not always necessary. Clearly, coverage computation incurs costs beyond the costs already incurred by formal-veri?cation algorithms. As in simulationbased veri?cation, the use of our algorithms will be determined by practical veri?cation methodologies developed in industry. References

[AFF+ 03] R. Armon, L. Fix, A. Flaisher, O. Grumberg, N. Piterman, and M.Y. Vardi. Enhanced vacuity detection for linear temporal logic. In Computer Aided Veri?cation, Proc. 15th International Conference. Springer-Verlag, 2003. [AFG+ 02] R. Armoni, L. Fix, R. Gerth, B. Ginsburg, T. Kanza, A. Landver, S. Mador-Haim, A. Tiemeyer, E. Singerman, M.Y. Vardi, and Y. Zbar. The ForSpec temporal language: A new temporal property-speci?cation language. In Proc. 8th Int’l Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’02), Lecture Notes in Computer Science 2280, pages 296–311. Springer-Verlag, 2002. [BA82] T.A. Budd and D. Angluin. Two notions of correctness and their relation to testing. Acta Informatica, 18:31–45, 1982. [BB94] D. Beatty and R. Bryant. Formally verifying a microprocessor using a simulation methodology. In Proc. 31st Design Automation Conference, pages 596–602. IEEE Computer Society, 1994. [BBER01] I. Beer, S. Ben-David, C. Eisner, and Y. Rodeh. Ef?cient detection of vacuity in ACTL formulas. Formal Methods in System Design, 18(2):141–162, 2001. [BCM+ 92] J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, and L.J. Hwang. Symbolic model checking: 1020 states and beyond. Information and Computation, 98(2):142–170, June 1992. [BF00] L. Bening and H. Foster. Principles of veri?able RTL design – a functional coding style supporting veri?cation processes. Kluwer Academic Publishers, 2000. [BKM02] C. Boyapati, S. Khurshid, and D. Marinov. Korat: Automated testing based on java predicates. In Proc. ACM/SIGSOFT International Symposium on Software Testing and Analysys (ISSTA), pages 123–133, Rome,Italy, 2002.

J.R. B¨ chi. On a decision method in restricted secu ond order arithmetic. In Proc. Internat. Congr. Logic, Method. and Philos. Sci. 1960, pages 1–12, Stanford, 1962. Stanford University Press. [Bud81] T.A. Budd. Mutation analysis: Ideas, examples, problems, and prospects. Computer Program Testing, pages 129–148, 1981. [Cad03] Cadence. Assertion-based veri?cation. http://www.cadence.com, 2003. [CGMZ95] E.M. Clarke, O. Grumberg, K.L. McMillan, and X. Zhao. Ef?cient generation of counterexamples and witnesses in symbolic model checking. In Proc. 32nd Design Automation Conference, pages 427–432. IEEE Computer Society, 1995. [CGP99] E.M. Clarke, O. Grumberg, and D. Peled. Model Checking. MIT Press, 1999. [Cho03] H. Chockler. Coverage metrics for model checking. PhD thesis, Hebrew University, Jerusalem, Israel, 2003. [CK02] H. Chockler and O. Kupferman. Coverage of implementations by simulating speci?cations. In R.A. BaezaYates, U. Montanari, and N. Santoro, editors, Proceedings of 2nd IFIP International Conference on Theoretical Computer Science, volume 223 of IFIP Conference Proceedings, pages 409–421, Montreal, Canada, August 2002. Kluwer Academic Publishers. [CKKV01] H. Chockler, O. Kupferman, R.P. Kurshan, and M.Y. Vardi. A practical approach to coverage in model checking. In Computer Aided Veri?cation, Proc. 13th International Conference, volume 2102 of Lecture Notes in Computer Science, pages 66–78. Springer-Verlag, 2001. [CKV01] H. Chockler, O. Kupferman, and M.Y. Vardi. Coverage metrics for temporal logic model checking. In Tools and algorithms for the construction and analysis of systems, number 2031 in Lecture Notes in Computer Science, pages 528 – 542. Springer-Verlag, 2001. [Dil98] D.L. Dill. What’s between simulation and formal veri?cation? In Proc. 35st Design Automation Conference, pages 328–329. IEEE Computer Society, 1998. [DLS78] R. A. DeMillo, R. J. Lipton, and F. G. Sayward. Hints on test data selection: Help for the practicing programmer. IEEE Computer, 11(4):34–43, 1978. [FLLO95] R.S. French, M.S. Lam, J.R Levitt, and K. Olukotun. A general method for compiling event-driven simulations. In Design Automation Conference, pages 151– 156, 1995. [GL94] O. Grumberg and D.E. Long. Model checking and modular veri?cation. ACM Trans. on Programming Languages and Systems, 16(3):843–871, 1994. [HH96] R.C. Ho and M.A. Horowitz. Validation coverage analysis for complex digital designs. In International Conference on Computer Aided Design, pages 146–151, November 1996. [HHK96] R.H. Hardin, Z. Har’el, and R.P. Kurshan. COSPAN. In Computer Aided Veri?cation, Proc. 8th International Conference, volume 1102 of Lecture Notes in Computer Science, pages 423–427. Springer-Verlag, 1996. [HKHZ99] Y. Hoskote, T. Kam, P.-H Ho, and X. Zhao. Coverage estimation for symbolic model checking. In Proc. 36th Design automation conference, pages 300–305, 1999. [Hol97] G.J. Holzmann. The model checker SPIN. IEEE Trans. on Software Engineering, 23(5):279–295, May 1997. Special issue on Formal Methods in Software Practice.

[B¨ c62] u

14 [Hos95]

Hana Chockler et al.: Coverage Metrics for Formal Veri?cation

Y.V. Hoskote. Formal techniques for veri?cation of synchronous sequential circuits. PhD thesis, The University of Texas at Austin, 1995. [Kat01] S. Katz. Techniques for increasing coverage of formal veri?cation. M.Sc. Thesis, The Technion, Israel, 2001. [KGG99] S. Katz, D. Geist, and O. Grumberg. “Have I written enough properties ?” a method of comparison between speci?cation and implementation. In 10th Advanced Research Working Conference on Correct Hardware Design and Veri?cation Methods, volume 1703 of Lecture Notes in Computer Science, pages 280–297. SpringerVerlag, 1999. [KN96] M. Kantrowitz and L. Noack. I’m done simulating: Now what? veri?cation coverage analysis and correctness checking of the dec chip 21164 alpha microprocessor. In Proceedings of Design Automation Conference, pages 325–330, June 1996. [Kur97] R.P. Kurshan. Formal veri?cation in a commercial setting. In Proc. Conf. on Design Automation (DAC‘97), volume 34, pages 258–262, 1997. [Kur98] R.P. Kurshan. FormalCheck User’s Manual. Cadence Design, Inc., 1998. [KV03] O. Kupferman and M.Y. Vardi. Vacuity detection in temporal model checking. Journal on Software Tools For Technology Transfer, 4(2):224–233, February 2003. [Mar99] B. Marick. How to misuse code coverage. In Proc. 16th International Conference on Testing Computer Software (TCS), June 1999. [MP92] Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems: Speci?cation. SpringerVerlag, Berlin, January 1992. [Pel01] D. Peled. Software Reliability Methods. SpringerVerlag, 2001. [PS02] M. Purandare and F. Somenzi. Vacuum cleaning CTL formulae. In Proc. 14th Conference on Computer Aided Veri?cation, Lecture Notes in Computer Science, pages 485–499. Springer-Verlag, July 2002. [SA99] J. Shen and J.A. Abraham. An rtl abstraction technique for processor microarchitecture validation and test generation. Journal of Electronic Testing, 16(1-2):67–81, February 1999. [TK01] S. Tasiran and K. Keutzer. Coverage metrics for functional validation of hardware designs. IEEE Design and Test of Computers, 18(4):36–45, 2001. [UZ98] S. Ur and A. Ziv. Off-the-shelf vs. custom made coverage models, which is the one for you? In Proceedings of International Conference on Software Testing, Analysis, and Review, 1998. [Ver03] Verisity. Surecove’s code coverage technology. http://www.verisity.com/products/surecov.html, 2003. [VW86] M.Y. Vardi and P. Wolper. An automata-theoretic approach to automatic program veri?cation. In Proc. 1st Symp. on Logic in Computer Science, pages 332–344, Cambridge, June 1986. [VW94] M.Y. Vardi and P. Wolper. Reasoning about in?nite computations. Information and Computation, 115(1):1–37, November 1994. [ZHM97] H. Zhu, P.V. Hall, and J.R. May. Software unit test coverage and adequacy. ACM Computing Surveys, 29(4):366–427, 1997.

赞助商链接

更多相关文章：
**
英语写作 ***manuscript* form

英语写作*manuscript* form_英语学习_外语学习_教育...clear sign showing where it is to *be* *inserted*.... *Software* *Tools* *for* Tec... 暂无评价 21页 免费...**
***manuscript*

1.*Manuscript* Form 112页 1下载券 *manuscript* II...not *for* distribution (pss-logo *will* *be* *inserted* ... we calculated the charge *transfer*, atomic ...**
chapter 1 ***manuscript* *for*...

etc*should* *not* *be* used as conjunctions to link two coordinate clauses; ... including the adverbial elements placed before the subject, or *inserted* in ...**
***manuscript*

*manuscript*_基础医学_医药卫生_专业资料。不错... Switzerland) was stereotaxically *inserted* into the... *not* only the brain ISF nature *will* *be* ...
更多相关标签：

英语写作

1.

etc