Power Aware Intent And Structural Verification Of Low-Power Designs

Power aware static verification, more popularly known as PA-Static checks, is performed on designs that adopt certain power dissipation reduction techniques through the power intent or UPF. The term static originates from verification tools and methodologies that applies a set of pre-defined power aware (PA) or multi-voltage (MV) rules based on the power requirements, statically on the structure of the design. More precisely, the rule sets are applied on the physical structure, architecture, and microarchitecture of the design, in conjunction with the UPF specification but without the requirements of any external stimulus or testbenches.

In this first part of a four-part series, we will describe the foundations of PA-Static verification and the solution features used for its verification.

Foundations of PA Static Verification
PA-Static verification is primarily targeted to uncover the power aware structural issues that affects design physically in architectural and microarchitectural aspects. The structural changes that occur in a PA design are mostly due to physical insertions of special power management and MV cells; such as power switches (PSW), isolation (ISO), level shifter (LS), enable level shifter ELS, repeaters (RPT), and retentions flops (RFF). These power management MV cells are essential for power-shutdown. The generic functionalities of these cells may be best summarized as follows:

List 1 – Generic Functionalities of Power Management and MV Cells

• Prevent inaccurate data propagation between Off and On power domains
• Provides accurate logic resolution between high-to-low or low-to-high voltage power domains
• Allows the control, clock, and reset signal to feed through Off-power domains
• Allows data and state retention during power Off or power reductions
• Provide primary power, ground, bias, related, and backup power connectivity

However, these features and functionalities mediated through MV cells are obtained at different levels of design abstraction. Further, these cells are defined through UPF strategies and Liberty libraries.

The fundamental technique that a PA-Static checking tool enforces to verify a design statically involves ascertaining the compliance of the MV or PA rules with the power intent or UPF specifications and Liberty libraries. Eventually, the tool performs all other possible syntax, semantic, and structural checks. Obviously all are based on internally integrated or pre-designed PA rules. There are also provisions to add custom rules based on demand, through an external interface of the tool through Tcl procedures. The PA rules are essential to verify or validate a design from RTL to PG-netlist, in conjunction with UPF and Liberty libraries, in the PA verification and implementation environment.

For different levels of design abstraction, the essential PA-Static checks can be best summarized by the following categories:

List 2 – Essential PA-Static Checks at Different Design Abstraction Levels
At RTL:

1. Power intent syntax and UPF consistency checks – for design elements, data, and control signals or ports against the design and UPF.
2. Power Architectural checks – for ISO, LS, ELS, RFF strategies against the power states or power state table definitions in UPF.

At GL-netlist:

3. Microarchitectural checks – for relative power on or always-on ordering of power domains for control signals, clocks, resets, etc., ensuring those are originated from relatively On- or always-on power domains and RPTs or feed-through buffers are present when passing through Off-power domains. These checks are performed against the design and UPF.

At both PG-netlist and GL-netlist:

4. Physical structural checks – for implemented PSW, ISO, ELS, LS, RPT, RFF against the UPF, specifications, Liberty libraries and MV or Macro cell inserted or instantiated design.

At PG-netlist:

5. PG-pin connectivity checks – for power-ground, bias, and backup power pins as well as identifying open supply nets and pins against the Liberty libraries, design, and UPF.

It is evident from the above categorization that PA-Static checks can start as early as the RTL, for consistency and architectural checks based on UPF specifications, and extend to the GL-netlist, for microarchitectural and physical structural checks.

The PG-pin connectivity checks can be performed only at the PG-netlist level. Although there are certain physical structural checks that are possible to accomplish only at the PG-netlist level, specifically PSW, RPT, etc. are usually implemented during the Place & Route (P&R) process, and the strategies physically become available for static checks only at the PG-netlist that is extracted from P&R.

Verification features
It is already distinct that PA-Static verification is mandatory for all stages of DVIF, along with PA-SIM. However, PA-Static verification provides more significant insight into the design at the GL-netlist and PG-netlist levels. This is because special power management MV and Macro cells are physically available in the design only at these netlist levels and provide detail of their PG connectivity.  PA-Static verification the input requirements for the tool are as follows:

List 3 – Input Requirements for PA-Static Verification

• The PA design under verification
• The UPF with proper definition of UPF strategies, power states, or a power state table
• PG-pin Liberty library for MV, Macro, and all other cells (specifically at or after the GL-netlist)

It is also important to mention here that the PA-Static checker optionally requires the PA Sim-Model library for MV and Macro cells for compiling purposes only, when these cells are instantiated in the design. The requirements of such model libraries are explained through the code snippet in Example 1.

Example 1 – PA-Static Tool Requirement of PA Sim-Model Library for Compilation Purposes

// The RTL design contains LS cell instantiated as follows:

     module memory (input mem_shift, output  mem_state);
     .....
Line 68                  LS_HL mem_ls_lh3 ( .I(mem_ shift), .Z(mem_state) );
     endmodule

// During compilation it is required to include the LS_LH module defined in (.v) file,

     `celldefine
     module LS_HL (input I, output Z);
     buf (Z, I);
     specify
     (I => Z) = (0, 0);
     endspecify
     endmodule
     `endcelldefine

