Power State Transition Verification For Electronic Design

Abstract

Various implementations of the invention may be applied to generate an auxiliary verification statement. The auxiliary verification statement defines properties that may be employed to check if the power domains are active at appropriate times. Particularly, the auxiliary verification statement checks to ensure that power domain transitions do not interfere with the operation of the device design. With various implementations of the invention, an auxiliary verification statement may be generated by first determining a set of properties instantiated in a verification statement and then synthesizing the auxiliary verification statement based upon the determined properties, the corresponding device design and the power domains. In some implementations, the auxiliary verification statement instantiates properties that check if the power domains related to the properties in the verification statement are active when the verifications statement is exercised. In various implementations, this is accomplished by substituting select ones of the properties in the verification statement with select properties corresponding to the power domain.

1 . A computer implemented method for synthesizing a set of auxiliary verification statements comprising:
 accessing by a computer a device design;   accessing by the computer a verification statement corresponding to the device design;   identifying a plurality of power domains in the device design;   identifying first property instantiated in the verification statement;   synthesizing on the computer a set of auxiliary verification statements based in part upon the plurality of power domains and the first property;   saving the set of auxiliary verification statements to a memory storage location.   
   
   
       2 . The computer implemented method recited in  claim 1 , the method act of synthesizing on the computer a set of auxiliary verification statements based in part upon the plurality of power domains and the first property comprising:
 determining on the computer a plurality of driving power domains corresponding to the first property, the plurality of driving power domains being a subset of the plurality of power domains; and   for the plurality of driving power domains,
 determining a condition wherein the driving power domain is active; 
 generating an auxiliary property based on the condition and the first property; 
 generating an auxiliary verification statement based on the auxiliary property and the verification statement; and 
 adding the auxiliary verification statement to the set of auxiliary verification statements. 
   
   
   
       3 - 8 . (canceled) 
   
   
       9 . The computer implemented method recited in  claim 2 , the method act of identifying a first property instantiated in the verification statement comprising:
 selecting a property from the verification statement; and   translating the property into the linear temporal logic form.   
   
   
       10 . The computer implemented method recited in  claim 9 , the device design having a plurality of design elements; and
 the method act of determining on the computer a plurality of driving power domains corresponding to the first property comprising:
 identifying ones of the plurality of design elements corresponding to the first property; and 
 identifying ones of the plurality of power domains corresponding to the ones of the plurality of design elements. 
   
   
   
       11 . The computer implemented method recited in  claim 10 , the translated property having the form pv1 U! pv2. 
   
   
       12 . The computer implemented method recited in  claim 11 , the method act of generating an auxiliary property based on the condition and the first property comprising:
 identifying pv2 from the translated property; and   forming the auxiliary property from the condition and pv2.   
   
   
       13 . The computer implemented method recited in  claim 12 , the auxiliary property having form c W pv2, where c represents the condition. 
   
   
       14 . The computer implemented method recited in  claim 13 , further comprising:
 identifying a second property instantiated in the verification statement; and   wherein the method act of synthesizing a set of auxiliary verification statements is further based in part upon the second property.   
   
   
       15 . The computer implemented method recited in  claim 14 , further comprising making the set of auxiliary verification statements available to a formal verification engine. 
   
   
       16 . The computer implemented method recited in  claim 10 , the translated property having the form X! pv2. 
   
   
       17 . The computer implemented method recited in  claim 16 , the method act of generating an auxiliary property based on the condition and the first property comprising;
 identifying the operator from the translated property; and   forming the auxiliary property from the condition and operator.   
   
   
       18 . The computer implemented method recited in  claim 17 , the auxiliary property having the form X c, where c represents the condition. 
   
   
       19 . An article of manufacture for synthesizing a set of auxiliary verification statements comprising:
 software instructions for enabling a computer to perform a set of predetermined operations; and   a computer readable medium bearing the software instructions;   the set of predetermined operations including:
 accessing a device design; 
 accessing a verification statement corresponding to the device design; 
 identifying a plurality of power domains in the device design; 
 identifying a first property instantiated in the verification statement; 
 synthesizing a set of auxiliary verification statements based in part upon the plurality of power domains and the first property; 
 saving the set of auxiliary verification statements to a memory storage location. 
   
   
   
       20 . The article of manufacture recited in  claim 19 , the predetermined operation for synthesizing a set of auxiliary verification statements based in part upon the plurality of power domains and the first property comprising:
 determining a plurality of driving power domains corresponding to the first property, the plurality of driving power domains being a subset of the plurality of power domains; and for the plurality of driving power domains,
 determining a condition wherein the driving power domain is active; 
 generating an auxiliary property based on the condition and the first property; 
 generating an auxiliary verification statement based on the auxiliary property and the verification statement; and 
 adding the auxiliary verification statement to the set of auxiliary verification statements. 
   
   
   
       21 . The article of manufacture recited in  claim 20 , the predetermined operation for identifying a first property instantiated in the verification statement comprising:
 selecting a property from the verification statement; and   translating the property into the linear temporal logic form.   
   
   
       22 . The article of manufacture recited in  claim 21 , the device design having a plurality of design elements; and
 the predetermined operation for determining a plurality of driving power domains corresponding to the first property comprising:
 identifying ones of the plurality of design elements corresponding to the first property; and 
 identifying ones of the plurality of power domains corresponding to the ones of the plurality of design elements. 
   
   
   
       23 . The article of manufacture recited in  claim 22 , the translated property having the form pv1 U! pv2. 
   
   
       24 . The article of manufacture recited in  claim 23 , the predetermined operation for generating an auxiliary property based on the condition and the first property comprising:
 identifying pv2 from the translated property; and   forming the auxiliary property from the condition and pv2.   
   
   
       25 . The article of manufacture recited in  claim 24 , the auxiliary property having the form c W pv2, where c represents the condition. 
   
   
       26 . The article of manufacture recited in  claim 25 , the set of predetermined operations further comprising:
 identifying a second property instantiated in the verification statement; and   wherein the method act of synthesizing a set of auxiliary verification statements is further based in part upon the second property.   
   
   
       27 . The article of manufacture recited in  claim 26 , the set of predetermined operations further comprising making the set of auxiliary verification statements available to a formal verification engine. 
   
   
       28 . The article of manufacture recited in  claim 22 , the translated property having the form X! pv2. 
   
   
       29 . The article of manufacture recited in  claim 28 , the predetermined operation for generating an auxiliary property based on the condition and the first property comprising:
 identifying the operator from the translated property; and   forming the auxiliary property from the condition and operator.   
   
   
       30 . The article of manufacture recited in  claim 29 , the auxiliary property having the form X c, where c represents the condition. 
   
   
       31 . A formal verification tool for synthesizing a set of auxiliary verification statements comprising:
 a design processing unit capable of accessing a device design;   a specification processing unit capable of accessing a verification specification;   an auxiliary verification statement generation unit capable of synthesizing a set of auxiliary verification statements based upon the device design and the verification specification; and   a formal verification engine capable of verifying the device design according to the verification specification and the set of auxiliary verification statements.