Test sequence generation and model checking using dynamic transition relations.
The task of finding a set of test sequences that provides good coverage of industrial circuits is infeasible because of the size of the circuits. For small critical subcircuits of the design, however, designers can create a set of test sequences that achieve good coverage. These sequences cannot be used on the full design because the inputs to the subcircuit may not be accessible. In this work we present an efficient test generation algorithm that receives a test sequence created for the subcircuit and finds a test sequence for the full design that reproduces the given sequence on the subcircuit. The algorithm uses a new technique called dynamic transition relations to increase its efficiency .The most common and most expensive step in our algorithm is the computation of the set of predecessors of a set of states. To make this computation more efficient we exploit a partitioning of the transition relation into a set of simpler relations. At every step we use only those that are necessary, resulting in a smaller relation than the original one. A different relation is used for each step, hence the name dynamic transition relations. The same idea can be used to improve symbolic model checking for the temporal logic CTL.We have implemented the new method in SMV and run it on several large circuits. Our experiments indicate that the new method can provide gains of up to two orders of magnitude in time and space during verification. These results show that dynamic transition relations can make it possible to verify circuits that were previously unmanageable due to their size and complexity .
Introduction
In recent years we have seen a rapid growth in the complexity and size of industrial de-
signs. The verification task of such systems has become extremely complex, requiring new
techniques that can handle large scale designs. Formal methods are an example of a new
technology that has gained popularity recently in this context. One such method, symbolic
model checking has been very successful in hardware verification. Model checkers have been
able to find several previously unknown errors in industrial circuits. Many companies are
starting to use symbolic model checking in their design cycles as a complement to dynamic
validation. We propose a new technique based on symbolic model checking called dynamic
transition relations that enhances both formal verification and dynamic validation.
Dynamic validation (or simulation) checks that a given run of a system is correct by
inputing a sequence of signals (a test sequence) to the design and observing the resulting
outputs. Since the number of runs is infinite, the method cannot be exhaustive, i.e., it
cannot check all possible runs. Thus, it is important to obtain a set of test sequences that
provides a good coverage of the design. However, this task might not be feasible if the
design is too large. Creating a set of test sequences covering most of the behaviors of the
circuit is extremely difficult due to the large number of behaviors that it can exhibit. There
are situations, however, in which a set of test sequences can be assumed to exist.
ffl It is important to test small critical sub-circuits extensively. For small circuits, it is
easier to generate efficient test sequences. For critical circuits it is worth the extra
effort to identify test sequences that can provide a good coverage.
ffl Sub-circuits are frequently reused in new designs, and in these cases test sequences
often have been developed for them.
ffl Sub-circuits can also be verified separately (using simulation or formal methods, for
example). If an error is found in a sub-circuit the designer must check if it is a real
error. It may not exist in the full design because the sequence of inputs that lead to
the error can never occur in the complete circuit.
ffl Important conditions in the full design can often be stated as test sequences. For
example, the violation of mutual exclusion can be stated as a condition on internal
signals (e.g. granted 0 - granted 1 ), which can be seen as a test sequence of length one.
However, test sequences for sub-circuits cannot be used directly in the full system. The
inputs to the sub-circuit can be internal signals of the full circuit which may not be accessible
from the exterior of the design. We address the problem of creating a test sequence for the
full design that will reproduce the test sequence of the small sub-circuit and thus achieve
good coverage of the sub-circuit by running tests on the full design.
The problem can be defined as follows (see figure 1). Let D be a large design with a
set of inputs I, and let Sub be some relatively small critical sub-circuit of D, with a set
of inputs I sub . D is a single clock synchronous circuit, or an equivalently transformed one.
Assume that the designer produces a set of test sequences that guarantees a good coverage
I
interior parts
of the design sub
The design D
I

Figure

