Introduction to Formal Verification
 

 


next up previous contents
Next: Formal Verification in Up: No Title Previous: Describing Designs for

Introduction to Formal Verification

 

Formal verification is the process of checking whether a design satisfies some requirements (properties). We are concerned with the formal verification of designs that may be specified hierarchically (as illustrated in the previous section); this is also consistent with how a human designer operates. In order to formally verify a design, it must first be converted into a simpler ``verifiable'' format. The design is specified as a set of interacting systems; each has a finite number of configurations, called states. States and transition between states constitute FSMs. The entire system is an FSM, which can be obtained by composing the FSMs associated with each component. Hence the first step in verification consists of obtaining a complete FSM description of the system. Given a present state (or current configuration), the next state (or successive configuration) of an FSM can be written as a function of its present state and inputs (transition function or transition relation).

We note that this entire framework is one of discrete functions. Discrete functions can be represented conveniently by BDDs (binary decision diagram; a data structure that represents boolean (2-valued) functions) and its extension MDDs (multi-valued decision diagram; a data structure that represents finite valued discrete functions). We use BDDs and MDDs to represent all quantities required in this discrete space (more specifically the transition functions, the inputs, the outputs and the states of the FSMs). For BDDs and MDDs to be efficient representations of discrete functions, a good ordering of input variables (actual inputs, outputs, state) of the functions must be computed. In general, BDDs operate on sets of points rather than individual points; this is called symbolic manipulation.

The two most popular methods for automatic formal verification are language containment and model checking. The current version of VIS emphasizes model checking, but it also offers to the user a limited form of language containment (language emptiness).

Model Checking of Temporal Logic

 

A finite state system can be represented by a labeled state transition graph, where labels of a state are the values of atomic propositions in that state (for example the values of the latches). Properties about the system are expressed as formulas in temporal logic of which the state transition system is to be a ``a model''. Model checking consists of traversing the graph of the transition system and of verifying that it satisfies the formula representing the property, i.e., the system is a model of the property.

Computation Tree Logic

 

Temporal logic expresses the ordering of events in time by means of operators that specify properties such as `` will eventually hold''. There are various versions of temporal logic. One is computational tree logic (CTL). Computation trees are derived from state transition graphs. The graph structure is unwound into an infinite tree rooted at the initial state. Fig. 3.1 shows an example of unwinding a graph into a tree. Paths in this tree represent all possible computations of the system being modeled. Formulae in CTL refer to the computation tree derived from the model. CTL is classified as a branching time logic because it has operators that describe the branching structure of this tree.

 
Figure 3.1:   Unwinding of state transition graph.

Formulae in CTL are built from atomic propositions (where each proposition corresponds to a variable in the model), standard boolean connectives of propositional logic (e.g., AND, OR, XOR, NOT), and temporal operators. Each temporal operator consists of two parts gif: a path quantifier ( or ) followed by a temporal modality (, , , ). All temporal operators are interpreted relative to an implicit ``current state''. There are in general many execution paths (sequences of state transitions) of the system starting at the current state. The path quantifier indicates whether the modality defines a property that should be true of all those possible paths (denoted by universal path quantifier ) or whether the property needs only hold on some path (denoted by existential path quantifier ). The temporal modalities describe the ordering of events in time along an execution path and have the following intuitive meaning:

  1. (reads `` holds sometime in the future'') is true of a path if there exists a state in the path where formula is true.
  2. (reads `` holds globally'') is true of a path if is true at every state in the path.
  3. (reads `` holds in the next state'') is true of a path if is true in the state reached immediately after the current state in the path.
  4. (reads `` holds until holds'', called ``strong until'' gif) is true of a path if is true in some state in the path, and holds in all preceding states.
In the VIS documentation there is a description of the syntax of CTL in the document entitled ``CTL Syntax''. In this chapter CTL formulas will be written in a simplified syntax.

The state of a system consists of the values stored in all latches. Each formula of the logic is either true or false in a given state; its truth is evaluated from the truth of its subformulas in a recursive fashion, until one reaches atomic propositions that are either true or false in a given state. A formula is satisfied by a system if it is true for all the initial states of the system. If the property does not hold, the model checker will produce a counterexample, that is an execution path that witnesses the failure. An efficient algorithm for automatic model checking used also in VIS has been described by Clarke et al. [7]. The following table shows examples of evaluations of formulas on the computation tree of Fig. 3.1:

