Formal Low-Power Verification of Power- Aware Designs



Introduction

Power reduction and management methods are now all pervasive in system- on-chip (SoC) designs. They are used in SoCs targeted at power-critical applications ranging from mobile appliances with limited battery life to big-box electronics that consume large amounts of increasingly expensive power. Power reduction methods are now applied throughout the chip design flow from architectural design through RTL implementation to physical design.

Power-Aware Verification Challenges

Power-aware verification must ensure not only that the power intent has been completely and correctly implemented as described in the Unified Power Format (UPF) specification [1] or the Common Power Format (CPF) specification [2] , but also that the functional design continues to operate correctly after the insertion of power management circuitry.

Power estimates are made at several stages in the design flow, with accurate estimates becoming available only after physical layout. Consequently, design changes such as RTL modifications and layout reworks ripple back and forth through the design flow. This iterative power optimization increases verification and debug effort, project risk, and cost. The objective is to achieve the target power consumption while limiting the cost of doing so.

The power management scheme

Initially, an implementation-independent functional specification is devised to meet product requirements. The functionality is then partitioned across hardware and software. An initial power management scheme can be devised at this architectural level, but it defines only which functionality can or should be deactivated for any given use case, not how it should be deactivated. The functionality is then implemented in RTL, making extensive use and reuse of pre-designed silicon IP blocks, together with new RTL blocks. Some of these blocks may be under the control of software stacks.

At this stage, decisions are made about how functionality should be deactivated, using a multiplicity of power reduction methods to achieve the requisite low-power characteristics. These decisions must comprehend both hardware- and software-controlled circuit activity. Common power management methods include:

  • Clock gating
  • Dynamic voltage-frequency scaling (DVFS)
  • Power shut-off
  • Memory access optimizations
  • Multiple supply voltages
  • Substrate biasing

These early-stage power management decisions can be influenced by a physical floorplan, but they do not—and cannot— comprehend the final partitioning at P& R, where accurate power estimates are made. Consequently, the power management scheme can be modified and must be re-verified after P& R.

Clearly, the power management scheme is a moving target, and requires iterative design optimization, verification, and re-verification at every stage of the design flow—including architecture, RTL implementation, and physical design.

Additional complications

Implementing any scheme is often subject to significant additional complications, such as the impact of IP use and re-use and of DFT circuitry. A given IP block can implement several functions, each of which can be or must be switched off independently of the others, for example, by adding interfaces to the power-control registers or signals. These functions can be problematic in the case of third-party IP, where (often) only black box information about its behavior is available. In any case, the verification challenge now includes re-verifying the redesigned IP block(s) as well as verifying the power management circuitry.

In order to minimize test pattern count and test time, conventional DFT assumes that the whole chip operates with all functions up and running. That is how it operates not only on the tester, but also in field diagnostics. With power-aware design, DFT circuitry must now mesh with the design’s power management scheme in order to avoid excessive power consumption and unnecessary yield loss at final test.

Power-Aware Verification Requirements

Functional analysis, optimization, and verification throughout the design flow, complicated by inadequate visibility of third-party IP white-box functionality, mandates the following five principal requirements for implementing and verifying a low-power scheme:

  • Sufficiently accurate power estimates using representative waveforms, both pre- and post-route
  • Accurate visibility and analysis of the white box behavior of third-party IP prior to its modification and reuse
  • Deployment and ongoing optimization and verification of appropriate power reduction techniques, both pre- and post-integration
  • Exhaustive functional verification at the architectural and RT levels, both before and after the deployment of power optimization circuitry
  • Verification of hardware functionality compliance with software control sequences

The first requirement can be addressed with commercially available tools that use simulation and formal methods. The rest of this section deals with the remaining requirements.

As previously indicated, the power management scheme starts at the architectural level, so any available architectural features such as communication protocols must first be verified (see Figure 1).

Figure_1
Figure 1: Ongoing power-aware optimization and verification

In the subsequent functional implementation (RTL) flow, low-power management constructs are introduced at different phases in the SoC development, depending upon the data available and the optimizations required. Taking the deployment of power domains as an example, verification must ensure that:

  • Normal design functionality is not adversely affected by the addition of power domains and controls. “Before and after” checking is critical.
  • A domain recovers the correct power states at the end of the power-switching sequence, and generates no additional Xs at outputs or in given block signals.
  • It achieves a high level of coverage of power-up /power-down events, which are very control-intensive operations.
  • Switching off a power domain does not break connectivity between IP blocks.

Therefore, taking the RTL model verified prior to the insertion of power management circuitry as the “golden” reference model, power-aware verification requires a combination of:

  • Architecture-level verification
  • IP white-box functional visualization and analysis
  • Exhaustive functional verification
  • Sequential equivalence checking
  • Control and Status Register (CSR) verification
  • X-propagation analysis
  • Connectivity checking

Limitations of Traditional Power-Aware Verification

Various tools and approaches are used for power-aware analysis and verification. This patchwork of tools and approaches clearly provides limited analysis and verification capability, and demonstrably achieves inadequate QoR. Automated structural analysis and limited, manual functional analysis can identify potential opportunities for the use of power management circuitry. Such analysis can assure consistency between the RTL design and the UPF/CPF specification, but cannot verify design correctness. At the architectural level, power analysis usually is performed manually with spreadsheets.