1: A schematic view of the test generation problem
of Sub. In general, the inputs to Sub are not accessible from the exterior of D. Thus, we
need to provide a test generation algorithm that given a test sequence \Pi
on I sub , either produces a test sequence \Pi on I that induces \Pi sub , or reports that no such
sequence exists. In the latter case, it means that \Pi sub can never occur when Sub is run
within D.
Our test generation algorithm performs this task in two phases. The first is a backwards
search on D that creates a sequence of sets of states in reverse order, from last to first. Any
computation path that goes through these sets induces the required \Pi sub . The second phase
traverses the sets from first to last determining one such path by choosing an appropriate
state from each set of states. A sequence of inputs \Pi that corresponds to the chosen path is
then projected from the path. The resulting \Pi is a correct input for a simulation tool that
will reproduce \Pi sub . If there is no such path, the algorithm returns "false".
Dynamic Transition Relations
The main operator in the backwards search of our algorithm is P red(A), which computes
the set of all predecessors of the states in A. A state is defined as an assignment of values
(valuation) to all variables in the model. A variable is the output of a latch or any state
holding signal in the circuit in addition to its inputs. P red(A) uses as a model for D a
transition relation defining the value of system variables in the next state as a formula on
the value of system variables in the current state. This operation might be very costly if the
transition relation is large. To avoid this problem, we exploit a partition of the transition
relation into simpler relations. Each such relation defines the value in the next state for a
single system variable. In computing the predecessors of A we apply only those relations that
define the next value for variables on which A depends. Thus, the transition relation used in
the backwards search is determined dynamically for each application of P red, according to
the set it is applied to. The new dynamic operator is called P redD . As the search proceeds,
the number of variables A i depends on may grow larger or smaller, and the sizes of the
dynamic transition relations vary accordingly. The search applied in the second phase uses
at each step the transition relation determined dynamically during the backwards search.
P redD is particularly useful if the algorithm is implemented symbolically, using a BDD [2]
representation of the design. BDDs can often provide very concise representations. How-
ever, their size tend to grow with the number of variables they depend on. But the next
value of each variable typically depends on a small number of other variables, and so each
of the dynamic transition relations will involve fewer variables than the global transition
relation. As a result, the BDD representations will often be smaller and the computation
of P redD faster.
Dynamic Transition Relations and Model Checking
The introduction of dynamic transition relations and the P redD operator has been motivated
by the test-generation algorithm that depends on it. However, the operation of finding the
set of predecessors of a set is also the core operation in other algorithms that manipulate
finite-state machines. The most prominent example is in Model Checking where a finite-state
machine that models a system is checked against a given specification to prove that it
works correctly or find a counterexample. We show that the same idea of dynamic transition
relations can be used in order to improve symbolic model checking [3] for the temporal logic
CTL.
Similarly to the test generation algorithm, one of the most common and most expensive
steps in symbolic model checking algorithms is the computation of P red (usually referred
to by the temporal operator EX). Replacing P red by P redD reduces space and time consumption
and allows the verification of larger systems. As before, the partial transition
relations are computed dynamically for each application of P redD . Note that, the result of
our computation is exact, i.e., we obtain the same set of states as we would have if we used
the global transition relation. Our changes only affect some of the intermediate results.
The method proposed has several advantages. As opposed to several algorithms frequently
used for test sequence generation, dynamic transition relations guarantee that test
sequences will be found when they exist. Also, the gains obtained by using as little of
the model as possible are automatic, there is no need to manually decide which signals to
consider and which not. It can potentially never consider large parts of the circuit, if they
do not affect the behavior of the sub-circuit under consideration. Because of this it can
be applied to much larger circuits than most other methods. Moreover, the method only
changes the P red function, not affecting the behavior of the tool in any other way. As a
consequence, it can be applied in addition to most other optimizations such as partitioned
transition relations, assume-guarantee and others for even better results.
Experimental Results
We have implemented dynamic transition relations and the test sequence generation algorithm
within the symbolic model checking tool SMV [13]. We have obtained a significant
improvement in time and space on a variety of examples such as the PCI local bus [4], a
distributed heterogeneous real-time system [5] (for model checking) and test sequence generation
for several Intel circuits. The new algorithm ran an average of 20 times faster than
the original (static) one (with a maximum speedup of 50 times) and using only 1.6% of the
memory. Moreover, our algorithm has been able to determine test sequences (or show that
they do not exist) in many cases when the static algorithm was unable to do so. The static
algorithm in these cases used more than 800M of memory and could not finish. The dynamic
algorithm, on the other hand, finished on average in 16 seconds using 5.1M of memory.
These results show that dynamic transition relations can provide significant gains for
both test sequence generation and symbolic model checking. It can enable the analysis of
larger systems than previously possible: In some cases we have been able to complete the
analysis 50 times faster with a savings of more than 200 times in memory. The fact that it
changes only the P red function enables its use with minimal changes in several verifiers.
Related Work
Test sequence generation from precomputed tests has been studied out of the context of
symbolic model checking [14, 6, 12, 11, 15, 10]. However, all of these techniques depend on
the internal structure of the circuit being tested, (e.g. in some cases they rely on a regular
bus structure in the design), and consequently are not as general as the one presented here.
In the context of model checking the problem has been addressed in [9]. But their work is
concerned mostly with expressing the test sequence and not with the complexity of dealing
with large circuits. In fact, in [9] the authors state that they have only used the method
in small examples. Another work relating to model checking and test sequence generation
is [1]. However, in that work ATPG algorithms (Automatic Test Pattern Generation) are
used to perform model checking, and ATPG algorithms do not guarantee that they will
eventually find a test sequence even in cases when it does exist.
One important aspect of our work is that is does not build a model of the complete
circuit beforehand and that it may never actually construct such model. In this aspect it
relates to techniques such as partitioned transition relations [7]. It differs from it, however,
because in that case all partitions are used in every iteration, and this may not be necessary.
Examples of techniques that may not consider all parts of the circuit are the cone of influence
reduction [7]. However, these techniques are static in the sense that they determine only
once which parts of the circuit can be ignored. Our method does it dynamically taking
advantage that not all parts of the circuit are relevant during all iterations. Because of
this our method produces better results, since it can use less of the circuit during most
iterations. In fact, the cone of influence can be seen as an upper bound on the behavior of
our algorithm.
Our paper is organized as follows. Section 2 first presents our test generation algorithm,
using a global transition relation. It then shows how to convert the test generation algorithm
to use dynamic transition relations, and explains how this algorithm can be implemented
with BDDs. Next, in Section 3 we show how dynamic transition relations are used for
model checking. In Section 4 we present experimental results that show the usefulness
of our ideas. Finally, section 5 gives our conclusions from this work and some future
directions of research.
Test Sequence generation
We model synchronous hardware designs as finite state machines. Let I sub be the set of
inputs to the sub-circuit and I be the set of circuit input variables, and let V be the set of
circuit variables that are not inputs, I sub ' I [ V . We assume that all circuit variables are
boolean.
We use boolean formulas to represent sets of states and transition relations. Each state
in the finite state machine representing a circuit is an assignment of values to all variables in
represents the set of states (assignments) that
satisfy f . A transition relation is represented by a formula R with
so that an assignment that satisfies R represents an edge from (I; V ) to We use the
same letter for a set of states (or transition relation) and the formula that represents it.
A finite state machine modeling a circuit is a tuple
ffl The set of states S is a set of valuations for I [ V .
ffl Init ' S is the set of initial states.
ffl The transition relation is defined by a set of functions N i , each defining the next-state
value for
The global transition relation is
We assume that every N i is a deterministic total function. Note that the
inputs are unrestricted.
A trace of M is a sequence
be a set of variables. A partial assignment with respect to U is an assignment that gives
values only to variables in U (as opposed to a state, which is an assignment that gives values
to all the variables of the circuit). A partial assignment oe with respect to U represents the
set of states s that agree with oe on U , i.e. for every v 2 U , oe(v). The projection of
a state s on U is a partial assignment over U that agrees with s. The projection of \Pi on
U is the trace obtained by taking the projection of each state in \Pi on U . An expansion of
oe to U 0 (s.t. U ae U 0 ) is a partial assignment oe 0 over U 0 that agrees with oe on U . A test
sequence over U is a series of partial assignments over U .
Formally, our problem is defined as follows. Given a set I sub of variables from I [ V ,
which are the inputs to the critical sub-circuit Sub, and a test sequence \Pi
over I sub , we must produce an initial state s init 2 S and a test sequence \Pi in = in m
where every in i is a partial assignment over I. Let
be the trace generated by \Pi in in M from s init We require that the
projection of s I sub will be identical to \Pi sub .
1 Notice that the transition relation R defines the next-state value for variables in V . By choosing a next-state
value for the inputs we deterministically define a successor state. Therefore, s init and \Pi in (together
with R) uniquely determine \Pi.
2.1 A Basic Static Algorithm
In this section we present an algorithm that uses the global transition relation R to determine
a test sequence for the circuit. The algorithm has two stages. The first is a backwards search
that creates a series of sets of states. Any computation path that goes through these sets
(starting at an initial state) is a solution to our problem. Given \Pi
construct a series of sets of states Am in reverse order, i.e. we start by
computing the set A n and end with Am . For every 1), every state s 2 A i has
a successor in A i+1 (see figure 2). Using a slight abuse of notation, we view every t i in the
test sequence as a set of states, the set of states (assignments to all variables) that agree
with t i . When creating the sets A 0 we make sure that A i ' t i . Thus, A 0
represent the set of traces that agree with \Pi sub . In order to make sure that a trace that
runs through these sets can be created starting at an initial state, we continue to compute
\Gamma2 and so on, until we arrive at a set Am in which there is an initial state. If such
an initial state can be found, we know that there is a trace \Pi that, from some point on,
reproduces the test sequence \Pi sub . If, however, we arrive at a set A
we can conclude that there is no input sequence \Pi in that can be used from an initial state
to reproduce \Pi, and we report this.
In the second stage we traverse the sets, from Am up to A n and find one suitable trace
. The test sequence \Pi in that generates this trace is created by taking the
projections of the states along \Pi on I. The output of the algorithm is an initial state s m ,
and a sequence of inputs in m
This algorithm uses the operator P red, which computes the set of predecessors of a
set of states A according to the transition relation R. It is defined by: P
This can be informally interpreted as there exists a state
(an assignment to I true), and this state is the end of a
transition in R (R(I; V; I Once an assignment to I
all of its predecessors, expressed in terms of I; V [13]. It also uses the function
choose(A), which receives a set A and produces a single state (assignment to I [
and the function succ(s), which returns the set of successors of a state according to R.
Stage I:
1: A n := t n
2: for do
3: A j := t
4: endfor
5: All := ;
while do
7: All := All [ A j
8:
10: endwhile
Stage II:
13: print "sequence generation failed"
14: else
in m := the projection of s m on I;
17: for to n do
19: in j := the projection of s j on I;
20: endfor
sm
Init
Rn

Figure

2: The data structure created by the test sequence generation algorithm
2.2 Dynamic Transition Relations: A More Efficient Algorithm
The algorithm presented in the previous section might not be practical for very large circuits.
In such circuits, the transition relation R is too big even if it is represented by a BDD. As
a result, for a set of states A the operation P red becomes too expensive.
It is possible, however, to exploit a partition of the transition relation into functions N i
that define the next state variables v 0
. Recall that a state of our model gives values to all
the variables in I [ V . We say that a set of states A is independent of a variable v i , if for
every state s in A, the state that differs from s only on v i is also in A. In such a case, we
can exclude the function N i from the computation of P red(A). We say that a formula f
is independent of a variable v if for every two assignments oe and oe 0 that differ only on v,
oe . Notice that if the formula f is independent of v then the set of states
that it represents is independent of v.
Let f be a formula (representing a set of states or a transition relation), and let the
support of f be the set of variables on which f depends. We define
f depends on vg and sup 0 depends on v 0 g. Therefore, sup(f) is the
set of current-state variables that f depends on and sup 0 (f) is the set of next-state variables
that f depends on.
We define a dynamic version of P red, called P redD . The operator
the set of predecessors of states in A according to the partial transition relation
i ], which is a transition relation that includes N i if and only if A depends
on v i . The operator P redD is therefore defined as: P redD
Lemma 1 For any set A, P
Proof: Assume that the variable v i does not appear in the support of A. We start with the
definition of P red:
(v 0
does not depend on v i , A(V 0 ) does not depend on v 0
i and we can move it through
the 9v 0
i quantifier to get:
(v 0
We assume that every N i is a total function, i.e. for every V there exists v 0
so:
(v 0
The above shows that for every variable v i that does not appear in the support of A we
can drop the term v 0
from the transition relation part of P red(A) without changing
the result. If we do this for all variables not in the support of A we get P redD (A). 2
If the next-state value of each variable depends only on a few of the other variables (as
is often the case in circuits), the support of the sets we compute will remain small.
We recall that given a state s, the application of R to s determines the next-state values
for the variables in V , but not for the variables in I. The input variables I are chosen
arbitrarily by the environment. The dynamic algorithm uses partial assignments oe i instead
of the full states s i , and partial transition relations R i instead of R. The output sequence
in generated by the algorithm is a series of partial assignments over
some (but perhaps not all) of the variables in I. When in i does not give a value for a
variable v 2 I it means that v does not influence the parts of the circuit that are being
considered, and its value can be chosen arbitrarily.
In the dynamic algorithm we use the following functions:
ffl choose(A; U) accepts a set of states represented by a formula A and a set of variables
U such that sup(A) ' U . It returns a partial assignment oe over U that satisfies A.
If we view oe and A as sets, then the chosen oe is a subset of A. Notice that if A is
given as a partial assignment a, then the resulting oe will be an assignment over U that
agrees with a. Notice also that the function choose that was used in the algorithm of
the previous subsection is just a call to this function with
receives a partial assignment oe over some set of variables U , and a set
of variables U 0 ' U . It expands oe to create a partial assignment over U 0 . The values
for variables in U 0 n U are chosen arbitrarily.
ffl project(s; U) receives a state and a set of variables and returns the projection of the
former on the later, i.e. it returns a partial assignment over U that agrees with s.
receives a partial transition relation R i and a partial assignment oe over
The partial transition relation is of the form R
some set of variables U . The result is a partial assignment oe 0 over U , such that for
every
Stage I:
1: A n := t n
2: for do
3: R j+1 := V
4: A j := t
5: endfor
7: while do
8: All := All [ A j
12: endwhile
Stage II:
14: if
15: print "sequence generation failed"
else
23: in j := choose(oe
24: endfor
26: in n := choose(oe n ; I)
27: endif
Stage I of the algorithm creates the same sets Am that were created in the
previous algorithm, but uses P redD instead of P red. Notice that by the end of stage I we
have that for every
the use of expand in lines 18,22 and apply in lines 21,25.
In stage II, the forward search for a path through the A i 's is done using partial assignments
instead of states (which are full assignments). Every partial assignment
oe i represents a set of states which differ only on variables not in the support of A i . When
moving from oe i\Gamma1 to oe i , in lines 21 and 25, we use the same partial transition relation R i that
was used to create A i\Gamma1 from A i (see figure 2). After applying R i , we expand the result to
the support of R i+1 (line 22) so that we can apply R i+1 in the next iteration of the loop. The
output of the algorithm is the initial state s init and the inputs in . The inputs
calculated by the algorithm do not necessarily give values to all input variables in I. When
giving inputs to a simulation we need to decide on values for all the input variables. We
therefore expand every in i to I by choosing arbitrary values for the extra input variables.
The following theorems state the correctness of the dynamic algorithm. Their proofs are
omitted for brevity, but can be found in the full paper.
Theorem 2.1: Assume the test generation algorithm returns "false". Then no computation
of D produces t
Theorem 2.2: Assume the test generation algorithm returns an initial state s init and a
sequence of inputs in be the computation generated when
running a simulation using s init and in in n\Gamma1 as inputs. Then,
2.3 BDD implementation
The algorithm can easily be implemented using BDD representations. The components
Init, S and N l of the model are represented using BDDs in the usual manner. In
addition, the sets A j computed by our algorithm are represented by BDDs. The input to
the algorithm is a sequence of binary vectors over T . It is straight forward to translate
each vector into a BDD that represents the set t i needed for the algorithm. Most BDD
libraries include a function to compute sup and sup 0 , which are simply the sets of current
or next state variables that appear in the BDD. All other operations used in our algorithm
are standard BDD operations.
A BDD implementation of the algorithm will mostly benefit from the use of partial
transition relations. The size of a BDD representing a set A is generally related to the
size of sup(A). In many cases, each N i will not depend on all the variables in I [ V .
Thus, taking fewer N i 's will result in a smaller support for the partial transition relation
As a result, the BDDs computed at intermediate stages in the
computation of P red using the partial transition relation will depend on less variables and
therefore will often be smaller.
3 Symbolic Model Checking
3.1 Model checking using dynamic transition relations
Model checking is the problem of finding the set of states in a finite-state machine where a
given temporal formula is true. One of the most efficient approaches for solving this problem
is a symbolic algorithm that uses BDDs [2] for representing the transition relation. This
representation is often very concise, allowing the verification of large and complex systems.
Verification is performed by an efficient search algorithm. The core of the algorithm is the
temporal operator EX, which given a model M and a set of states A, both represented by
BDDs, determines the set of predecessors of states in A.
The EX operator is part of the temporal logic CTL (Computation Tree Logic [8]), frequently
used in model checkers. Formulas in CTL express properties of states in the system.
They are built from atomic propositions, boolean connectives and temporal operators. Each
operator consists of two parts: a path quantifier followed by a temporal modality. Path
quantifiers indicate that the property should be true of all paths starting on a given state
(A), or some path from a given state (E). Temporal modalities describe how events should
be ordered with respect to time along a path specified by the path quantifier. For example,
means that p holds in the next state; F p means that p holds in some future state;
G p means that p holds in all states on the path. Some common CTL operators are: AG
p which is true at a state if p is globally true in all paths from the current state, i.e., p is
an invariant; EF p, which is true if p holds sometime in the future for some path, i.e., p is
reachable.
We demonstrate how the symbolic model checking algorithm works by showing the
algorithm for EF p. The algorithm for the other temporal operators are similar in nature.
The object is to construct a BDD that represents the set of all states that satisfy EF p.
The algorithm starts with the BDD A for the states that satisfy p. At each step, we add to
A the set of its predecessors which is computed by EX A. The algorithm terminates when
no more states can be added to A.
The most expensive computation step in the above algorithm is the application of the
EX operator. We notice that the EX operator is exactly the P red operator that was defined
in the previous section. We therefore replace the computation of EX by the operator P redD
that uses a partial transition relation. Like before, we compute the partial transition relation
dynamically according to the set to which EX is applied. As before, we assume that each N i
is defined over a small number of (unprimed) variables. Thus, by referring to the smallest
number of N i 's, the resulting set of states will depend on small number of variable.
The same treatment also handles model checking for Fair-CTL which is the logic CTL,
extended with fairness constraints that restrict the set of paths in the model which are
required to satisfy a given formula [8, 3].
4 Implementation and Experimental Results
We have implemented the dynamic transition relations method in SMV [13]. We have tested
our method on models that have already been verified by SMV such as the PCI local bus [4].
In addition, we have applied our method to several large Intel circuits. The table below
summarizes the results obtained for the following examples:
ffl #1. A simplified cache coherence protocol derived from the PCI Local bus;
ffl #2. The model of the PCI Local bus discussed in [4];
ffl #3 to #10 Circuits from Intel.
In the first two examples we have applied model checking, while in the other ones we have
computed test sequences. Some examples have more than one result because they have been
run with different parameters such as different length of test sequences, different width of
test vectors and different inputs to the sub-circuit.
Times are given in seconds (unless otherwise stated) and measures of space are given
in megabytes. The "Dyn." columns relate to the dynamic transition relations algorithms,
while the "St." columns relate to the static algorithm using all of the circuit. The "Vec."
column is the sub-circuit input vector width. The "Seq." column shows the length of the test
sequence for the sub-circuit. The columns for number of variables used and total number of
variables represent respectively the maximum number of variables in the support sets of the
set of states considered at each iteration and the total number of variables in the circuit.
The last column indicates if the algorithm has determined a test sequence (Successful) or if
such a sequence does not exist (Fail).
We have run 19 different tests, eleven of which were successful in determining test se-
quences, six that reported that the test sequences for the sub-circuits were unreachable and
two model checking examples. Twelve examples finished executing in both the dynamic
and static algorithms. From these twelve we have obtained an average speedup of about 20
times 2 . Memory usage has been only 1.6% of the original, a gain of more than times.
The examples that only finished with dynamic transition relations executed on average for
seconds using only 5.1M of memory. During experiments we killed a process whenever
it used all of the memory available, 800M. From this we can conclude that in these examples
we have obtained a gain in memory consumption greater than 150 times (800/5.1). Another
important result that can be derived from this table is that on average the algorithm had
to consider only about 25% of the variables in the circuit description.
As expected, the new algorithms are better suited for large examples. In the smallest
ones (the first three), the gains were not impressive. This happens because it is necessary
to reconstruct the transition relation at each iteration, which in small examples may take
more time and space (due to intermediate computations) than simply creating a transition
relation for the complete circuit.
2 The numbers in the table have been rounded, but the averages have been computed from the correct
numbers.
# Time Space Vec. Seq. # Variables S/F
Dyn. St. Dyn. St. used total
73 2301 2.5 595 8 5

Figure

3: Experimental Results
Example number five, however, is puzzling, since its gains are clearly below the average
for the medium and large examples. Even by saving significantly on the number of variables
(17 out of 90) we still need more space (even though less time) to complete the test sequence
generation. This indicates that the method can be more efficient for some types of circuits
than others. Future work includes the characterization of which are the "good" circuits and
which are the "bad" ones.
These results show that the dynamic transition relations method can provide significant
gains in verification time and space, in some cases up to two orders of magnitude. As
expected, it does not work in the same way for all kinds of circuits, but our experiments
seem to indicate that it works extremely well for several types of circuits that are used in
industry today.
Conclusions
We have presented two major results in this paper. The first is an efficient test-generation
algorithm which enables designers to translate test sequences they have created for small
sub-circuits into test sequences for the full design. This algorithm guarantees that a test
sequence will be found if it exists. The second is the introduction of dynamic transition
relations which enhance the operation of finding a set of predecessors. This operation is the
source of state-explosion in both our test-generation algorithm and symbolic model checking
algorithms and any improvement in its efficiency can prove very useful.
We have implemented the new method in SMV and run it on several large circuits.
Our experiments indicate that the new method can provide gains in time and space during
verification of up to two orders of magnitude. These results show that dynamic transition
relations can make it possible to verify circuits that were previously unmanageable due to
their size and complexity.
This work can be extended in several ways. One inefficiency of the method is that it
recreates the transition relation at each iteration. However, there may be cases in which
the same transition relation has already been constructed. An optimization consists of
implementing an algorithm that reuses previously used transition relations.
Another extension is to apply the idea of dynamic transition relations to other operators
besides P red. In symbolic model checking the P red operator is called EX, and its dual
operator is AX. Given a set A, the operator AX A computes the set of states for which all
successors are in A. It is easy to show that the same idea can be applied to this operator.
Another direction we plan to pursue is to deal with an asynchronous model of com-
putation. In this model the verified system is either an asynchronous hardware design or
a distributed program, and is represented by a set of processes. At each step one of the
processes is chosen and executed. The transition relation of such a model is a disjunction of
relations, rather than a conjunction as in the synchronous case. We plan to adjust both the
test-generation algorithm and the dynamic version of P red to this computational model.
A forward search algorithm can also be defined using dynamic transition relations. As
before, we determine which transition relations to use according to the support of the set on
which we are operating. This time, however, we choose the N i 's according to their current
state support, and not the next state support. Unfortunately, in this case we may take
into account states which are not necessarily reachable, because a transition in N i may
conflict with another transition in N j and therefore not exist in the global model. However,
if variable v i is in the support set of the states under consideration but not v j the dynamic
transition relations algorithm would allow the transition of N i to be taken, identifying
unreachable states as reachable. However, in model checking the set of reachable states can
be used to simplify the model before verification (e.g. only traverse reachable states), and in
this case an upper approximation does not introduce errors, but can speed up verification.



--R

Model checking based on sequential ATPG.

Symbolic model checking: 10 20 states and beyond.
Verifying the performance of the PCI local bus using symbolic techniques.
Selective quantitative analysis and interval model checking: verifying different facets of a system.

Model Checking.
Automatic verification of finite-state concurrent systems using temporal logic specifications
Test generation for intelligent networks using model check- ing
A testability strategy for silicon computers.
An architectural level test generator for a hierarchical design environ- ment
An architectural level test generator for a hierarchical design environment based on nonlinear equation solving.
Symbolic Model Checking: An Approach to the State Explosion Problem.
Hierarchical Testing using Precomputed Tests for Modules.
Multiple path sensitization for hierarchical circuit testing.
--TR
symbolic model checking;binary decision diagrams;test sequence generation