Specification of Properties in CTL

 

Temporal logic formulas can be difficult to interpret, so that a designer may fail to understand what property has been actually verified. Therefore it is important to be familiar with the most common constructs of CTL used in hardware verification.


  1. For all reachable states (), if is asserted in the state, then always at some later point () we must reach a state where is asserted. is interpreted relative to the initial states of the system. is interpreted relative to the state where is asserted. In other words, it is always the case that if the signal is high, then eventually will also be high. A common mistake would be to write , instead of . The meaning of the former is that if is asserted in the initial state, then it is always the case that eventually we reach a state where is asserted, while the latter requires that the condition is true for any reachable state where holds. If is identically true, reduces to .

  2. From every reachable state, for all paths starting at that state we must reach another state where is asserted. In other words, must be asserted infinitely often.

  3. From any reachable state, there must exist a path starting at that state that reaches a state where is asserted. In other words, it must always be possible to reach the restart state.

  4. It is possible to get to a state where holds, but does not hold.

  5. It is always the case that if occurs, then eventually is true, and until that time, must continue to be true.

  6. Whenever goes high, will go high within two clock cycles.

  7. If it is possible for to be asserted in three consecutive states, then it is also possible to reach a state where is asserted and from there to reach in two more steps a state where is asserted.

We summarize the most common CTL templates with the corresponding English language meaning:

  1. is ``nothing bad ever happens'' ( is bad). Used to specify an invariant, i.e., a condition that must be true in all states. Helpful for partial correctness (no wrong answers are produced), mutual exclusion (no two processors are in a critical section simultaneously), deadlock freedom (no deadlock state is reached).
  2. is ``eventually the system is confined to states where is always true'' or ``the system stays out of states where is true only a finite number of times''. It can be used to specify the property of finite number of failures in the system.
  3. is ``from all reachable states where is true, something good, , eventually happens''. Helpful to express total correctness (termination eventually occurs with correct answers), accessibility (eventually a requesting process will enter its critical section), starvation freedom (eventually service will be granted to a waiting processor). If is always true, it reduces to .
  4. is ``infinitely often '', i.e., from any reachable state one must reach a state where is asserted. It can be used, for instance, to enforce a reset condition from any state.
  5. is ``something good, , eventually (or finally) happens'' (less restrictive than ).
  6. is ``always possible''. It can detect, for instance, the absence of deadlocks, by requiring that is it always possible to reach deadlock-free states. This is an example of a CTL property that cannot be represented by an -automaton gif.
  7. forces a complete traversal of the states of the system.
  8. is `` is possible''. This is another example of a CTL property that cannot be represented by an -automaton.

Caveats

  1. The variables appearing in a CTL formula must be a function of register variables (e.g., states or outputs attached to states). Variables that depend on inputs or pseudo-inputs are not allowed, since this could lead to a state where both and are true, depending on the input.
  2. The propositional logic operator , as in is equivalent to , and is satisfied by . Do not use it in place of , which is true if and only if and are both true.
  3. The syntax of CTL and of Verilog are different. For instance, we have: 

     
        Verilog CTL      meaning

        &&      *        AND
        ||      +        OR
        ==      =        equal
        a!=NO   !(a=NO)  not equal
                ->       implies
                ^        xor

Fairness Constraints

 

It is often necessary to introduce some notion of fairness. For example, if the system allocates a shared resource among several users, only those paths along which no user keeps the resource forever should be considered. CTL by itself cannot express assertions about correctness along fair paths.

Fair CTL is a modification of CTL to handle fairness. Fair CTL is characterized by the introduction of fairness constraints, which are sets of states expressed by means of CTL formulas, each giving a fairness condition; a fair path is a path along which each fairness condition is satisfied infinitely often. These types of fairness constraints are called Büchi type. More general fairness constraints, such as Street type, are not allowed currently. Fair CTL has the same syntax as CTL, but the semantics is modified so that all path quantifiers only range over fair paths. VIS supports Fair CTL; in the documentation we may sometimes refer to CTL, where we really mean Fair CTL.

