>>>>> "vg" == vanessa goyal <vanessa_goyal@rediffmail.com> writes:
vg> In some cases its good to use rachability analysis step, but in
vg> some we can skip it. can you please tell us by a short example
vg> in which cases we should use this step and in which we can leave
vg> it. In short i want to ask,how does reachability analysis
vg> affects model checking.
Simplifying a bit, here is how it works. Suppose we want to model
check EF p=1. Without reachability analysis, we would start with all
the states that satisfy p=1, find their predecessors, then the
predecessors of the predecessors, and so on, until no more states can
be added. Then we check if all initial states are in the accumulated
states.
In so doing, we may trace paths back from states labeled p=1 that are
not reachable from any initial state. This is wasted work, because
tracing back from an unreachable state we cannot encounter an initial
state.
If we know what states are reachable in advance, we can trace back
from states that satisfy p=1 *and* are reachable.
Another way to use reachability information is to simplify the
transition relation. Again omitting a few details, the main idea is
that we can arbitrarily change the transitions out of unreachable
states, because this will never make an unreachable state reachable;
hence, the reachable part of the state graph, which is what counts in
deciding a property, is not affected.
The transition relation is represented by a set of BDDs, and BDD
packages have operators that try to simplify BDDs using a "care set."
The care set gives the inputs for which the simplified BDD should
produce the same output as the original BDD. VIS uses such operators
with the reachable states as care set to get smaller BDDs for the
transition relation. Smaller BDDs are usually manipulated in less
time.
It should not be hard to see that an upper bound to the reachable
states can also be used. It may miss some opportunities for
optimization, but correctness is guaranteed. (Sometimes an upper
bound works even better than the exact set, but I won't go into why
this time.)
Summarizing, reachability analysis allows VIS to narrow the search,
and to use smaller BDDs. Obviously, the advantages will vary from
example to example, because we have to search forward to help the
search backward. Whether we recoup the cost of the forward search
depends on how expensive the two steps are, and how much benefit is
there to be had from using reachability information.
Suppose all states are reachable in the given design. Then all the
effort spent in acquiring the reachable states is wasted, because
there is no pruning of the backward search, and no simplification of
the transition relation. If reachability analysis is expensive, we'll
do much worse with it. Counters provide excellent examples of this
behavior.
On the other hand, if the reachable states are a tiny fraction of all
states, and reachability analysis is relatively inexpensive, then we
can gain a lot by using it. Among the models distributed with VIS,
the "ethernet" examples are good examples of this behavior.
VIS also provides the so-called "forward model checking" algorithm (mc
-F) , in which some CTL formulae (but not all) can be decided by
forward search, rather than backward search. Forward model checking
is not always better than the standard one, but when it is better, it
is often because it combines, in a way, reachability analysis and
property checking in one search.
Fabio
This archive was generated by hypermail 2b30 : Sat Jun 02 2001 - 09:40:41 MDT