Otherwise, the simulation analysis process will generate the following Error shown in Example 2:

Example 2 – PA-SIM Analysis Error during Compilation of the Design

** Error: memory.v(68): Module 'LS_HL' is not defined.

Here an LS LH_HL is instantiated in a design. The corresponding snippet of a model library and LS cell Liberty library is also presented.

The PA-Static checker tool actually analyzes the input information before conducting verification statically. The MV or PA rules applied to the design under verification are based on the following information, extracted and analyzed within the tool from the UPF, Liberty libraries, and the design itself, specifically when the design is at the GL-netlist after synthesis.

The PA-Static tool extracted and internally analyzed information can be summarized as follows:

List 4 – Summary of Information Analyzed by PA-Static Tool

• Power domains,
• Power domain boundary,
• Power domain crossings,
• Power states,
• ISO, LS, ELS, RFF, PSW, RTP, etc. UPF strategies,
• Cell-level attributes,
• Pin-level attributes (PG-pin only)

Recalling the create_power_domain –elements {} syntax and semantics from UPF LRM, the tool processes and creates the power domains based on the UPF definition and HDL hierarchical instances from the design. The fundamental concepts of power domains that specify and confine certain portions of a design or elements play a significant role in establishing connectivity for inter-domain and intra-domain communications.

The formation of power domains inherently defines its domain boundary and domain interface through the create_power_domain UPF command and option combinations. Specifically, power supply, power strategies, logic port and net connectivity, and subdomain hierarchical connections are established through the domain boundary and domain interface. Hence, the power domain boundaries are the foundation of UPF methodologies, based on which all UPF strategies and source-sink communication models are established.

The power domain crossings, which are more PA or MV terminology and relevant to the PA-Static tool, actually identify two or more relevant power domains that are communicating through HDL signal wires, nets, and ports. The power domain boundaries and their crossings actually formulate the source-sink communication model within the tool, not just considering HDL connectivity and hierarchical connectivity (HighConn and LowConn), but also coordinating other substantial factors defined within the UPF, design, and Liberty. These factors are the states of supply set or supply net, the states of the power domains, corresponding supply port and net names, as well as the combination of supply sets or supply nets for power domains that form different operating modes for the source-sink communication models or for the entire design.

The states of supply set, supply net, power domains, and their combinations that form the operating modes are composed from the add_power_state and PSTs that are usually constructed with the add_power_state, add_port_state, and add_pst_state semantics in UPF. The following examples show the pertinent components that facilitate forming the operating modes through power states as well as the power domain crossings that finally reinforce the source-sink communication models.

Example 3 – UPF Power States from PST for the Power Domain

set_scope cpu_top
create_power_domain PD_top
create_power_domain PD_sub1 –elements {/udecode_topp}

....

set_domain_supply_net PD_ top \
     -primary_power_net VDD \
     -primary_ground_net VSS

....

set_domain_supply_net PD_ sub1 \
     -primary_power_net VDD1 \
     -primary_ground_net VSS

create_pst soc_pt             -supplies          { VDD VSS VDD1}
add_pst_state ON  –pst soc_pt –state    { on  on  on}
add_pst_state OFF –pst soc_pt –state    { on  on   off}

Example 4 – UPF Power States from add_power_states for the Power Domain

