Verification system using symbolic variable reduction

Abstract

Methods for formal verification of circuits and other finite-state systems are disclosed herein, providing for improved efficiency and capacity of popular binary decision diagram (BDD) based algorithms. A lazy pre-image computation method is disclosed that builds new transition relation partitions on-demand only for relevant next internal variables of a state predicate. A symbolic variable reduction method is disclosed to eliminate variables in a state predicate under “don't care” conditions. Symbolic variable reduction improves the efficiency for symbolic model checking computations especially lazy pre-image based computations 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 automated 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 verification system comprising: 
 means for identifying a don't care variable in a first state predicate; and    means for producing a reduced second state predicate from the first state predicate.    
     
     
         2 . The verification system of  claim 1  further comprising: 
 means for performing lazy pre-image computations on the reduced second predicate.  
 
     
     
         3 . A verification system comprising: 
 means for identifying a don't care variable in a first state predicate and a don't care condition; and    means for producing a reduced second state predicate from the first state predicate.    
     
     
         4 . The verification system of  claim 3  wherein the second state predicate is implied by the first state predicate and wherein the second state predicate implies the first state predicate or the don't care condition.  
     
     
         5 . The verification system of  claim 3  further comprising: 
 means for performing lazy pre-image computations on the reduced second predicate.  
 
     
     
         6 . 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: 
 identify a first variable of a state predicate, P, under a condition predicate, Q; such that there exists a reduced state predicate, P′, not including the first variable and satisfying the relation: 
 (P P′) AND (P′  (P OR Q)); and  
 
 produce the state predicate, P′, by eliminating the first variable from the state predicate, P.  
   
     
     
         7 . The verification system of  claim 6  wherein a first value is substituted for said first variable.  
     
     
         8 . The verification system of  claim 7  wherein a constant logical value is substituted for the first variable in (P OR Q).  
     
     
         9 . 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: 
 eliminate a variable in a state predicate under a don't care condition by a symbolic variable reduction having a first argument involving the state predicate and a second argument involving a union of the state predicate and the don't care condition.  
   
     
     
         10 . The verification system of  claim 9  wherein said plurality of executable instructions are further to cause the processing device to: 
 identify a first case when the variable is in the first argument and not in the second argument.  
 
     
     
         11 . The verification system of  claim 10  wherein said plurality of executable instructions are further to cause the processing device to: 
 identify a second case when the variable is in the first argument and in the second argument.  
 
     
     
         12 . The verification system of  claim 11  wherein said second case being identified, said plurality of executable instructions are further to cause the processing device to: 
 substitute a first value for the variable in the first argument and substitute a second value for the variable in the second argument  
 check if an intersection of the first argument having the first value substituted for the variable with the second argument having the second value substituted for the variable is empty.  
 
     
     
         13 . 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: 
 eliminate a variable, v, in a state predicate, P, under a don't care condition, Q.  
   
     
     
         14 . The verification system of  claim 13  wherein said plurality of executable instructions cause the processing device to: 
 eliminate said variable, v, by a symbolic variable reduction having a first argument involving the state predicate, P, and a second argument involving a union of the state predicate, P, and the don't care condition, Q.  
 
     
     
         15 . The verification system of  claim 14  wherein said wherein the second argument is a negated union of the state predicate, P, and the don't care condition, Q.  
     
     
         16 . The verification system of  claim 14  wherein said wherein a first value is substituted for the variable the first argument.  
     
     
         17 . The verification system of  claim 16  wherein said wherein a second value is substituted for the variable the second argument.  
     
     
         18 . The verification system of  claim 14  wherein said wherein said plurality of executable instructions cause the processing device to: 
 eliminate said variable, v, from the first argument if it can be identified that said variable, v, is in the first argument and is not in the second argument;  
 else if it can be identified that said variable, v, is in the first argument and in the second argument, substitute a first value and a second value for said variable, v, in the first argument and for said variable, v, in the second argument,  
 form a first intersection of the first argument having the first value substituted for said variable, v, with the second argument having the second value substituted for said variable, v,  
 form a second intersection of the first argument having the second value substituted for said variable, v, with the second argument having the first value substituted for said variable, v, and if the first intersection and the second intersection are empty, eliminate said variable, v, from the first argument.  
 
     
     
         19 . The verification system of  claim 18  wherein it can be identified that said variable, v, is in the second argument and is not in the first argument, said plurality of executable instructions cause the processing device to: 
 eliminate a variable, w, by a recursive symbolic variable reduction having a first recursive argument involving the state predicate, P, and a second recursive argument involving the second argument having said variable, v, eliminated.  
 
     
     
         20 . The verification system of  claim 19  wherein said second recursive argument involves a negated intersection of the second argument having the first value substituted for said variable, v, with the second argument having the second value substituted for said variable, v.