Abstract:
Method and system for verifying power specifications of a low power design are disclosed. The method includes receiving a register-transfer level (RTL) netlist representation of the low power design, receiving a power specification file for describing power requirements of the low power design and verifying the power specification file in accordance with the RTL netlist representation of the low power design. The method further includes verifying completeness, compatibility, and consistency of power requirements for the low power design.

Description:
FIELD OF THE INVENTION 
       [0001]    The present invention relates to the field of electronic design automation tools. In particular, the present invention relates to a method and system for verifying power specifications of a low power design. 
       BACKGROUND OF THE INVENTION 
       [0002]    Due to consumers&#39; increasing expectation of longer battery life and higher performance for their mobile devices, power management has become one of the most critical design issues. However, as integrated circuits move into nanometer-scale processes, devices created using 90-nanometer and smaller process technologies can consume as much power when they are not in use as when they are being used because of increased leakage current when the devices are in the idle state. Minimizing leakage current and optimizing dynamic power consumption can lead to longer battery life and lower packaging and cooling costs. While advanced low power design methodologies, such as static and dynamic voltage/frequency scaling, power gating, and state retention, offer additional power savings, they also increase the complexity of design verification. 
         [0003]    The complexity of design verification is exacerbated by the fact that the majority of the low power logic is introduced into the gate netlist during synthesis and physical implementation. However, a full-chip exhaustive gate-level simulation is not a practical or scalable methodology for verifying the functionalities of today&#39;s complex designs. In recent years, verification methodology utilizing formal (mathematical) proofs has gained wide popularity due to their ability to verify complex designs exhaustively. Equivalence checking (EC) is one such formal verification method which allows checking the logical equivalence of two designs at the same or different levels of abstraction. For instance, EC can check whether an implemented full-chip gate netlist is equivalent to the reference full-chip RTL design. 
         [0004]      FIG. 1A  illustrates a conventional method for conducting equivalence checking. As shown in  FIG. 1A , the method compares a design specification represented by an RTL netlist  102  to a design implementation represented by a gate netlist  106 . The gate netlist  106  is created from the RTL netlist  102  by using a synthesis tool  104 . In general, an EC methodology utilizes formal verification techniques such as Binary Decision Diagrams (BDDs) and Satisfiability (SAT) Solvers that operate on the Boolean gate level netlist to establish the equivalence between the RTL netlist  102  and the gate netlist  106  of a design. One drawback of this conventional methodology is that no low power logic is included in the RTL netlist and the gate netlist, and thus the EC does not verify any low power logic that may be used in the ultimate design. 
         [0005]      FIG. 1B  illustrates another conventional method for conducting equivalence checking. This method modifies the conventional method described in  FIG. 1A  by incorporating synthesis-tool specific low power commands  103  in the generation of the gate netlist. Thus the synthesis tool  104  uses both the RTL netlist and the synthesis-specific low power commands to generate a low power gate netlist  108 . Then, the EC is conducted between the design specification represented by the RTL netlist  102  and the design implementation represented by the low power gate netlist  108 . There are at least three drawbacks associated with this approach. First, the low power logic in the gate netlist cannot be verified since there is no low power logic in the original RTL netlist. Second, performing EC between RTL netlist and low power gate netlist without disabling the low power logic in gate netlist may yield incorrect verification results. The reason is that the low power logic inserted in the gate netlist by the synthesis-specific commands, such as isolation cell logic, state retention cell logic etc., is shared with the normal operation logic, and can alter the functionality of the design in the normal operating modes. In order to perform EC of normal operating mode (between RTL netlist and low power gate netlist), certain constraints need to be manually added to the low power gate netlist. These constraints tie certain signals in the design (pins or nets) to logic 0 or logic 1 value, thereby allowing disabling the low power logic. The process of applying such hard-coded (0 or 1) constraints to the gate netlist is very tedious and prone to human errors. Furthermore, applying multiple pin or net constraints on the low power gate netlist may cause certain valid functional modes to be excluded from the formal verification process, thereby resulting in incomplete verification. 
         [0006]    Another drawback of the conventional methodology described in  FIG. 1B  is that designers can only conduct verification of power requirements with the gate netlist  108 . The gate netlist is typically a large file containing complex circuit details and structures. If problems are found in the specification of power constraints, such problems need to be fixed in the RTL netlist  102  and the synthesis tool specific low power commands  103 , and then the revised design would be synthesized again to generate a revised low power gate netlist  108 . As a result, this verification and debugging process is tedious and time-consuming. 
         [0007]    Therefore, there is a need to address the issues associated with the conventional methodologies for verifying power specifications of a low power design. 
       SUMMARY 
       [0008]    The present invention relates to a method and system for verifying power specifications of a low power design. In one embodiment, the method includes receiving a register-transfer level (RTL) netlist representation of the low power design, receiving a power specification file for describing power requirements of the low power design and verifying the power specification file in accordance with the RTL netlist representation of the low power design. The method further includes verifying completeness, compatibility, and consistency of power requirements for the low power design. 
     
    
     
       BRIEF DESCRIPTION OF THE DRAWINGS 
         [0009]    The aforementioned features and advantages of the invention, as well as additional features and advantages thereof, will be more clearly understandable after reading detailed descriptions of embodiments of the invention in conjunction with the following drawings. 
           [0010]      FIG. 1A  illustrates a conventional method for conducting equivalence checking. 
           [0011]      FIG. 1B  illustrates another conventional method for conducting equivalence checking. 
           [0012]      FIG. 2  illustrates an example design incorporating power information according to an embodiment of the present invention. 
           [0013]      FIG. 3  illustrates a method for conducting equivalence checking according to an embodiment of the present invention. 
           [0014]      FIG. 4  illustrates a flow diagram for processing power specification file commands to generate a reference low power RTL netlist according to an embodiment of the present invention. 
           [0015]      FIGS. 5A-5E  illustrate insertion of low power logic in an exemplary design according to embodiments of the present invention. 
           [0016]      FIG. 6  illustrates a method for verifying power specifications of a low power design according to an embodiment of the present invention. 
       
    
    
       [0017]    Like numbers are used throughout the figures. 
       DESCRIPTION OF EMBODIMENTS 
       [0018]    Methods and systems are provided for equivalence checking of a low power design. The following descriptions are presented to enable any person skilled in the art to make and use the invention. Descriptions of specific embodiments and applications are provided only as examples. Various modifications and combinations of the examples described herein will be readily apparent to those skilled in the art, and the general principles defined herein may be applied to other examples and applications without departing from the spirit and scope of the invention. Thus, the present invention is not intended to be limited to the examples described and shown, but is to be accorded the widest scope consistent with the principles and features disclosed herein. 
         [0019]    Some portions of the detailed description that follows are presented in terms of flowcharts, logic blocks, and other symbolic representations of operations on information that can be performed on a computer system. A procedure, computer-executed step, logic block, process, etc., is here conceived to be a self-consistent sequence of one or more steps or instructions leading to a desired result. The steps are those utilizing physical manipulations of physical quantities. These quantities can take the form of electrical, magnetic, or radio signals capable of being stored, transferred, combined, compared, and otherwise manipulated in a computer system. These signals may be referred to at times as bits, values, elements, symbols, characters, terms, numbers, or the like. Each step may be performed by hardware, software, firmware, or combinations thereof. 
         [0020]    A power specification file contains design and technology-related power constraints that capture a designer&#39;s power management intent. In general, a power specification file allows a designer to specify the power domains, low power cells, rules for creating low power logic, etc. A power specification file is defined in any low power design specification language. The Common Power Format (CPF) is a low power design specification language created by Cadence Design Systems, Inc., and is used for creating a power specification file. In subsequent text, references to CPF file will mean references to a power specification file created in any generic low power design specification language. Similarly, a CPF command will refer to any generic low power design specification command. 
         [0021]    In a low power design, a power domain (PD) is a collection of logic blocks (hierarchical instances) and leaf instances that use the same power supply during normal operation and that can be powered on or off at the same time. In addition, a power mode (PM) is a static state of a design that indicates the ON and OFF status of each power domain; a power management module (PMM), which is also called as the power manager, is a low power controller that generates control signals for enabling or disabling the low power logic; isolation (ISO) cells are logic used to isolate signals which are going from a power off domain to a power on domain; level shifter (LS) cells are logic to pass data signals between power domains operating at different voltages; and state retention (SR) cells are special flop or latch used to retain the state of the cell when its main power supply is turned off. 
         [0022]      FIG. 2  illustrates an example design incorporating power information according to an embodiment of the present invention. The example design  200  includes four logic instances inst_A  204 , inst_B  206 , inst_C  212 , and inst_D  216 , a power manager instance pm_inst  218 , and a clock muxing logic  220 . Each design instance includes a set of input and output signals. The clock muxing logic  220  receives inputs clk and test_clk, and a control signal TM. Based on the control signal TM, the clock muxing logic selects clk or test_clk as its output, which is then fed to instances inst_A  204 , inst_B  206 , inst_C  212 , and inst_D  216 . 
         [0023]    As shown in  FIG. 2 , the example design includes four power domains. The top-level design (also referred to as top design) and the power manager instance pm_inst  218  belong to the default power domain PD 1   200 . Instances inst_A  204  and inst_B  206  belong to the power domain PD 2   202 . Instance inst_C  212  belongs to power domain PD 3   210 . Instance inst_D  216  belongs to power domain PD 4   214 . Table 1 shows the static behavior of the four domains according to embodiments of the present invention. 
         [0000]    
       
         
               
               
               
             
               
               
               
               
               
             
           
               
                   
                 TABLE 1 
               
             
             
               
                   
                   
               
               
                   
                 Power Mode 
                   
               
             
          
           
               
                 Power Domain 
                 PM1 
                 PM2 
                 PM3 
                 PM4 
               
               
                   
               
               
                 PD1 
                 ON 
                 ON 
                 ON 
                 ON 
               
               
                 PD2 
                 ON 
                 OFF 
                 OFF 
                 OFF 
               
               
                 PD3 
                 ON 
                 ON 
                 OFF 
                 OFF 
               
               
                 PD4 
                 ON 
                 ON 
                 ON 
                 OFF 
               
               
                   
               
             
          
         
       
     
         [0024]    The power manager instance (pm_inst)  218  generates three sets of control signals, namely pse_enable, pge_enable, and ice_enable, to control each power domain. Table 2 shows control signals of the power manager instance pm_inst  218  for controlling the four power domains according to embodiments of the present invention. 
         [0000]    
       
         
               
               
             
               
               
               
               
             
           
               
                   
                 TABLE 2 
               
             
             
               
                   
                   
               
               
                   
                 Power Control Signals 
               
             
          
           
               
                 Power 
                 power switch enable 
                 isolation cell enable 
                 power gating enable 
               
               
                 Domain 
                 (PSE) 
                 (ICE) 
                 (PGE) 
               
               
                   
               
               
                 PD1 
                 no control signal 
                 no control signal 
                 no control signal 
               
               
                 PD2 
                 pse_enable[0] 
                 ice_enable[0] 
                 pge_enable[0] 
               
               
                 PD3 
                 pse_enable[1] 
                 ice_enable[1] 
                 pge_enable[1] 
               
               
                 PD4 
                 pse_enable[2] 
                 ice_enable[2] 
                 pge_enable[2] 
               
               
                   
               
             
          
         
       
     
         [0025]    The following is an example netlist of a common power format (CPF) file of the top design according to an embodiment of the present invention. 
         [0000]    
       
         
               
             
           
               
                   
               
             
             
               
                 # Define top design 
               
               
                 set_top_design top 
               
               
                 # Set up logic structure for all power domains 
               
               
                 create_power_domain -name PD1 -default 
               
               
                 create_power_domain -name PD2 -instances {inst_A inst_B} \ 
               
               
                 -shutoff_condition {pm_inst.pse_enable[0]} 
               
               
                 create_power_domain -name PD3 -instances inst_C \ 
               
               
                 -shutoff_condition {pm_inst.pse_enable[1]} 
               
               
                 create_power_domain -name PD4 -instances inst_D \ 
               
               
                 -shutoff_condition {pm_inst.pse_enable[2]} 
               
               
                 # Define static behavior of all power domains and specify 
               
               
                 timing constraints 
               
               
                 create_power_mode -name PM1 -sdc_files ../SCRIPTS/cm1.sdc \ 
               
               
                 -activity_file ../SIM/top_1.tcf 
               
               
                 create_power_mode -name PM2 -off_domains 
               
               
                 PD2 -sdc_files ../SCRIPTS/cm2.sdc 
               
               
                 create_power_mode -name PM3 -off_domains {PD2 PD3} 
               
               
                 create_power_mode -name PM4 -off_domains {PD2 PD3 PD4} 
               
               
                 # Set up required isolation and state retention logic of all domains 
               
               
                 create_state_retention_logic -restore_edge {pm_inst.pge_enable[0]} \ 
               
               
                 -instances inst_A.reg_bank_1.out 
               
               
                 create_state_retention_logic -power_domain PD3 -restore_edge \ 
               
               
                 {pm_inst.pge_enable[1]} 
               
               
                 create_state_retention_logic -power_domain PD4 -restore_edge \ 
               
               
                 {pm_inst.pge_enable[2]} 
               
               
                 create_isolation_logic -from PD2 -isolation_condition \ 
               
               
                 {pm_inst.ice_enable[0]} -isolation_output high 
               
               
                 create_isolation_logic -from PD3 -isolation_condition \ 
               
               
                 {pm_inst.ice_enable[1]} 
               
               
                 create_isolation_logic -from PD4 -isolation_condition \ 
               
               
                 {pm_inst.ice_enable[2]} 
               
               
                   
               
             
          
         
       
     
         [0026]    In a normal design process, a low power design undergoes numerous iterations prior to final layout, and each step in this process has the potential to introduce logical errors. The methodology presented by the current invention can be employed to check functional equivalence of different versions of a low power design at these various stages and enables designers to identify and correct errors as soon as they are introduced. 
         [0027]    In addition, the method validates the insertion of state retention registers in the design netlist using user-defined mapping rules. These mapping rules are validated during an equivalence checking run. The method also models level shifters and isolation cells as domain anchor points (compare points) during equivalence checking to detect whether logic gates have erroneously crossed domain boundaries from one version of the netlist to another. 
         [0028]      FIG. 3  illustrates a method for conducting equivalence checking according to an embodiment of the present invention. In this example, the original RTL netlist  302  and a CPF file  304  are used to generate a reference low power RTL netlist  308  representing the design specification and a low power gate netlist  312  representing design implementation for equivalence checking. In this approach, first, the original RTL netlist  302  and a CPF file  304  are processed (in block  306 ) to generate a reference low power RTL netlist  308 , which represents the design specification. The original RTL netlist  302  and the CPF file  304  are processed by a synthesis tool  310  to generate a low power gate netlist  312 , which represents the design implementation. Then, EC is conducted between the low power RTL netlist  308  and the low power gate netlist  312  for design verification. 
         [0029]    In one embodiment, the method and system for equivalence checking and for verifying power requirements of a low power design may be implemented using a computer system. The computer system may include one or more central processing units (CPUs), at least a user interface for displaying computation results and circuit schematics, a memory device, a system bus, and one or more bus interfaces for connecting the CPU, user interface, memory device, and system bus together. The computer system also includes at least one network interface for communicating with other devices on a computer network. In alternative embodiments, much of the functionality of the method and system for equivalence checking and for verifying power requirements of a low power design may be implemented in one or more application-specific integrated circuits (ASICs) or field-programmable gate arrays (FPGAs), thereby either eliminating the need for a CPU, or reducing the role of the CPU. 
         [0030]    The memory device may include high-speed random-access memory and may also include non-volatile memory, such as one or more magnetic disk storage devices. The memory device may also include mass storage that is remotely located from the CPU(s). The memory device preferably stores:
       an operating system that includes procedures for handling various basic system services and for performing hardware-dependent tasks;   databases for storing information of the circuit;   application programs for performing other user-defined applications and tasks; and   an integrated sizing, layout, and extractor program for designing the circuit.       
 
         [0035]    The database, the application programs, and the integrated sizing, layout, and extractor program may include executable procedures, sub-modules, tables, and other data structures. In other embodiments, additional or different modules and data structures may be used, and some of the modules and/or data structures listed above may not be used. 
         [0036]    The CPF file may be used throughout the design automation tool flow, such as verification, synthesis, test, physical synthesis, routing, etc. Examples of commercial tools that support the CPF file include Conformal, RTL Compiler, SoC Encounter, Encounter Test, and NCSim Simulator from Cadence Design Systems, Inc. 
         [0037]      FIG. 4  illustrates a flow diagram for processing CPF commands to generate a reference low power RTL netlist according to an embodiment of the present invention. In this exemplary flow diagram, the method starts in block  402  and thereinafter moves to block  404  where the method reads the RTL netlist and the CPF command file. In block  406 , the method gets the next command in the CPF file and processes the CPF command which may annotate the low power information or create the low power logic in RTL design. 
         [0038]    In block  408 , a first determination is made as to whether the CPF command is a define-low-power-cells command. If the CPF command is not a define-low-power-cells command ( 408 _No), the method moves to block  412 . In the alternative, if the CPF command is a define-low-power-cells command, the method continues in block  410  where the method annotates the low power cells in RTL netlist or library. After completing annotating low power cells in block  410 , the method continues in block  426 . Examples of CPF commands that define low power cells are define_isolation_cell, define_level_shifter_cell, define_state_retention_cell, etc. 
         [0039]    The define_isolation_cell command identifies the library cells that can be used as isolation cells. It also allows the method to identify the instances of isolation cells in RTL where library files are not used. An exemplary syntax of the define_isolation_cell command is shown below. 
         [0000]    
       
         
               
               
             
           
               
                   
                   
               
             
             
               
                   
                 define_isolation_cell 
               
               
                   
                 -cells cell_list [-libraries library_list] 
               
               
                   
                 [{-power_switchable LEF_power_pin | -ground_switchable 
               
               
                   
                 LEF_ground_pin} 
               
               
                   
                 -power LEF_power_pin -ground LEF_ground_pin] 
               
               
                   
                 [-valid_location { from | to}]  -enable pin 
               
               
                   
                   
               
             
          
         
       
     
         [0040]    The define_level_shifter_cell command identifies the library cells that can be used as level shifter cells. It also allows the method to identify the instances of level shifter cells in RTL where library files are not used. An exemplary syntax of the define_level_shifter_cell command is shown below. 
         [0000]    
       
         
               
               
             
           
               
                   
                   
               
             
             
               
                   
                 define_level_shifter_cell 
               
               
                   
                 -cells cell_list [-libraries library_list] 
               
               
                   
                 -input_voltage_range {voltage | voltage_range} 
               
               
                   
                 -output_voltage_range {voltage | voltage_range} 
               
               
                   
                 [-direction {up|down|bidir}] [-output_voltage_input_pin pin] 
               
               
                   
                 { -input_power_pin LEF_power_pin [-output_power_pin 
               
               
                   
                 LEF_power_pin] 
               
               
                   
                 | [-input_power_pin LEF_power_pin] -output_power_pin 
               
               
                   
                 LEF_power_pin } 
               
               
                   
                 -ground LEF_ground_pin 
               
               
                   
                 [-valid_location { from | to}] 
               
               
                   
                   
               
             
          
         
       
     
         [0041]    The define_state_retention_cell command identifies the library cells that can be used as state retention cells. In addition, it allows the method to identify the instances of state retention cells in RTL where library files are not used. An exemplary syntax of the define_state_retention_cell command is shown below. 
         [0000]    
       
         
               
               
             
           
               
                   
                   
               
             
             
               
                   
                 define_state_retention_cell 
               
               
                   
                 -cells cell_list [-libraries library_list] 
               
               
                   
                 [-clock_pin pin] 
               
               
                   
                 -restore_function expression [-restore_check expression] 
               
               
                   
                 [-save_function expression] [-save_check expression] 
               
               
                   
                 [ {-power_switchable LEF_power_pin | -ground_switchable 
               
               
                   
                 LEF_ground_pin} 
               
               
                   
                 -power LEF_power_pin -ground LEF_ground_pin ] 
               
               
                   
                   
               
             
          
         
       
     
         [0042]    In block  412 , a second determination is made as to whether the CPF command is an identify_power_logic command. If the CPF command is not an identify_power logic command ( 412 _No), the method moves to block  416 . In the alternative, if the CPF command is an identify_power_logic command ( 412 _Yes), the method continues in block  414  where the method annotates the low power logic in RTL netlist. After completing annotating low power logic in block  414 , the method continues in block  426 . The identify_power_logic command identifies any isolation logic instantiated in RTL that is implemented through regular cells (non-library cells), and is not defined through the define_isolation_cell command. An exemplary syntax of the identify_power_logic command is shown below. 
         [0000]    
       
         
               
               
             
           
               
                   
                   
               
             
             
               
                   
                 identify_power_logic 
               
               
                   
                 -type isolation 
               
               
                   
                 -instances instance_list 
               
               
                   
                   
               
             
          
         
       
     
         [0043]    In block  416 , a third determination is made as to whether the CPF command is a create_power_domain command. If the CPF command is not a create_power_domain command ( 416 _No), the method moves to block  420 . In the alternative, if the CPF command is a create_power_domain command ( 416 _Yes), the method continues in block  418  where the method annotates the boundary ports of the low power domains. After completing annotating boundary ports in block  418 , the method continues in block  426 . The create_power_domain command creates a power domain and specifies the instances and top-level ports that belong to this power domain. By default, instance inherits the power domain setting from its parent hierarchical instance or design. An exemplary syntax of the create_power_domain command is shown below. 
         [0000]    
       
         
               
             
           
               
                   
               
             
             
               
                 create_power_domain 
               
               
                 -name power_domain 
               
               
                 { -default [-instances instance_list] 
               
               
                 | -instances instance_list [-boundary_ports pin_list] 
               
               
                 | -boundary_ports pin_list } 
               
               
                 [ -power_switchable_nets net_list | -ground_switchable_nets net_list] 
               
               
                 [ -shutoff_condition expression] 
               
               
                   
               
             
          
         
       
     
         [0044]    In block  420 , a fourth determination is made as to whether the CPF command is a create-low-power-logic command. If the CPF command is not a create-low-power-logic command ( 420 _No), the method continues in block  426 . In the alternative, if the CPF command is a create-low-power-logic command ( 420 _Yes), the method moves to block  422  where the method uses the annotated low power information to synthesize low-power logic into the RTL netlist. Examples of CPF commands that create low power logic include create_level_shifter_logic, create_isolation_logic, and create_state_retention_logic. 
         [0045]    In one example, the syntax of the create_level_shifter_logic command and the pseudo code for processing this command is listed below. 
         [0000]    
       
         
               
               
             
           
               
                   
                   
               
             
             
               
                   
                 create_level_shifter_logic 
               
               
                   
                 { -from power_domain | -to power_domain_list} 
               
               
                   
                 [-location {from | to} ] 
               
               
                   
                 [-cells cell_list] [-prefix string] 
               
               
                   
                   
               
             
          
         
       
     
         [0046]    1) If -from/-to option is specified,
       identify all the power crossing net pairs (“from” net and “to” net) that go from/to the specified Power Domain (PD) to/from any other PD       
 
         [0048]    2) Analyze the net pairs to determine insertion location(s) for Level Shifter (LS) cells
       LS cells are inserted at “from” net (output net of module) or at “to” net (input net of a module) depending on the voltage level required by the driven nets. The algorithm can be controlled to insert minimal number of LS cells between two power domains.       
 
         [0050]    3) Use LS cells from cell_list or pre-defined LS cells 
         [0051]    4) Insert the LS cells 
         [0052]    In another example, the syntax of the create_isolation_logic and the pseudo code for processing this command are shown below. 
         [0000]    
       
         
               
             
           
               
                   
               
             
             
               
                 create_isolation_logic 
               
               
                 -isolation_condition expression 
               
               
                 {-pins pin_list | -from power_domain_list | -to power_domain_list} ... 
               
               
                  [-exclude pin_list] [-location {from | to} ]  [-isolation_output 
               
               
                 {high|low|hold}] 
               
               
                 [-cells cell_list] [-prefix string] 
               
               
                   
               
             
          
         
       
     
         [0053]    1) If -from/-to option is specified,
       identify all the power crossing net pairs (“from” net and “to” net) which go from/to the specified Power Domains (PDs) to/from any other PD       
 
         [0055]    2) If -pins option is specified, identify all the power crossing net pairs such that the
       first net in each pair originates from the pin list   second net in each pair starts a new PD boundary       
 
         [0058]    3) Use expression to generate the logic for isolation condition which controls the output of the isolation cell, and integrate the isolation condition logic with the isolation cell and the power manager; 
         [0059]    4) Analyze the net pairs to determine insertion location(s) for Isolation (ISO) cells
       ISO cells are inserted at “from” net (output net of module) or at “to” net (input net of a module) depending on the logic value required at the driven nets. The algorithm can be controlled to insert minimal number of ISO cells between two power domains       
 
         [0061]    5) Use Isolation Cells (ISO) from cell_list or pre-defined ISO cells
       selection of isolation cells will depend on value of isolation_output and isolation_condition       
 
         [0063]    6) Insert the ISO cells 
         [0064]    In yet another example, the syntax of the create_state_retention_logic and the pseudo code for processing this command are shown below. 
         [0000]    
       
         
               
               
             
           
               
                   
                   
               
             
             
               
                   
                 create_state_retention_logic 
               
               
                   
                 { -power_domain power_domain | -instances instance_list } 
               
               
                   
                 -restore_edge expression [ -save_edge expression ] 
               
               
                   
                  [ -clock_gating_condition expression ] 
               
               
                   
                  [ -cell_type string ] 
               
               
                   
                   
               
             
          
         
       
       
         
           
             1) Identify all data storage element instances, such as D flip-flops (DFFs)/D latches (DLATs), in a specified power domain 
             2) Replace the normal DFFs/DLATs with state retention cells 
             3) Generate control logic for restore_edge/save_edge and stitch this control logic between state retention cell and power manager 
             4) Generate the control logic for clock_gating_condition and stitch this control logic between state retention cell and power manager 
           
         
       
     
         [0069]    In block  424 , the method integrates the low power logic created in block  422  into the RTL netlist. In block  426 , a fifth determination is made as to whether there are more commands in the CPF file to be processed. If there are more commands in the CPF file to be processed ( 426 _Yes), the method continues in block  406  and repeats the processing blocks between  406  and  424 . In the alternative, if there are no more commands in the CPF file to be processed ( 426 _No), the method goes to block  428  and ends the processing of the CPF commands. In another embodiment, the blocks  422  and  424  can be processed after the block  426 . Such an embodiment will involve processing all the commands specified in the CPF file before creating the low power logic, and integrating the created low power logic into the RTL netlist to generate the reference low power RTL netlist. 
         [0070]      FIGS. 5A-5E  illustrate insertion of low power logic in an exemplary design according to embodiments of the present invention. In  FIG. 5A , the exemplary design includes an instance of module M 1   502  residing in power domain  1  (PD 1 ), an instance of module M 2   504  residing in power domain  2  (PD 2 ), and an instance of module M 3   506  residing in power domain (PD 3 ). In this example, pin A of M 1   502  fans out to pin B of module instance M 2   504  of power domain PD 2  and to pin C of module instance M 3  of power domain PD 3   506 , respectively. The output net of M 1  (PD 1 ) is net 0 , the input net of M 2  (PD 2 ) is net 1 , and the input net of M 3  (PD 3 ) is net  2 . 
         [0071]    Referring to the example shown in  FIG. 5A , the pseudo code for inserting the level shifter logic using the CPF command create_level_shifter_logic -from PD 1  -location from is as follows. The design after insertion of level shifter logic is shown in  FIG. 5B .
       1) Since -from option is specified, get the appropriate power domain crossing net pairs, i.e., (net 0 , net 1 ) and (net 0 , net 2 )   2) Analyze the power domain crossing net pairs to determine insertion location(s) for level shifters
           LS cell cannot be inserted at net 0 , because it fans out to two different PDs   LS cells can be inserted at net 1  and net 2     
           3) Use LS cells from pre-defined LS cells, since -cell option is not specified   4) Insert LS cells at net 1  and net 2         
 
         [0078]    As shown in  FIG. 5B , a first level shifter cell LS 1   508  is inserted between M 1  (PD 1 )  502  and M 2  (PD 2 )  504 , and a second level shifter cell LS 2   510  is inserted between M 1  (PD 1 )  502  and M 3  (PD 3 )  506 . These level shifter cells are necessary to shift the voltage levels of signals going from one power domain (PD 1 ) to a different power domain (PD 2  or PD 3 ). 
         [0079]    In this example, a level shifter cell includes a buffer  511 , an input signal line  512 , a first power supply signal line (VDD 1 )  513  from power domain  1 , a second power supply signal line (VDD 2 )  514  from power domain  2 , and a level shifter output signal line  515 . After inserting the level shifter cells, the functionality of the design in low power mode is same as in normal operation mode. 
         [0080]    Since pin A of M 1  (PD 1 ) and pin B of M 2  (PD 2 ) belong to different power domains, the tool inserts the first level shifter cell at net 1 . Similarly, since pin A of M 1  (P 1 ) and pin C of M 3  (PD 3 ) belong to different power domains, the tool inserts the second level shifter cell at net 2 . Note that level shifter cells cannot be inserted at net 0 , because net 0  fans out to two different power domains. 
         [0081]    With respect to the example shown in  FIG. 5A , the pseudo code for inserting the isolation logic using the CPF command create_isolation_logic -isolation_condition !(iso_en) -pin M 1 /A -location from -isolation_output low is as follows. The design after insertion of isolation logic is shown in  FIG. 5C .
       1) Since, -pin option is specified,
           get the appropriate power crossing net pairs, i.e., (net 0 , net 1 ) and (net 0 , net 2 )   
           2) An inverter with iso_en as input (from power manager) is created to generate the signal isolation condition (iso_cond). The output (iso_cond) then feeds the isolation condition signal of the ISO cells.   3) Analyze the net pairs to determine insertion location(s) for ISO cell
           ISO cell can be inserted at net 1  and net 2 , or   ISO cell can be inserted at net 0  (minimizes usage of ISO cells)   
           4) Use ISO cells from pre-defined ISO cells, since -cell option is not specified   5) Use an AND gate for ISO cell from pre-defined ISO cells, since isolation_output value is low (i.e. 0), and the isolation_condition value is 0 when iso_en is enabled (i.e., 1)   6) Insert ISO cell at net 1  and net 2  (ISO cell insertion is not minimized).       
 
         [0091]    As shown in  FIG. 5C , a first isolation cell ISO 1   516  is inserted between M 1  (PD 1 ) and M 2  (PD 2 ), and a second isolation cell ISO 2   518  is inserted between M 1  (PD 1 ) and M 3  (PD 3 ). For example, when PD 2  is powered on and PD 1  is switched off, the tool needs to insert isolation cell at net 1  so that the logic value at net 1  is 0. Similarly, when PD 3  is powered on and PD 1  is switched off, the tool needs to insert isolation cell at net 2  so that the logic value at net 2  is 0. In another implementation, the tool may insert a single isolation cell at net 0 , which may serve the same purpose as the two isolation cells shown in  FIG. 5C , and thus minimizes the number of isolation cells used. 
         [0092]    In this example, an isolation (ISO) cell includes an AND gate  519 , an input signal  520 , an isolation condition signal  521 , and an isolation output  522 . Note that iso 1 _cond and iso 2 _cond are signals representing the isolation condition for enabling isolation cells. The iso 1 _cond and iso 2 _cond are in turn driven by the iso_en signal from the power management module. In the above example iso 1 _cond and iso 2 _cond represent the same signal. In general, iso_cond is derived from the iso_en signal. In addition, after inserting the isolation cells, the functionality of the design in low power mode is different from normal operation mode. 
         [0093]      FIG. 5D  illustrates another exemplary design of low power logic for equivalence checking according to embodiments of the present invention. In  FIG. 5D , a first isolation cell ISO 1   523  and a first level shifter cell LS 1   524  are inserted between M 1  (PD 1 ) and M 2  (PD 2 ). A second isolation cell ISO 2   525  and a second level shifter cell LS 2   526  are inserted between M 1  (PD 1 ) and M 3  (PD 3 ). 
         [0094]      FIG. 5E  shows a variation of the exemplary design of  FIG. 5D . In  FIG. 5E , the locations of the first level shifter cell LSI  527  and the first isolation cell ISO  528  are switched as compared to  FIG. 5D . Similarly, the locations of the second level shifter cell LS 2   529  and the second isolation cell ISO 2   530  are switched as compared to  FIG. 5D . 
         [0095]    There are a number of functionalities provided by the methodology of the present invention. First, the method enables EC of low power designs between a reference low power RTL netlist and a low power gate netlist. It is able to verify that the low power logic has been synthesized correctly by the synthesis tool in the RTL to gate synthesis. The method is employed to EC the entire chip functions, including normal functions and the low power functions. It provides an automatic EC flow without the need to manually apply constraints to the low power gate netlist. 
         [0096]    The use of the CPF file provides a common source for realizing the low power logic in the reference low power RTL netlist and the low power gate netlist. In addition, the CPF file reinforces EC capabilities in verifying low power logic, such as checking one to one mapping of all isolation cells and level shifter cells between the reference RTL netlist and the lower power gate netlist, and checking for functional equivalence (normal function and low power function) for each power domain between the reference RTL netlist and the lower power gate netlist. 
         [0097]      FIG. 6  illustrates a method for verifying power specifications of a low power design according to an embodiment of the present invention. As shown in  FIG. 6 , the pre-synthesis verification of power requirements  602  and post-synthesis verification of power requirements  604  blocks are added to  FIG. 3  as discussed above. The descriptions for blocks  302 ,  304 ,  306 , and  308  remain the same as in  FIG. 3 . This approach allows a front-end design engineer to verify whether the power requirements of the design is complete, consistent, and compatible before passing the design to an back-end design engineer. By using the pre-synthesis verification  602  and post-synthesis verification  604  processes, the front-end design engineer can fix and debug the power requirements using the RTL netlist  302 , the CPF file  304 , and the reference low power RTL netlist  308 . These verification methodologies are more efficient than the conventional methods of verifying power requirements using a gate-level netlist of the design. 
         [0098]    In the pre-synthesis verification of power requirements  602 , the compatibility and consistency of the power requirements are verified. Note that the pre-synthesis verification discussed below may also be conducted after the reference low power RTL netlist  308  has been generated. For example, the following conditions are checked for compatibility using the RTL netlist  302  and the CPF file  304 :
       The method checks the same crossing net that have multiple isolation rules apply to it. It ensures that these rules are either compatible or complementary with one another, and they do not conflict with each other. This is done by 1) collecting set of isolation rules that apply to the same net; and 2) checking if the location and type of the isolation cell specified in each rule match.   The method checks instances with multiple power domains, when a list of instances is specified in the create_power_domain. This is done by marking the instances as having been assigned to the power domain. If an instance has already been marked as belonging to another power domain, then it is flagged as an error.   The method checks if an isolation condition covers the corresponding shutoff condition of a source domain. The isolation condition should be a superset of the shut-off condition, since the isolation condition is required to support the shut-off condition.       
 
         [0102]    In addition, the method for verifying power specifications of a low power design also includes checking for consistency of the options and arguments of a power requirement command in the power specification file. For instance, the following are some exemplary checks conducted for a cell isolation rule:
       Both -pins and -from options are specified but at least one pin in the pin list is not driven by a power domain in the power_domain_list argument specified with the -from option.   Both -pins and -to options are specified but at least one pin in the pin list is not driving logics that belong in a power domain that is not in the power_domain_list argument specified with the -to option.   Both -from and -to are specified but there is no signal coming from a power domain in the power_domain_list argument specified with -from flag and then ending at a power domain in the power_domain_list argument specified with the -to option.   All three options -pins, -from and -to are specified but at least one pin in the pin list that is either not driven by a power domain in the -from power_domain_list argument or not driving logic elements that belong in a power domain that is not in the power_domain_list argument specified with the -to option.   Both -pins and -exclude arguments are specified but all pins in the pin list are excluded.   The usage of a low power cell is consistent with both its location and its specification of the create_isolation_rule location.   The instances named by identify_power_logic as instances of standard isolation cells can actually be used for isolation. If it is already a dedicated isolation cell, then issue a warning that this command is redundant.       
 
         [0110]    In the post-synthesis verification of power requirements  604 , the completeness of the power requirements is verified. For example:
       There should be at least one isolation rule that covers every power domain net crossing where one of the domains can be shutoff.   There should be at least one level shifter rule that covers every power domain net crossing between two domains with different voltages.   There should be at least one isolation rule which have been updated using the combine_level_shifting option, when there is a crossing between two domains of different voltages and one or both of the domains can be shutoff.       
 
         [0114]    The method further uses the RTL netlist  302 , CPF file  304 , and the reference low power RTL netlist  308  to conduct other verification of the power domains, power switches, isolation cells, state-retention cells, level shifter cells, and always-on cells of the low power design. In one embodiment, the following exemplary power domain conditions are checked:
       Power domain of the instance is unknown   Unknown power domain for primary I/O pins   Instance with multiple power domains   Black box pins with multiple power domain       
 
         [0119]    In another embodiment, the following exemplary cell isolation conditions are checked:
       Isolation cell instance is not_required (i.e. redundant)   Source and destination domains are the same power domain (i.e. redundant)   Isolation cell output is floating   Power of isolation control pin can be OFF while isolation cell is ON   No valid isolation gates found (i.e. invalid cell)   Control pin reaches an invalid gate for isolation (i.e. invalid cell)   Data pin reaches a non-isolation gate (i.e. invalid cell)   Isolation cell instance is not in source, destination or global power domain (i.e. invalid instance)   Control pin is buffered (i.e. invalid instance)   Data pin is buffered (i.e. invalid instance)   Output pin is buffered (i.e. invalid instance)   Invalid isolation cell type (i.e. invalid instance)   Invalid isolation cell location (i.e. invalid instance)   Missing isolation cell   Isolation control limit is exceeded   Isolation cell control pin is not connected to the specified signal   Isolation cell does not match cells specified in the isolation rule   Multiple isolation rules match isolation instance   Isolation instance not found for pin specified in an isolation rule   Isolation instance control pin is connected with a wrong polarity       
 
         [0140]    In yet another embodiment, the following exemplary state retention conditions are checked:
       State retention cell normal power and data driving power are from different domains   Output of retention cell is floating   Retention control limit is exceeded   Retention cell control pin is not connected to the specified signal   Retention control signal controls unspecified retention cell instance       
 
         [0146]    In yet another embodiment, the following exemplary level shifter conditions are checked:
       Input connected to an incorrect voltage   Output connected to an incorrect voltage   Input-Output voltage combination is invalid   Missing level shifter   Redundant level shifter   Output of level shifter is floating   Back-to-back level shifters detected   Incorrect level shifter location       
 
         [0155]    In yet another embodiment, the following exemplary always-on cell conditions are checked:
       Always-on instance with floating outputs   Always-on instance drives non-power control net       
 
         [0158]    Upon performing pre-synthesis verification and post-synthesis verification of power requirements of the low power design, problems identified may be fixed by adding additional power requirements to the power requirement file, including the update_power_domain, update_power_switch_rule, update_isolation_rules, update_state_retention_rules, update_level_shifter_rules, and other power requirement commands. Note that the update_power_domain, update_power_switch_rule, update_isolation_rules, update_state_retention_rules, update_level_shifter_rules commands correspond to the create_power_domain, create_power_mode, create_isolation_logic, create_state_retention_logic, create_level_shifter logic commands respectively. 
         [0159]    In one example, the syntax of the update_power domain command and its corresponding options and arguments are shown below. The update_power_domain command specifies implementation aspects of the specified power domain. Note that at least one of the options besides -name needs to be specified, and several options may be used or combined. 
         [0000]    
       
         
               
               
             
           
               
                   
                   
               
             
             
               
                   
                 update_power_domain 
               
               
                   
                 -name domain 
               
               
                   
                 { -internal_power_net net | -internal_ground_net net 
               
               
                   
                 | -min_power_up_time float | -max_power_up_time float 
               
               
                   
                 | -pmos_bias_net net | -nmos_bias_net net | -user_attributes 
               
               
                   
                 string_list 
               
               
                   
                 | -rail_mapping rail_mapping_list -library_set library_set} 
               
               
                   
                   
               
             
          
         
       
       
         
           
             The -internal_ground net option specifies the main ground net for all functional gates in the specified power domain. 
             The -internal_power_net option specifies the main power net for all functional gates in the specified power domain. 
             The -library_set references the library set to be used to search for the specified power rails. It also specifies the library set name. 
             The -min_power_up_time option specifies the minimum time allowed for the power domain to ramp up. It specifies the time in the units defined by set_time_unit. 
             The -rimos_bias_net option specifies the net to be used to bias the n-type transistors of all functional gates in this power domain. 
             The -name option specifies the name of the power domain. 
             The -pmos_bias_net option specifies the net to be used to bias the p-type transistors of all functional gates in this power domain. 
             The -rail_mapping option specifies the mapping of the power rails in the library (.lib files) to the power and ground nets defined in the CPF file. One may use the following format to specify a rail mapping: {power_rail_name power or ground net}. 
             The -user_attributes option attaches a list of user-defined attributes to the domain. It specifies a list of strings. 
           
         
       
     
         [0169]    In another example, the syntax of the update_power_switch_rule command and its corresponding options and arguments are shown below. The update_power_switch_rule appends the specified rules for power switch logic with implementation information. 
         [0000]    
       
         
               
             
           
               
                   
               
             
             
               
                 update_power_switch_rule 
               
               
                 -name string 
               
               
                 { -enable_condition_1 expression [-enable_condition_2 expression]] 
               
               
                 | -acknowledge_receiver pin 
               
               
                 | -cells cell_list -library_set library_set 
               
               
                 | -prefix string 
               
               
                 | -max_peak_delta_voltage float 
               
               
                 | -max_average_delta_voltage float } 
               
               
                   
               
             
          
         
       
       
         
           
             The -acknowledge_receiver option specifies an input pin in the design which may be connected to an output pin of the power switch cell. 
             The -cells option specifies the name of the library cells that can be used as power switch cells. 
             The -enable_condition_ 1  (-enable_condition_ 2 ) option specifies the condition when the power switch should be enabled. The condition is a Boolean expression of one or more pins. If only -enable_condition_ 1  is specified, the expression is used as the enable signal for the enable pin(s) of the power switch cell. If both options are specified, the expression of the -enable_condition_ 1 , -enable — condition_ 2  will be used respectively as enable signal for the enable pin of stage  1  and stage  2  of the power switch cell. Note that if the specified power domain has a shutoff condition, the support set of this expression is a subset of the support set of the shut-off condition. 
             The -library_set option references the library set to be used to search for the specified cells. It specifies the library set name, and all matching cells will be used. 
             The -max_average_delta_voltage option specifies the maximum allowed average voltage change across a power switch due to resistive effects in volt (V). It has a default value of 0. 
             The -max_peak_delta_voltage option specifies the maximum allowed peak voltage change across a power switch due to resistive effects in volt (V). It has a default value of 0. 
             The -name option specifies the name of the power switch rule. The specified string may contain wildcards. 
             The -prefix option specifies the prefix to be used when creating this logic. 
           
         
       
     
         [0178]    In yet another example, the syntax of the update_isolation_rules command and its corresponding options and arguments are shown below. The update_isolation_rules command appends the specified isolation rules with implementation information. Note that at least one of the options besides -name needs to be specified, and several options may be used or combined. 
         [0000]    
       
         
               
               
             
           
               
                   
                   
               
             
             
               
                   
                 update_isolation_rules 
               
               
                   
                 -names rule_list 
               
               
                   
                 { -location {from | to} 
               
               
                   
                 | -cells cell_list -library_set library_set 
               
               
                   
                 | -prefix string 
               
               
                   
                 | -combine_level_shifting} 
               
               
                   
                 [-open_source_pins_only] 
               
               
                   
                   
               
             
          
         
       
       
         
           
             The -cells option specifies the names of the library cells that are used as isolation cells for the selected pins. By default, the appropriate isolation cells are chosen from the isolation cells defined with the define_isolation_cell command or from the library cells with isolation related library attributes. 
             The -combine_level_shifting option applies the specified rules when level shifter logic is needed. Whenever isolation logic is inserted for a given pin and a level shifter is also required for that pin, the tool uses a cell that has both functions. 
             The -library_set option references the library set to be used to search for the specified cells. It also specifies the library set name, and all matching cells that will be used. 
             The -location option specifies the power domain to which the isolation logic may be added. The ‘from’ argument stores the isolation logic with the instances of the originating power domain. The ‘to’ argument stores the isolation logic with the instances of the destination power domain, which is also the default argument. 
             The -names option specifies the names of the rules to be updated. The name may contain wildcards. 
             The -open_source_pins_only option limits the pins to be isolated to the open source pins that belong to a power domain that is switched off while the driver domain remains powered on. This implies that only those rules that were created with the -isolation_target option may be updated. 
             The -prefix option specifies the prefix to be used when creating the isolation logic. 
           
         
       
     
         [0186]    In yet another example, the syntax of the update_level_shifter_rules command and its corresponding options and arguments are shown below. The update_level_shifter_rules command appends the specified isolation rules with implementation information. Note that at least one of the options besides -name needs to be specified, and several options may be used or combined. 
         [0000]    
       
         
               
               
             
           
               
                   
                   
               
             
             
               
                   
                 update_level_shifter_rules 
               
               
                   
                 -name string 
               
               
                   
                 { -location {from | to} 
               
               
                   
                 | -cells cell_list -library_set library_set 
               
               
                   
                 | -prefix string } 
               
               
                   
                   
               
             
          
         
       
       
         
           
             The -cells option specifies the names of the library cells to be used to bridge the specified power domains. By default, the appropriate level shifter cells are chosen from the level shifter cells defined with the define_level_shifter_cell command or from the library cells with level-shifter related library attributes. 
             The -library_set option references the library set to be used to search for the specified cells. It also specifies the library set name, and all matching cells that will be used. 
             The -location option specifies where the level shifters may be stored. 
             The ‘from’ argument stores the level shifters with the instances of the originating power domain. The ‘to’ argument stores the level shifters with the instances of the destination power domain, which is also the default argument. 
             The -name option specifies the name of the level shifter rule. The specified string may contain wildcards. 
             The -prefix argument specifies the prefix to be used when creating this logic. 
           
         
       
     
         [0193]    In yet another example, the syntax of the update_state_retention_rules command and its corresponding options and arguments are shown below. The update_state_retention_rule command appends the specified rules for state retention logic with implementation information. By default, the appropriate state retention cells are chosen from the state retention cells defined with the define_state_retention_cell command or from the library based on the appropriate library attributes. 
         [0000]    
       
         
               
               
             
           
               
                   
                   
               
             
             
               
                   
                 update_state_retention_rules 
               
               
                   
                 -names rule_list 
               
               
                   
                 {-cell_type string | -cell libcell} 
               
               
                   
                 -library_set library_set 
               
               
                   
                   
               
             
          
         
       
       
         
           
             The -cell option specifies the library cell to be used to map the flops. 
             The -cell_type option specifies the class of library cells that can be used to map the flops. 
             The -library_set option references the library set to be used to search for the specified cell or specified cell type. It specifies the library set name. 
             The -names option specifies the names of the rules to be updated. The name may contain wildcards. 
           
         
       
     
         [0198]    The benefits of the current invention include at least: 1) minimizing silicon re-spin risk by providing complete certification coverage; 2) detecting low power implementation errors early in the design cycle; 3) reducing verification time significantly by verifying multimillion gate designs faster than traditional gate-level simulation; and 4) closing the RTL-to-layout verification gap. 
         [0199]    It will be appreciated that the above description for clarity has described embodiments of the invention with reference to different functional units and processors. However, it will be apparent that any suitable distribution of functionality between different functional units or processors may be used without detracting from the invention. For example, functionality illustrated to be performed by separate processors or controllers may be performed by the same processors or controllers. Hence, references to specific functional units are to be seen as references to suitable means for providing the described functionality rather than indicative of a strict logical or physical structure or organization. 
         [0200]    The invention can be implemented in any suitable form, including hardware, software, firmware, or any combination of these. The invention may optionally be implemented partly as computer software running on one or more data processors and/or digital signal processors. The elements and components of an embodiment of the invention may be physically, functionally, and logically implemented in any suitable way. Indeed, the functionality may be implemented in a single unit, in a plurality of units, or as part of other functional units. As such, the invention may be implemented in a single unit or may be physically and functionally distributed between different units and processors. 
         [0201]    One skilled in the relevant art will recognize that many possible modifications and combinations of the disclosed embodiments may be used, while still employing the same basic underlying mechanisms and methodologies. The foregoing description, for purposes of explanation, has been written with references to specific embodiments. However, the illustrative discussions above are not intended to be exhaustive or to limit the invention to the precise forms disclosed. Many modifications and variations are possible in view of the above teachings. The embodiments were chosen and described to explain the principles of the invention and their practical applications, and to enable others skilled in the art to best utilize the invention and various embodiments with various modifications as are suited to the particular use contemplated.