add_power_state PD_top.primary
     -state {TOP_ON –logic_expr {pwr_ctrl ==1}
     {-supply_expr { ( power ==  FULL_ON, 1.0 ) && ( ground == FULL_ON ) }
     -simstate NORMAL}

add_power_state PD_sub1.primary
     -state {SUB1_ON –logic_expr {pwr_ctrl ==1}
     { -supply_expr { ( power == FULL_ON, 1.0 ) && ( ground == FULL_ON, 0 ) }
     –simstate NORMAL}

add_power_state PD_sub1.primary
     -state {SUB1_OFF –logic_expr {pwr_ctrl ==0}
     { -supply_expr { ( power == FULL_ON, 0 ) && ( ground == FULL_ON, 0 ) }
     -simstate CORRUPT}

Example 3 and 4 are based on the UPF 1.0 and UPF 2.1 LRM specifications respectively, and are alternates of each other, representing the same information in different releases or versions of the UPF. These examples explain that PD_sub1 and PD_top contain instances that are parent and child in the hierarchical tree; hence there is HDL hierarchical connectivity. As well, the power states and operating modes reveal that PD_sub1 has both the ON and OFF modes, whereas PD_top only has the ON mode. Hence cross power domain information is generated between PD_sub1 and PD_top within the tool. Also, recall that the UPF strategies (like ISO, LS, RFF, PSW etc.) are explicitly defined in UPF with relevance to particular source-sink communication models as shown in Example 5.

Example 5 – UPF Snippet for ISO Strategy and Corresponding Power Domain

set_isolation Sub1_iso  -domain PD_sub1  \
     -isolation_power_net VDD1 \
     -isolation_ground_net VSS \
     -elements {mid_1/mt_1/camera_instance}
     -clamp_value 0 \
     -applies_to outputs
set_isolation_control Sub1_iso  -domain PD_sub1 \
     -isolation_signal {/tb/is_camera_sleep_or_off_tb} \
     -isolation_sense high  \
     -location parent

In this example, the ISO strategy is applied at the boundary of the PD_sub1 power domain that implies a source. Obviously all signals from the domain boundary that propagate to any destination are implicitly becoming sinks; however, the source-sink model formation also coordinates with the power states as defined in Examples 3 and 4.

The last two items in List 4, the cell-level and the pin-level attributes, are very crucial information in PA-Static verification. Because, the cell-level attributes actually categorize a cell whether it is an ISO or LS or RFF etc. Hence it stands as a differentiator between a special power management MV cell and any regular standard cell.

The pin-level attributes, unlike the PA-SIM, PA-Static require only the PG-pin information, which are listed below.

List 5 – PG Pin-Level Attributes of Liberty Libraries

pg_pin,
pg_type,
related_power,
related_ground,
bias_pin,
related_bias,
std_cell_main_rail.

To note, that the other attribute, ‘power_down_function’ is exclusive for PA-SIM, and it is not required for PA-Static verification.

So once all these different categories of information are extracted and analyzed within the tool, the PA-Static verification or the checks can be started. As it is already clear that the static verification or checking criterion are different for different design abstraction levels; hence, the tool may conduct verification as early as from the RTL with only the first five of the seven analyzed information shown in List 4, (i.e., power domains, power domain boundary, power domain crossings, and power states). The last two, the cell and pin-level attributes, are mandatory for the GL-netlist and PG-netlist levels of the design.

Nevertheless, the static checks that are conducted at a higher level of design abstraction, such as the RTL, must be repeated exactly at lower levels; at the GL-netlist and PG-netlist levels on top of their own dedicated checks; just to ensure and achieve consistent PA-Static verification results throughout the entire verification process. However, conducting checks at RTL that are more appropriate for GL or PG-netlist will definitely not provide target results. This is because PA-Static checks at the RTL are limited to only the power intent syntax and UPF consistency checks and the power architectural checks for ISO, LS, ELS, and RFF strategy definitions, as noted in List 2.

In general, the PA-Static tool performs verification on the collected, extracted, and analyzed information along with the built-in MV or PA rules. The methodology that the tool imposes for matching the built-in MV or PA rules with the UPF specifications, physical design, library attributes, and analyzed information are based on the following aspects:

List 6 – PA-Static Rule vs UPF Specification Analytical Approaches

• UPF Strategy: PA rules imply to check if UPF strategy definitions are correct, incorrect, missing, or redundant.
• Power Management Special MV Cell: PA rules imply to check if special MV cells are correct, incorrect, missing, or redundant.

Alternatively, the checks are performed for cross comparing the above two in the following manner as well.

• UPF Strategies and MV Cell Cross Comparison: Whether the UPF strategies are present but cells are missing, or vice versa.

Here, the correct, incorrect, missing, and redundant cells for any of the above UPF Strategy or MV Cell aspects are not only for the syntax and semantics definition of MV cells and MV cell type checks, but are also responsible for checking the locations — including the domain boundary interface, ports, nets, and hierarchical instance path — where the strategies are applied or cells are actually inserted.

However, the tool sometimes may not perform checks on certain cases, specifically where the power states or PST states between any source-sink power domain communication models are missing. Hence, such situation are usually referred to as Not-Analyzed.

In addition, the PA-Static checker also requires conducting checks on the control and acknowledgement signals of these UPF strategies, like ISO, ELS, RFF, and PSW etc., specifically to ensure that control signals are not originated from relatively OFF power domains instead of the locations where the strategy is applied or cells actually reside. Besides, it is also required to confirm following aspects for the control signals:

List 7 – PA-Static Check Requirements for the UPF Strategy’s Control Signals

• Must not cross any relatively OFF power domains,
• Must not originate or driven from any relatively OFF power domain,
• Must not propagate unknown values,
• Possess the correct polarity, and
• Reachable.

As well, it is also required to perform checks on the strategies to ensure that:

• Strategies are not applied and MV cells are not physically inserted on the control signal path of another MV cell, or
• On any control signal paths of the design, like the scan control.

Further, it need to ensure that the MV cells are not inserted:

• On or before any combinational logics on a source-sink communication path, design clock, design reset, pull-up and pull-down nets, as well as on nets or ports with constant values specifically at the RTL, which may become pull-up or pull-down logic later in synthesis.

It is also worth mentioning here that the PA-Static checks at the RTL for physical presence of MV cells, their types (AND, OR, NOR, Latches), or their locations will generate false erroneous results.

This is because such cells are available only after synthesis or only if they are manually instantiated as Mixed-RTL. Although a PA-Static checker provides options for virtually inferring cells at the RTL as appropriate, based on UPF definitions and tool internal analytical capabilities, it may be worth either ignoring or switching off such design checks or inferring options and focusing on categorized checks for RTL, as listed in List 2.

In this article, Part 1 of a four-part series, we examined the foundations and verification features of PA static verification. In Part 2, we will discuss the features of the static verification library and describe best static verification practices.