Method and system for implementing selective transformation for low power verification

Abstract

Disclosed is an improved approach to implement selective transformations of circuit components for performing verification. The approach looks at the observability of components to downstream properties to determine whether transformations are needed. The verification system leverages the knowledge about the behavior of the domains/components to identify only a subset of components that really need to undergo transformation.

The invention claimed is: 
     
       1. A computer-implemented method for implementing transformations for verifying a circuit design, comprising:
 analyzing a circuit design comprising a plurality of components; 
 accessing power intent information for the circuit design; 
 receiving observable points for the circuit design and accessing one or more verification tasks corresponding to the observable points; 
 identifying one or more phases for a power sequence associated with the circuit design; 
 for a phase from the one or more phases, identifying a subset of components from the plurality of components within the circuit design for transformation in a logical representation of the circuit design, wherein a component is identified for the transformation if corruption for the component is observable for the observable points; 
 executing, at a transformation module stored partially in memory and functioning in conjunction with at least one microprocessor of a computing system, the transformation on the component identified for the transformation to generate a transformed component in the logical representation of the circuit design while skipping execution of the transformation on one or more remaining components in the circuit design; and 
 performing the verification with the logical representation of the circuit design having the transformed component and the one or more remaining components. 
 
     
     
       2. The method of  claim 1 , wherein the verification comprises formal verification. 
     
     
       3. The method of  claim 2 , in which the power sequence associated with the circuit design is partitioned into the one or more phases. 
     
     
       4. The method of  claim 2 , in which the observable points are identified from the one or more phases, the observable points pertaining to a specific verification task to be executed from among the one or more verification tasks. 
     
     
       5. The method of  claim 2 , in which phases are identified by a process comprising:
 selecting a property to analyze; 
 identifying the one or more phases based at least in part upon the one or more conditions; and 
 extracting one or more conditions for the property. 
 
     
     
       6. The method of  claim 2 , wherein behavior of an output of a powered-off domain is reviewed to identify the component to transform. 
     
     
       7. The method of  claim 2 , wherein the transformation is performed by a process comprising:
 determining a power control signal; 
 determining a supply net; 
 identifying a dependency between the power control signal and the supply net; and 
 from the dependency, determining the component to transform. 
 
     
     
       8. A computer program product that includes a non-transitory computer readable medium, the computer readable medium comprising a plurality of computer instructions which, when executed by a processor, cause the processor to execute performing a process for implementing transformations for verifying a circuit design, the process comprising:
 analyzing a circuit design comprising a plurality of components; 
 accessing power intent information for the circuit design; 
 receiving observable points for the circuit design and accessing one or more verification tasks corresponding to the observable points; 
 identifying one or more phases for a power sequence associated with the circuit design; 
 for a phase from the one or more phases, identifying a subset of components from the plurality of components within the circuit design for transformation in a logical representation of the circuit design, wherein a component is identified for the transformation if corruption for the component is observable for the observable points; 
 executing, at a transformation module stored partially in memory and functioning in conjunction with at least one microprocessor of a computing system, the transformation on the component identified for the transformation to generate a transformed component in the logical representation of the circuit design while skipping execution of the transformation on one or more remaining components in the circuit design; and 
 performing the verification with the logical representation of the circuit design having the transformed component and the one or more remaining components. 
 
     
     
       9. The computer program product of  claim 8 , wherein the verification comprises formal verification. 
     
     
       10. The computer program product of  claim 9 , in which the power sequence associated with the circuit design is partitioned into the one or more phases. 
     
     
       11. The computer program product of  claim 9 , in which the observable points are identified from the one or more phases, the observable points pertaining to a specific verification task to be executed from among the one or more verification tasks. 
     
     
       12. The computer program product of  claim 9 , wherein the plurality of computer instructions, when executed by a processor, further cause the processor to execute:
 selecting a property to analyze; 
 identifying the one or more phases based at least in part upon the one or more conditions; and 
 extracting one or more conditions for the property. 
 
     
     
       13. The computer program product of  claim 9 , wherein behavior of an output of a powered-off domain is reviewed to identify the component to transform. 
     
     
       14. The computer program product of  claim 9 , wherein the plurality of computer instructions, when executed by a processor, further cause the processor to execute:
 determining a power control signal; 
 determining a supply net; 
 identifying a dependency between the power control signal and the supply net; and 
 from the dependency, determining the component to transform. 
 
     
     
       15. A system for verifying a design, comprising:
 one or more processors that process computer program code, where the one or more processors process the computer code for analyzing a circuit design comprising a plurality of components; accessing power intent information for the circuit design; receiving observable points for the circuit design and identifying one or more verification tasks corresponding to the observable points; identifying one or more phases for a power sequence associated with the circuit design; for a phase from the one or more phases, identifying a subset of components from the plurality of components within the circuit design for transformation in a logical representation of the circuit design, wherein a component is identified for the transformation if corruption for the component is observable for the observable points; executing the transformation on the component identified for the transformation to generate a transformed component in the logical representation of the circuit design while skipping execution of the transformation on one or more remaining components in the circuit design; and performing the verification with the logical representation of the circuit design having the transformed component and the one or more remaining components; and 
 a tangible, non-transitory storage medium for storing results of verifying the electronic design. 
 
     
     
       16. The system of  claim 15 , wherein the verification comprises formal verification. 
     
     
       17. The system of  claim 16 , in which the power sequence associated with the circuit design is partitioned into the one or more phases. 
     
     
       18. The system of  claim 16 , in which the observable points are identified from the one or more phases, the observable points pertaining to a specific verification task to be executed from among the one or more verification tasks. 
     
     
       19. The system of  claim 16 , wherein the computer code, when executed by the one or more processors, further cause the one or more processors to execute:
 selecting a property to analyze; 
 identifying the one or more phases based at least in part upon the one or more conditions; and 
 extracting one or more conditions for the property. 
 
     
     
       20. The system of  claim 16 , wherein behavior of an output of a powered-off domain is reviewed to identify the component to transform. 
     
     
       21. The system of  claim 16 , wherein the computer code, when executed by the one or more processors, further cause the one or more processors to execute:
 determining a power control signal; 
 determining a supply net; 
 identifying a dependency between the power control signal and the supply net; and 
 from the dependency, determining the component to transform.