Power-aware simulation is used at the RTL, but, like conventional simulation, is not exhaustive. This situation is exacerbated by the state space explosion resulting from the insertion of complex power management schemes. It not only significantly degrades simulation performance, but also fails to systematically avoid X optimism and pessimism.

Power-related DRC can enable limited power integrity analysis at the gate level.

Meeting Power-Aware Verification Requirements with JasperGold Apps

The JasperGold power-aware verification flow comprehensively meets power- aware verification requirements with the requisite QoR.

The front-end of the flow is the JasperGold LPV App (see Figure 2), which automatically creates power-aware transformations and automatically generates a power-aware model that identifies power domains, the power supply network and switches, isolation rules, and state retention rules. It does so by parsing and extracting relevant data from the UPF/CPF specification, the RTL code, and any user-defined assertions. It then automatically generates assertions that are used by other JasperGold Apps to verify that the power reduction and management circuitry conforms to the UPF/CPF specification and does not corrupt the original RTL functionality.

Figure_2
Figure 2: Jasper Gold power-aware verification flow

Power-aware model

The resulting power-aware model enables the analysis and verification of a wide-range of power management characteristics, for example:

  • Power-domain correctness, such as the absence (or otherwise) of clock glitches and correct operation of reset logic
  • Power state table consistency, analyzing all possible power-state transitions and detecting illegal ones
  • Retention cell verification, validating the integrity of saved data in all power states.
  • Power-supply network connectivity, to detect power intent errors made when defining the power-supply network
  • Power-aware correctness, ensuring equivalence between a power-aware design and the original RTL when all power domains are continuously on

LPV-generated assertions

Examples of assertions automatically generated by the JasperGold LPV App include:

  • Ensure that a power domain clock is disabled when the domain’s power supply is switched on or off
  • If a power supply net has resolution semantics, there is never more than one active driver
  • Ensure that the power supply of retention logic is on when the value of an element is restored from that logic
  • Whenever a power domain is powered down, all the isolation conditions related to this power domain are true before, during, and after power shut-off
  • No signal is isolated twice with contradictory clamp values

The JasperGold Apps approach

In contrast to the general purpose, all-in-one formal verification tool approach, the JasperGold Apps approach enables step-wise adoption of formal methods. Each JasperGold App provides all of the tool functionality and formal methodology necessary to perform its intended application-specific task. This approach requires design teams to acquire only the expertise necessary for the particular task at hand, and at a pace that suits the project requirements and user expertise.

Providing an empirical measurement on the effectiveness and progress of the formal verficiation, the JasperGold Design Coverage Verification (COV) App takes in the user’s RTL, assertion properties, and constraint properties and outputs a textual and GUI-based report showing how aspects of the DUT were verified by the formal analysis. These reports how lines of code (“statement coverage”), conditional statements (“branch coverage”), and functional coverage points that were exercised.

The JasperGold Formal Property Verification (FPV) App performs exhaustive verification of (a) all RTL functionality before the insertion of power management circuitry, and (b) the power management circuitry itself. For example, it analyzes and verifies power sequencing both during block design and after integration, including sequence safety such as clock deactivation, block isolation, and power down, as well as state correctness.

The JasperGold Control and Status Register (CSR) Verification App verifies that the design complies with the CSR specification, and that the value read from a register is always correct, both before and after power management insertion.

The JasperGold Sequential Equivalence Checking (SEC) App verifies the equivalence of blocks before and after power management circuitry is inserted, as well as those blocks subject to late-stage modification. In addition, it verifies that memory optimizations do not compromise functionality. For example, where a memory is replaced by two low-power memories with a wrapper, the JasperGold SEC App verifies that the two memory models are equiv- alent to the original memory.

The JasperGold X-Propagation App (XPROP) analyzes and verifies Xs at block outputs caused by power-down, and compares differences in output X behavior before and after application of the UPF/CPF specification.

The JasperGold Connectivity (CONN) Verification App exhaustively verifies RTL connections at the block and unit level, and after integration.

Conclusion

The Cadence JasperGold power-aware formal verification flow enables exhaustive analysis and verification of power-aware designs, achieving QoR superior to those designs produced by the traditional ad hoc patchwork of tools and approaches. Starting with the JasperGold LPV App to automatically generate a power-aware model and the appropriate assertions, the flow leverages an expandable range of additional JasperGold Apps, each targeted at a particular task. Design teams can deploy JasperGold Apps as needed and acquire expertise in a low-risk, step-wise fashion.

References and Further Information

[1] 1801-2013 – IEEE Standard for Design and Verification of Low-Power Integrated Circuits. Available at http://standards.ieee.org/findstds/standard/1801-2013.html.

[2] Si2 Common Power Format (CPF) Specification. Available at http://www.si2.org /?page=811.

To learn more about Cadence JasperGold Apps, contact your local sales office at http://www.cadence.com/cadence/contact_us

Contact Information

Cadence Design Systems, Inc.

2655 Seely Avenue
San Jose, CA, 95134
USA

tele: 408.943.1234
fax: 408.943.0513
www.cadence.com

Share and Enjoy:
  • Digg
  • Sphinn
  • del.icio.us
  • Facebook
  • Mixx
  • Google
  • TwitThis

Tags: