U.S. patent application number 10/666619 was filed with the patent office on 2004-04-01 for symbolic model checking with dynamic model pruning.
Invention is credited to Yang, Jin.
Application Number | 20040064794 10/666619 |
Document ID | / |
Family ID | 29270973 |
Filed Date | 2004-04-01 |
United States Patent
Application |
20040064794 |
Kind Code |
A1 |
Yang, Jin |
April 1, 2004 |
Symbolic model checking with dynamic model pruning
Abstract
Formal verification methods provide for improved efficiency of
popular binary decision diagram (BDD) based algorithms. A lazy
pre-image computation method builds new transition relation
partitions on-demand for relevant internal variables of a state
predicate, and conjoins only next state relations for relevant
internal variables to a pre-image including the state predicate. A
lazy fixpoint computation method makes iterative use of lazy
pre-image computation to compute conditions that must be satisfied
to produce a given set of states. A forward assumption propagation
method generates assumptions to characterize a set of interesting
states for a property being evaluated at one or more evaluation
stages. A dynamic transition relation reduction improves the
efficiency for symbolic model checking by reducing transition
relations under assumptions dynamically generated from properties
being evaluated. These methods provide symbolic model checking of
circuits and other finite state systems previously too large to be
completed successfully using BDD based algorithms.
Inventors: |
Yang, Jin; (Portland,
OR) |
Correspondence
Address: |
Lawrence M. Mennemeier
BLAKELY, SOKOLOFF, TAYLOR & ZAFMAN LLP
Seventh Floor
12400 Wilshire Boulevard
Los Angeles
CA
90025-1030
US
|
Family ID: |
29270973 |
Appl. No.: |
10/666619 |
Filed: |
September 17, 2003 |
Related U.S. Patent Documents
|
|
|
|
|
|
Application
Number |
Filing Date |
Patent Number |
|
|
10666619 |
Sep 17, 2003 |
|
|
|
09677262 |
Sep 30, 2000 |
|
|
|
6643827 |
|
|
|
|
Current U.S.
Class: |
716/103 ;
716/106 |
Current CPC
Class: |
G06F 30/3323
20200101 |
Class at
Publication: |
716/002 |
International
Class: |
G06F 017/50 |
Claims
What is claimed is:
1. A computer software product having one or more recordable medium
having executable instructions stored thereon which, when executed
by a processing device, causes the processing device to: generate,
from a first property, a first assumption including a first state
predicate; generate, for a model, a first transition relation that
includes the first state predicate; and reduce the first transition
relation according to the first assumption.
2. The computer software product recited in claim 1 wherein
reducing the first transition relation reduces the size of the
model.
3. The computer software product recited in claim 1 wherein
reducing the first transition relation reduces the computational
complexity of evaluating the first property.
4. The computer software product recited in claim 1 wherein
reducing the first transition relation reduces the number of
variables in the model.
5. The computer software product recited in claim 1 wherein
reducing the first transition relation reduces the number of
variables in the first transition relation.
6. The computer software product recited in claim 1 wherein the
first assumption is generated from an implication structure of the
first property.
7. The computer software product recited in claim 6 which, when
executed by a processing device, further causes the processing
device to: propagate the first assumption to generate a second
assumption according to a second property.
8. The computer software product recited in claim 7 wherein the
second property is a sub-property of the first property.
9. The computer software product recited in claim 7 wherein the
second property is to be evaluated under the first assumption.
10. The computer software product recited in claim 7 wherein the
first assumption is propagated only one transition stage to
generate the second assumption.
11. A verification system comprising: means for producing, from a
first property, a first assumption including a first state
predicate; and means for producing a reduced next state function
from a first next state function involving the first state
predicate by applying the first assumption.
12. The verification system of claim 11 wherein the first
assumption is produced from the structure of the first
property.
13. The verification system of claim 12 further comprising: means
for propagating the first assumption according to a second property
to generate a second assumption; and means for producing, for a
model, a transition relation that includes the reduced next state
function.
14. The verification system of claim 13 wherein the second property
is a sub-property of the first property.
15. The verification system of claim 14 wherein the first
assumption is propagated only one transition stage to generate the
second assumption.
16. A verification system comprising: a recordable medium to store
executable instructions; a processing device to execute executable
instruction; and a plurality of executable instructions to cause
the processing device to: produce, from a first property, a first
assumption including a first state predicate; produce, for a model,
a first transition relation that includes the first state
predicate; and reduce the first transition relation according to
the first assumption.
17. The verification system of claim 16 wherein the first
assumption is produced from the logical structure of the first
property.
18. The verification system recited in claim 17, the plurality of
executable instructions further comprising instructions to cause
the processing device to: propagate the first assumption to
generate a second assumption according to a second state
predicate.
19. The computer software product recited in claim 18 wherein the
second property is a sub-property of the first property.
Description
RELATED APPLICATIONS
[0001] This is a continuation of application Ser. No. 09/677,262
filed Sep. 30, 2000, which is currently pending.
FIELD OF THE INVENTION
[0002] This invention relates generally to automated design
verification, and in particular to more efficient use of binary
decision diagrams to perform automated symbolic model checking for
very large scale integrated circuit designs and other finite state
systems.
BACKGROUND OF THE INVENTION
[0003] Modern design of very large-scale integrated circuits often
involves years of research and the efforts of hundreds of
engineers. Automated formal verification methods are an essential
part of the design effort, reducing errors, lost time and risk to
financial investment. Formal verification involves building a
finite model of a system as a set of states and state transitions
and checking that a desired property holds in the model. An
exhaustive search of all possible states of the model may be
performed in order to verify a desired property.
[0004] As the size and complexity of designs increase, much effort
is expended to improve the efficiency of automated formal
verification methods. One technique used in symbolic model checking
to improve efficiency is to employ binary decision diagrams (BDDs).
A BDD is a directed acyclic graph that represents a Boolean
expression. For each Boolean variable, there are two outgoing edges
representing true or false assignments to the variable. The use of
BDDs permits computation times, which are some polynomial function
of the number of expression variables. Alternative representations
such as clauses or truth tables require execution times, which are
some exponential function of the number of expression variables.
Therefore, use of BDDs has been popular in the formal verification
community since the late 1980's.
[0005] BDDs, however, are not without drawbacks. The ordering of
variables is critical to an efficient use of BDDs. Poor variable
ordering can increase a BDDs size and cause exponential execution
times. One method for symbolic model checking using BDDs comes from
Carnegie Mellon University and is known as Symbolic Model Verifier
(SMV).
[0006] Alternatively SMV uses a well known heuristic based
procedure named simplify_assuming that is aimed at reducing BDD
representations by simplifying a predicate using an invariant
assumption but introduces a proof obligation, which must also be
verified. Since the assumption is static it may also be ineffective
in pruning a model.
[0007] Over the years, techniques have been developed to improve
performance and capacity of BDD-based algorithms. One technique is
called Cone of Influence (COI) reduction. In COI reduction, an
abstraction is built for a circuit model consisting of next state
functions only for variables in the dependency closure of variables
of interest in the circuit specification. One drawback is that all
variables in the dependency closure do not necessarily influence
the variables of interest in the circuit specification. A second
drawback is that the abstraction that is built and used for each
model-checking step may include portions that are useful in only a
few of the model checking steps. Therefore needless extra
computations are potentially performed, resulting in little benefit
to the circuit verification.
[0008] Some methods have attempted to improve upon COI reduction by
starting from a small portion of the dependency closure and
extending the portion only when model checking fails to produce a
satisfactory result. But these techniques also perform unnecessary
computations on portions that are not relevant to the particular
model-checking step being performed.
[0009] One method called the bounded cone of influence (BCOI) was
proposed by A. Biere et al for symbolic model checking without BDDs
[A. Biere, E. Clark, R. Raimi, and Y. Zhu; Verifying safety
properties of a PowerPC.TM. microprocessor using symbolic model
checking without BDDs; CAV'99; 1999]. However, even the BCOI method
potentially includes irrelevant variables in the abstraction it
builds, and the technique is not applicable to improve the widely
used BDD-based approaches.
BRIEF DESCRIPTION OF THE DRAWINGS
[0010] The present invention is illustrated by way of example and
not limitation in the figures of the accompanying drawings.
[0011] FIG. 1 illustrates an example of a circuit.
[0012] FIG. 2a graphically illustrates a transition relation for a
circuit.
[0013] FIG. 2b shows another transition relation built as part of a
lazy pre-image computation.
[0014] FIG. 3a illustrates one embodiment of a method for
performing lazy pre-image computations.
[0015] FIG. 3b illustrates one embodiment of a more detailed method
for performing lazy pre-image computations.
[0016] FIG. 4a illustrates one embodiment of a method for computing
a fixpoint using lazy pre-image computations.
[0017] FIG. 4b shows an example of a lazy fixpoint computation for
a circuit.
[0018] FIG. 5a illustrates a parsing of a property to be
evaluated.
[0019] FIG. 5b. illustrates one embodiment of a method for
producing and propagating assumptions from sub-properties to be
evaluated.
[0020] FIG. 5c. shows an example of producing and propagating
assumptions from sub-properties to be evaluated.
[0021] FIG. 6a graphically illustrates the state space of a model
with its transition relation built using lazy pre-image
computations to evaluate sub-property 530.
[0022] FIG. 6b graphically illustrates the state space of a
dynamically pruned model with its transition relation built using
lazy pre-image computations to evaluate sub-property 531 under
assumption 541.
[0023] FIG. 6c graphically illustrates the state space of a
dynamically pruned model with its transition relation built using
lazy pre-image computations to evaluate sub-property 532 under
assumption 542.
[0024] FIG. 6d graphically illustrates the state space of a
dynamically pruned model with its transition relation built using
lazy pre-image computations to evaluate sub-property 533 under
assumption 543.
[0025] FIG. 7a illustrates one embodiment of a method for
dynamically pruning a model by producing and propagating
assumptions from sub-properties to be evaluated and pruning the
transition relation under the assumptions generated.
[0026] FIG. 7b an example of dynamically pruning a transition
relation for a model under assumptions generated from
sub-properties to be evaluated.
[0027] FIG. 8 depicts a computing system for automated lazy
symbolic model checking of finite state systems using symbolic
variable reduction.
DETAILED DESCRIPTION
[0028] Embodiments of the present invention may be realized in
accordance with the following teachings and it should be evident
that various modifications and changes may be made in the following
teachings without departing from the broader spirit and scope of
the invention. The specification and drawings are, accordingly, to
be regarded in an illustrative rather than restrictive sense and
the invention measured only in terms of the claims.
[0029] Methods for formal verification of circuits and other
finite-state systems are disclosed herein providing improved
efficiency and capacity of popular binary decision diagram (BDD)
based algorithms. For one embodiment of a lazy pre-image
computation, a method is disclosed that builds new transition
relation partitions on-demand only for relevant next internal
variables of a state predicate, and conjoins only next state
relations for relevant next internal variables to a pre-image
including the state predicate. For one embodiment of a lazy
fixpoint computation, a method is disclosed that makes iterative
use of lazy pre-image computation to compute conditions that must
necessarily be satisfied to produce a given set of states. For one
embodiment of forward assumption propagation, a method is disclosed
that generates assumptions to characterize a set of interesting
states for sub-properties of the property being evaluated at one or
more evaluation stages. For one embodiment of a dynamic transition
relation pruning technique, a method is disclosed that improves the
efficiency for symbolic model checking computations by pruning
transition relations under assumptions dynamically generated from
the properties being evaluated, thereby providing means to handle
very large scale integrated circuits and other finite state systems
of problematic complexity for prior methods. The teachings of these
disclosed methods provide for symbolic model checking of circuits
and other finite state systems previously too large to be completed
successfully using BDD based algorithms.
[0030] FIG. 1 illustrates an example of a circuit 101 having
internal state variables c, d, e and f; and input variables a and
b. According to the logical combination of inputs to memory element
102, the value of internal state variable c at its next transition
can be determined to be the value of the Boolean expression a AND
c. From the logical combination of inputs to memory element 103,
the value of internal state variable d at its next transition can
be determined to be the value of the input variable b. From the
logical combination of inputs to memory element 104, the value of
internal state variable e at its next transition can be determined
to be the value of the Boolean expression c OR e. Finally, from the
logical combination of inputs to memory element 105, the value of
internal state variable f at its next transition can be determined
to be the value of the Boolean expression c NAND d.
[0031] A model of a circuit or other finite state system can be
formally defined as: a nonempty finite set of Boolean variables,
V=V.sub.S.orgate.V.sub.I, consisting of a union V of internal state
variables V.sub.S with input variables V.sub.I; and a next state
function N(v) for each v in V.sub.S, which is an assignment mapping
of internal state variables according to Boolean (true or false)
valued expressions on V called state predicates.
[0032] For one embodiment, a model may be represented as a nonempty
transition relation, R, on state predicate pairs, where (S1, S2) is
an element of the transition relation, R, if there exists a
transition in the finite state system from a state satisfying
predicate S1 to state satisfying predicate S2. R is also referred
to as a model of the finite state system.
[0033] A partitioned transition relation, R, on a partitioning of
the internal state variables {V1, V2, . . . , Vk} has the
implicitly conjoined form:
R(V,V')=R1(V,V1') AND R2(V,V2') . . . AND Rk(V,Vk')
[0034] where the ith partition is Ri(V,Vi')=AND.sub.for all v' in
Vi' (v'=N(v)). The assertion v'=N(v) is called the next state
relation for v and v' is a copy of v to record the value taken on
by v at the next transition.
[0035] The set of states, S, may be represented using a Boolean
state predicate S(V). Operations on sets may be carried out as
algebraic manipulations of state predicates. The set of states that
can move to S in one transition is called the pre-image of S and
written
Pre(S(V))=V'.[AND.sub.for all v' in Vs' (v'=N(v)) AND S(V')].
[0036] An existential operation V'.[S(V')] represents a
quantification of state predicate S(V') over the variables in V'.
Typically, in order to more efficiently use computation resources,
the operation of computing the pre-image of a set of states is
carried out as a relation product of state predicates using early
variable quantification for partitioned transition relations,
thereby permitting staged reductions of Boolean expressions, as
follows:
1 Pre(S(V)) = V1'.[R1(V,V1') AND ( V2'.[R2(V, V2') AND ( . . .
Vk.[Rk(V,Vk') AND ( VI'.S(V') )] . . . )] )].
[0037] An alternative definition for a model can be set forth as a
pair of induced transformers, Pre and Post, such that Pre(S2)
includes S1 and Post(S1) includes S2 if (S1,S2) is an element of R.
In other words, the Pre transformer identifies any states
satisfying predicate S, for which there exists a transition to some
state satisfying predicate S'. Pre is called a pre-image
transformer. The Post transformer identifies any states satisfying
predicate S', for which there exists a transition from some state
satisfying predicate S. Post is called a post-image
transformer.
[0038] One drawback of a typical pre-image computation is that it
involves the entire partitioned transition relation. But S(V) may
involve only a few variables. Consequently, not all next state
relations are relevant in any particular invocation of a pre-image
computation.
[0039] For example, FIG. 2a graphically illustrates a possible
transition relation 201 for circuit 101 having V.sub.S={c, d, e, f}
and V.sub.I={a, b}. The next state function for variable c is
N(c)=a AND c. Therefore, in order for the circuit to reach a state,
S(c), where c=1 it must have made transition 211 from a state S(a
AND c) where a=1 and c=1. The next state function for variable d is
N(d)=b. Therefore, in order for the circuit to reach a state, S(d),
where d=1 it must have made transition 219 from a state S(b) where
b=1. The next state function for variable e is N(e)=e OR c.
Therefore, in order for the circuit to reach a state, S(e), where
e=1 it must have made transition 212 from a state S(c) where c=1 or
it must have made transition 213 from a state S(e) where e=1. The
next state function for variable f is N(f)=d NAND c. Therefore, in
order for the circuit to reach a state, S(f), where f=1 it must
have made transition 215 from a state S(NOT c) where c=0 or it must
have made transition 218 from a state S(NOT d) where d=0.
[0040] Computing all states reachable to S(e) in two or more
transitions includes the next state function for variable c, which
has already been shown as N(c)=a AND c represented by transition
211. The next state function for variable NOT c is N(NOT c)=NOT(a
AND c)=(NOT a) OR (NOT c). Therefore, in order for the circuit 101
to reach a state, S(NOT c), where c=0 it must have made transition
214 from a state S(NOT a) where a=0 or it must have made transition
216 from a state S(NOT c) where c=0. The next state function for
variable NOT d is N(NOT d)=NOT b. Therefore, in order for the
circuit to reach a state, S(NOT d), where d=0 it must have made
transition 217 from a state S(NOT b) where b=0.
[0041] For a given state predicate, an invocation of a pre-image
computation that uses transition relation 201 may result in
computations that are not relevant to that state predicate. For one
embodiment, a lazy pre-image computation is disclosed which
provides a relevant transition relation abstraction for each
pre-image computation according to the state predicate of the
invocation. Such a lazy pre-image computation may be performed for
a state predicate S(W), where W is contained in V and W.sub.S' is
the set of next internal variables in the set of next variables W',
as follows:
Pre(S(W))=W'.[AND.sub.for all v' in Ws' (v'=N(v)) AND S(W')].
[0042] The approach provided by the lazy pre-image computation
disclosed above differs from previous COI reduction approaches in
that it is not statically derived from a model specification and
then used throughout. Instead, it dynamically provides an
abstraction for each pre-image computation that is relevant to the
particular state predicate associated with the invocation.
Accordingly, lazy pre-image computation provides for greater
efficiency and capacity improvements in popular BDD-based symbolic
model checking methods than previously used pre-image computation
methods.
[0043] For example, the lazy pre-image of a state predicate S(e)
for circuit 101 where e=1 can be computed: 1 Pre ( S ( ) ) = ' [ (
' = N ( ) ) AND S ( ' ) ] . = ' [ ( ' = OR c ) AND ' ] . = ( OR c )
.
[0044] FIG. 2b graphically illustrates a possible transition
relation 202 for circuit 101 built as a result of an invocation of
the lazy pre-image computation Pre(S(e)) on the state predicate
S(e) where e=1. The next state function for variable e is N(e)=e OR
c. Therefore, in order for the circuit to reach a state, S(e),
where e=1 it must have made transition 222 from a state S(c) where
c=1 or it must have made transition 223 from a state S(e) where
e=1. Since no other transitions are relevant to reaching state
S(e), the lazy pre-image method need not build them. As seen in the
above example, this lazy pre-image method potentially reduces the
number of transition relation partitions involved and also the
sizes of partitions. Therefore computations required to explicitly
build a BDD for a desired function may be significantly
reduced.
[0045] For one embodiment, FIG. 3a illustrates performing a lazy
pre-image computation. In processing block 311 transition relation
partitions are updated as needed by adding new transition relations
for only the relevant next internal variables. In processing block
312 a pre-image is initialized to the next state predicate of the
invocation and existentially quantified over the relevant next
input variables. In processing block 313, partitions with relevant
next variables are identified. Finally in processing block 314,
next state relations for relevant variables from the partitions
identified in processing block 313 are conjoined to the pre-image
and quantified.
[0046] The lazy pre-image method disclosed above provides for
greater efficiency and capacity for symbolic model checking
operations, particularly on circuits with a large number of
variables. In a BDD based implementation, building transition
relation partitions only as needed and only for relevant next
internal variables is especially beneficial since the next state
function for an internal variable is efficiently and implicitly
encoded, but a BDD for the function must be explicitly built for
symbolic model checking. Explicitly building BDDs unnecessarily may
become computationally expensive.
[0047] FIG. 3b details one embodiment of a method for performing a
lazy pre-image computation on a state predicate S(W) involving a
set W of internal variables and input variables. In processing
block 320, W.sub.S' is initialized to be the set of next internal
variables in W'. In processing block 321, W.sub.I' is initialized
to be the set of next input variables in W'. In processing block
322, the next internal variables are checked to identify some
variable w' that has not been evaluated. If one is identified,
w'=N(w) is conjoined to the partition including w' and flow returns
to processing block 322 to look for more next variables that have
not been evaluated. Thus the transition relation partitions are
built as needed for the relevant next internal variables. When no
more are found, flow proceeds at processing block 324. In
processing block 324 the pre-image is initialized to the state
predicate existentially quantified for the relevant next input
variables and partition counter i is set to k+1. In processing
block 325, i is decremented. Then in processing block 326,
partition counter i is tested to see if it has reached zero. If
partition counter i has not reached zero, in processing block 327
partition Vi' is checked against W' to identify relevant variables.
If no relevant variables are found, partition Vi' is skipped and
flow proceeds at processing block 325. Otherwise in processing
block 328, all next variables in Vi' that are not in W' are
existentially quantified out from partition Vi' and the remaining
relevant variables are evaluated according to their next state
relations and assigned to Ra. Then in processing block 329, Ra is
conjoined with the pre-image Pre and flow proceeds with the next i
at processing block 325. When i=0 indicating no more partitions
remain at processing block 326, the processing terminates and
pre-image Pre is complete.
[0048] In one embodiment, the lazy pre-image computation disclosed
above provides for potential improvements in key model checking
techniques. For example one embodiment of a lazy pre-image method
provides an efficient general operation that may also be used
effectively in performing fixpoint computations.
[0049] FIG. 4a illustrates one embodiment of a fixpoint computation
method which uses lazy pre-image computations. In processing block
411, a partial fixpoint state predicate, Fix.sub.0, and an initial
frontier predicate, Front.sub.0, are both set to the input
predicate S(W), and counter i is initialized to 1. In processing
block 412, the new frontier predicate, Front.sub.i, is set to the
lazy pre-image of the previous frontier predicate, Front.sub.i-1,
intersected with the negated partial fixpoint predicate,
Fix.sub.i-1, in order to exclude any states whose pre-images have
already been computed. This computation is expressed symbolically
as Pre(Front.sub.i-1) .LAMBDA.Fix.sub.i-1. In processing block 413
a new fixpoint predicate Fix.sub.i is set to the union of the new
frontier predicate, Front.sub.i, and the previous partial fixpoint
predicate, Fix.sub.i-1. Counter i is then incremented. In
processing block 419, Front.sub.i is tested to see if any states
from the previous iteration that need to have pre-images computed
remain in the frontier. If so, processing beginning at processing
block 412 repeats until Front.sub.i is emptied of such states, in
which case processing terminates at processing block 419.
[0050] FIG. 4b illustrates an example for one embodiment of
performing a lazy fixpoint computation for state predicate, S(e),
where e=1, on circuit 101. The fixpoint Fix.sub.0 predicate 420 for
the states reachable to S(e) in zero transitions and the frontier
Front.sub.0 are initially set to e. Since no pre-image computation
is required, no transition relation is built. To compute the
fixpoint Fix.sub.1 predicate 421 for the states reachable to S(e)
in one transition a lazy pre-image of the frontier predicate
Front.sub.0 is computed and combined with NOT Fix.sub.0. Since
frontier predicate Front.sub.0 only involves signal e, lazy
transition relation building only computes a transition relation
partition for e, as [N(e)=e OR c]. Lazy pre-image Pre(S(e)) can be
computed as previously shown, and the lazy pre-image computation
returns e OR c based on the partially computed transition relation.
The new frontier predicate Front.sub.1 is set to (e OR c) AND NOT e
in accordance with processing block 412, which reduces to c AND NOT
e. Fixpoint Fix.sub.1 predicate 421 for states reachable to S(e) in
one transition is set to (c AND NOT e) OR e, which becomes e OR
c.
[0051] To compute the fixpoint Fix.sub.2 predicate 422 for those
states reachable to S(e) in two transitions, the lazy pre-image of
the frontier predicate Front.sub.1 is computed and combined with
NOT Fix.sub.1. The pre-image is calculated as follows: 2 Pre ( c
AND NOT ) = ' , c ' [ ( ' = N ( ) ) AND ( c ' = N ( c ) ) AND S ( '
, c ' ) ] . = ' , c ' [ ( ' = OR c ) AND ( c ' = c AND a ) AND ( c
' AND NOT ' ) ] . = ( c AND a ) AND NOT ( OR c ) .
[0052] Predicate (c AND NOT e) requires lazy transition relation
building of the translation relation partition for c, as [N(c)=c
AND a]. Lazy pre-image computation returns (c AND a) AND NOT (e OR
c) based on the partially computed transition relation. The new
frontier predicate Front.sub.2 is set to (c AND a) AND NOT (e OR c)
in accordance with processing block 412, which reduces to (c AND a
AND NOT e AND NOT c)=0. Fixpoint Fix.sub.2 Predicate 422 for states
reachable to S(e) in two transitions becomes just (e OR c).
[0053] Since frontier predicate Front.sub.2=0 the lazy fixpoint
computation terminates. The transition relations for b, d and f are
not needed and therefore they are not built.
[0054] It will be appreciated that a symbolic model checking
operation may benefit significantly from a reduction in the number
of transition relations used to represent a model. A further
reduction may be accomplished if for each property to be evaluated,
only the necessary portions of the model are represented. For one
embodiment of a dynamic transition relation pruning technique, a
method is disclosed that improves the efficiency for symbolic model
checking computations by pruning transition relations under
assumptions dynamically generated from the properties being
evaluated, thereby providing means to handle very large scale
integrated circuits and other finite state systems of problematic
complexity for prior methods.
[0055] FIG. 5a illustrates a parsing of a property 510, a(bX(Xf)).
At the first stage the property is parsed into a root 500
representing the logical implication operation, a left sub-property
506 representing the variable, a, and a right sub-property 511
representing bX(Xf). The operator X indicates that its predicate
argument holds at the next transition.
[0056] At the second stage the sub-property 511 is parsed into a
root 501 representing the logical implication operation, a left
sub-property 507 representing the variable, b, and a right
sub-property 512 representing X(Xf). At the third stage the
property is parsed into a root 502 representing the next state
operator X, and a right sub-property 513 representing Xf. Finally
at the fourth stage the sub-property 513 is parsed into a root 503
representing the next state operator X, and a right sub-property
514 representing f. Given a parsing of the property assumptions may
be generated for the sup-properties to be evaluated.
[0057] FIG. 5b illustrates one embodiment of a method for producing
and propagating assumptions from sub-properties to be evaluated. In
processing block 521, the assumption for iteration zero,
Assum.sub.0, is initialized to the value one (true) and Node is set
to the root 500 of the property to be evaluated. The iteration
counter i is then incremented and processing proceeds to processing
block 522. In processing block 522, the Node is tested to see if it
consists of a single variable, in which case processing terminates
at processing block 522. If not, processing proceeds to processing
block 523. In processing block 523 the type of the Node operation
is identified. If it is an implication operation processing
proceeds at processing block 524. On the other hand, if it is a
next state operator X, then processing proceeds to processing block
525.
[0058] In processing block 524 the assumption for iteration i,
Assum.sub.i, is set to the assumption for iteration i-1,
Assum.sub.i-1, combined with the left sub-property of Node using
the logical AND operation. In processing block 525 the assumption
for iteration i, Assum.sub.i, is set to post-image of the
assumption for iteration i-1, Assum.sub.i-1. Processing then
proceeds to processing block 526 from processing block 524 or from
processing block 525, where Node is set to the right sub-property
of Node. The iteration counter i is then incremented and processing
proceeds to processing block 522.
[0059] FIG. 5c shows an example of producing and propagating
assumptions from sub-properties to be evaluated. In iteration zero,
assumption 540 is set to the value one and sub-property 530 is set
to the state predicate for property to be evaluated (a(bX(Xf))). In
iteration one, assumption 541 is set to a=(1 AND a) in accordance
with processing block 524 and sub-property 531 is set to the right
sub-property of sub-property 530, bX(Xf) in accordance with
processing block 526. In iteration two, assumption 542 is set to a
AND b and sub-property 532 is set to the right sub-property of
sub-property 531, X(Xf). In iteration three, assumption 543 is set
to Post(a AND b), which may be evaluated as d since N(d)=b, and
sub-property 533 is set to the right sub-property of sub-property
532, Xf. In iteration four, assumption 544 is set to Post(Post(a
AND b) which may be evaluated to one (true) and sub-property 534 is
set to the right sub-property of sub-property 533, f.
[0060] The number of variables in a transition relation may be
reduced according to a dynamically generated assumption as the
transition relation is built. For instance the next state function
for a variable f, N(f)=c NAND d may be pruned according to an
assumption including (d=1) to N(f)=NOT c.
[0061] FIG. 6a graphically illustrates the state space of a model
with a transition relation that was built according to one
embodiment of an iterative lazy pre-image computation method to
evaluate sub-property 530 or 534. It includes five variables that
may be exhaustively searched for an assignment that satisfies the
sub-property 530 or 534. These variables are f at block 611, c at
block 613, d at block 615, a at block 617 and b at block 618. The
three internal variables for which next state functions are
included in the transition relation are, N(f) at block 612, N(c) at
block 614, and N(d) at block 616. Since the assumptions 540 and 544
are trivial no pruning may be performed on the next state
functions.
[0062] FIG. 6b graphically illustrates the state space of a
dynamically pruned model with a transition relation that was built
according to one embodiment of a lazy pre-image computation method
to evaluate sub-property 531 under assumption 541. It includes four
variables that may be exhaustively searched for an assignment that
satisfies the sub-properties 531 or 532. These variables are f at
block 621, c at block 623, d at block 625, and b at block 628. The
three internal variables for which next state functions are
included in the transition relation are, N(f) at block 622, N(c) at
block 624, and N(d) at block 626. Since the assumption 541 includes
only the input variable, a, pruning of the transition relation may
be performed only on the next state function for c, producing
N(c)=c instead of N(c)=c AND a.
[0063] FIG. 6c graphically illustrates the state space of a
dynamically pruned model with a transition relation that was built
according to one embodiment of a lazy pre-image computation method
to evaluate sub-property 532 under assumption 542. It includes
three variables that may be exhaustively searched for an assignment
that satisfies the sub-property 531. These variables are f at block
621, c at block 623, d at block 625. The three internal variables
for which next state functions are included in the transition
relation are, N(f) at block 622, N(c) at block 624, and N(d) at
block 626. Since the assumption 541 includes the input variables, a
and b, pruning of the transition relation may be performed on the
next state function for c, producing N(c)=c instead of N(c)=c AND a
and on the next state function for d, producing N(d)=1 instead of
N(d)=b.
[0064] FIG. 6d graphically illustrates the state space of a
dynamically pruned model with a transition relation that was built
according to one embodiment of a lazy pre-image computation method
to evaluate sub-property 533 under assumption 543. It includes only
two variables that may be exhaustively searched for an assignment
that satisfies the sub-property 533. These variables are f at block
631 and c at block 633. Both of these internal variables' next
state functions are included in the transition relation. They are,
N(f) at block 632, and N(c) at block 634. Since the assumption 543
includes the input variable, a, and the internal variable, d,
pruning of the transition relation may be performed on the next
state functions for c, producing N(c)=c instead of N(c)=c AND a and
for f, producing N(f)=NOT c instead of N(f)=c NAND d.
[0065] It will be appreciated that a property may be considered a
sub-property of itself. It will also be appreciated that an
assumption produced from a sub-property to be evaluated may be used
to prune a transition relation in a variety of ways. It can be
observed in FIG. 6a through FIG. 6e that a significant reduction in
state storage may be achieved through dynamic model pruning.
[0066] Alternatively the computational complexity of checking the
model may be reduced according to the assumption. For instance some
model checking methods exhaustively search a state space in order
to verify a property or sub-property. If the transition relation is
pruned by one or more assignments of variables according to the
assumption produced from a sub-property of the property being
evaluated, the computational complexity of the search may be
significantly reduced.
[0067] It will also be appreciated that one may desire to reduce
the overall size of the model representation, perhaps at the cost
of some addition computational complexity. Alternatively the number
of variables in a model or the complexity of evaluating a
sub-property may be reduced according to the assumption as the
sub-property is being evaluated on the transition relation.
[0068] For example, a lazy pre-image of a state predicate S(Xf) AND
Assum.sub.3 for circuit 101 can be computed: 3 Pre ( S ( Xf ) ) AND
Assum 3 = f ' [ ( f ' = N ( f ) ) AND S ( f ' ) ] AND Assum 3 = f '
[ ( f ' = ( c NAND d ) ) AND f ' ] AND Assum 3 = ( c NAND d ) AND d
= 1 = NOT c
[0069] In general each sub-property may need to be evaluated
according to its corresponding assumption. This operation may be
performed in such a way as to substantially reduce the size of
transition relations by pruning next state functions as the
transition relations are dynamically built by a lazy pre-image
calculation.
[0070] FIG. 7a illustrates one embodiment of a method for
dynamically pruning a model by producing and propagating
assumptions as shown in FIG. 5b from sub-properties to be evaluated
and then pruning the transition relation under the assumptions
generated. Processing block 711 is entered when a singular Node is
identified in processing block 522. In processing block 711, the
iteration counter i is decremented and then the sub-property for
iteration i, SP.sub.i is computed from the singular Node variable
under the assumption for iteration i, Assum.sub.i. Processing then
proceeds to processing block 712 where the iteration counter is
tested. Processing beginning in processing block 713 is repeated
until the iteration counter is equal to zero in processing block
712, in which case processing terminates and returns the predicate
SP.sub.i. In processing block 713 the Node is set to its parent
Node and the iteration counter, i, is decremented. Processing then
proceeds in processing block 714.
[0071] In processing block 714 the type of the Node operation is
identified. If it is an implication operation processing proceeds
at processing block 715. On the other hand, if it is a next state
operator X, then processing proceeds to processing block 716.
[0072] In processing block 715 the state predicate for iteration i,
SP.sub.i, is set to the state predicate for iteration i+1,
SP.sub.i+1, combined with the negated left sub-property of Node
using the logical OR operation and evaluated under the assumption
Assum.sub.i. In processing block 716 the state predicate for
iteration i, SP.sub.i, is set to lazy pre-image of the state
predicate for iteration i+1, SP.sub.i+1 and evaluated under the
assumption Assum.sub.i. Processing then proceeds to processing
block 712 from processing block 715 or from processing block
716.
[0073] FIG. 7b shows an example of dynamically pruning a transition
relation as it is built in a lazy pre-image computation according
to assumptions generated from sub-properties to be evaluated. In
iteration 4, state predicate 724 is set to the singular Node
variable, f, and evaluated under the assumption 1 (true) which
leaves the predicate unchanged. In iteration 3, state predicate 723
is set to the lazy pre-image of the predicate of the predicate f
and evaluated under the assumption, d, which in accordance with
processing block 716, reduces the next state function N(f)=c NAND d
to N(f)=NOT c. In iteration 2, state predicate 722 is set to the
lazy pre-image of the predicate, NOT c, and evaluated under the
assumption, a AND b, which in accordance with processing block 716,
reduces the next state function N(c)=a AND c to N(c)=c. In
iteration 1, state predicate 721 is set to the logical OR
combination of predicate, NOT c, and negated left sub-property, b,
resulting in (NOT b OR NOT c) and then evaluated under the
assumption, a, in accordance with processing block 715, which
leaves the predicate unchanged. In iteration 0, state predicate 720
is set to the logical OR combination of predicate, (NOT b OR NOT
c), and negated left sub-property, a, resulting in (NOT a OR NOT b
OR NOT c) and then evaluated under the assumption, a, in accordance
with processing block 715, which leaves the predicate
unchanged.
[0074] In general, each sub-property may need to evaluated
according to its corresponding assumption. If the lazy pre-image
computation Pre(SP.sub.i+1) under the assumption Assum.sub.i is
equal to 1 then no succeeding evaluations are needed as each will
trivially be satisfied in processing block 715 or processing block
716.
[0075] It will be appreciated that the methods herein disclosed or
methods substantially similar to those herein disclosed may be
implemented in one of many programming languages for performing
automated computations including but not limited to lazy pre-image
computations, dynamic production and propagation of assumptions,
dynamic pruning of transition relations, lazy fixpoint computations
using dynamic model pruning, and lazy model checking using dynamic
model pruning on high-speed computing devices.
[0076] For example, FIG. 8 illustrates a computer system to perform
computations, for one such embodiment. Processing device 822 is
connectable with various recordable storage media, transmission
media and I/O devices to receive data structures and programmed
methods. Representative data structures 801 may include circuit
descriptions 811, transition relations 812, and finite state models
813. Representative programmed methods 802 may include assumption
propagation programs 814, lazy pre-image programs 815, transition
relation pruning programs 816, and model checking programs 817.
Components of either or both of the data structures and programmed
methods may be stored or transmitted on recordable media such as
removable storage disks 825, which may be accessed through an
access device 826 in processing device 822 or in a storage serving
system 821. Storage serving system 821 or processing device 822 may
also include other removable storage media or non-removable storage
media suitable for storing or transmitting data structures 801 or
programmed methods 802. Component data structures and programmed
methods may also be stored or transmitted on transmission media
such as network 824 for access by processing device 822 or entered
by users through I/O device 823. It will be appreciated that
systems such as the one illustrated are commonly available and
widely used in the art of designing finite state hardware and
software systems. It will also be appreciated that the complexity,
capabilities, and physical forms of such design systems improves
and changes rapidly, and therefore understood that the design
system illustrated is by way of example and not limitation.
[0077] The above description is intended to illustrate preferred
embodiments of the present invention. From the discussion above it
should also be apparent that the invention can be modified in
arrangement and detail by those skilled in the art without
departing from the principles of the present invention within the
scope of the accompanying claims.
* * * * *