Next: Formal Verification in Up: No Title Previous: Describing Designs for
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).
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.
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.
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 : 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:
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. .
The following table shows examples of evaluations of formulas
on the computation tree of Fig. 3.1:
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.
We summarize the most common CTL templates with the corresponding English language meaning:
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.
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)));
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: Formal Verification in Up: No Title Previous: Describing Designs for
Tue Feb 6 11:58:14 PST 1996
|©2002-2018 U.C. Regents|