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.

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.