An example of a fairness condition is , that restricts the system to only those paths where is asserted infinitely often.

Properties and Fairness Conditions of Traffic Light Controller in CTL

 

Not all behavior exhibited by the description of the Traffic Light Controller is valid. In order to restrict the behavior we impose the following two fairness constraints. The first is: 

!(timer.state=START);
The timer must eventually leave the START state. This constraint prevents it from staying in START forever. The second fairness constraint: 
!(timer.state=SHORT);
ensures that the timer must eventually leave the SHORT state. Liveness properties (e.g, cars on farm road and highway will eventually cross) would not pass if these fairness constraints are not placed on the timer.

One obvious property to check is that the light is not green in both directions at the same time, ensuring that collisions do not occur between traffic on the farm road and highway. This property is written as the CTL formula: 

AG ( !((farm_light = GREEN) * (hwy_light = GREEN)) );

To ensure that a car on the farm road eventually crosses the intersection, we require that if a car is present on the farm road, and the timer is long, then eventually the farm light will turn green. In CTL this is written as: 

AG(((car_present = YES) * (timer.state = LONG)) -> AF(farm_light = GREEN));

In addition, regardless of what happens on the farm road, the highway should always be green in the future: 

AG(AF(hwy_light = GREEN));

The presence of a car on the farm road does not guarantee that eventually the farm light will turn green. A car may approach, and then back away, all before the timer goes long. This property is not necessary for safety, it just maximizes the time that the highway light is green. Thus, it is desirable that the system satisfies the following property: 

!(AG((car_present = YES) -> AF(farm_light = GREEN)));

Language Containment

 

There are properties of practical interest that cannot be described in CTL. An example is the ``almost always'' property: a condition, , always holds after a finite number of transitions (note that formulas and would express this, but these are not legal CTL formulas). This property looks a lot like , but it is not the same. One can exhibit a transition system where is true, while is false.

A solution would be to use a more expressive type of temporal logic (for instance, the previous property could be expressed in PLTL or CTL*). But there would be drawbacks, such as the higher complexity of algorithms for model checking. An alternative is to use another verification paradigm, called language containment, based on the theory of -automata. For example, it is easy to express the previous ``almost always'' property using an automaton.

Currently VIS supports a restricted form of language containment. We review briefly the idea of language containment: for a system to satisfy a property it must be that , where is an -automaton representing the system, is an -automaton representing the property and is the language accepted by the automaton. It is a fact that is equivalent to .

To achieve language containment checking we represent the composition of the given system with a model representing the negation of the property and check it for language emptiness. The language of the composed system is empty if and only if the system satisfies the property .

Language emptiness is used not only to verify properties that cannot be expressed in Fair CTL, but also to check whether the abstraction of a system still contains the original system. In both cases one must complement an -automaton (), and this is hard to do if the automaton is nondeterministic (as is usually the case for an abstraction). The fact that complementation of a deterministic property is easy, while complementation of a nondeterministic property may be hard, is a key problem with language containment. This has prompted a lot of research on different classes of -automata with different expressiveness and difficulty of complementation. Currently VIS supports language emptiness of nondeterministic Büchi automata; only it is the responsibility of the user to derive the complement of a given nondeterministic property. Büchi automata acceptance conditions are states that must be reached infinitely often and they are specified by means of fairness constraints. Thus to use language containment, the user must insert in the Verilog hierarchy a monitor, which represents the complement automaton structure, and impose a set of fairness conditions to specify the complement automaton acceptance conditions, i.e., the acceptance conditions are specified in terms of fair paths.

As a final note, inside VIS, language emptiness (language containment) is reduced to CTL, by checking the CTL formula on the system (system composed with complemented property), i.e., whether there is an infinite path (notice that is always satisfied), satisfying appropriate fairness constraints.


next up previous contents
Next: Formal Verification in Up: No Title Previous: Describing Designs for


Yuji Kukimoto
Tue Feb 6 11:58:14 PST 1996
Contact 
©2002-2018 U.C. Regents