Delicate Balance

Optimizing power in complex devices is much simpler using formal verification techniques.


By Joe Hupcey III
It’s not surprising that power optimization is a critical part of today’s complex designs. Unbeknownst to most consumers is an underlying methodology that every design engineer must follow to make sure a consumer device meets the power requirements of the consumer—even if the consumer doesn’t realize they’re demanding it.

The situation in industrial products, such as servers and routers in cloud computing data centers, is equally acute. Running at lower power can save millions of dollars in electricity consumption and reduced HVAC capacity. Without a solid power optimization methodology, today’s devices would be stuck in the proverbial “stone ages,” with extremely limited functionality, painfully short battery life, and/or huge electricity and cooling bills. Therefore, without a solid power-aware design methodology, engineers could not deliver electronic devices that perform the necessary tasks users demand from their electronic devices.

To get the desired power intent, designers must strike a precise balance of power usage throughout the device. The design and verification engineer need to address whether the inserted power management circuitry functions correctly, as well as making sure the overall chip functionality is not corrupted by the power intent described in the UPF or CPF descriptions. 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:

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

Traditional power-aware verification has been done with a patchwork of tools and approaches, which only provide limited analysis and verification capabilities and achieve inadequate quality of results (QoR).
A formal power-aware verification flow, in contrast, comprehensively meets power-aware verification requirements with the requisite QoR.
The front-end of the flow should automatically create power-aware transformations and generate a power-aware model that identifies power domains, the power supply network and switches, isolation rules and data retention rules. That requires parsing and extracting relevant data from the UPF/CPF specification, the RTL code and any user-defined assertions.

It then must automatically generate assertions to verify the interplay between design elements defined in the power description (e.g., isolation cells) and design elements defined in the RTL description (e.g., clock & control signals). It helps if the app is automated, outputting a report that summarizes which DUT elements satisfy or violate a particular property.

Additionally, the power-aware design database and assertions generated by the app can be used to verify the power reduction and management circuitry conforms to the UPF/CPF specification and does not corrupt the original RTL functionality. Other critical pieces include:

  1. Tools to analyze and verify architectural features that affect power-aware implementation, such as communication protocols;
  2. Behavioral indexing technology to analyze unfamiliar RTL blocks— such as third-party IP blocks—to understand their white-box behavior sufficiently to modify them reliably according to the power management scheme. That allows users to design, modify, and verify the RTL code throughout the design flow, and visualize the impact of the changes.
  3. Formal property verification to perform exhaustive verification of all RTL functionality before the insertion of power management circuitry, as well as the power management circuitry itself. This includes analyzing and verifying 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.
  4. Control and status verification to ensure the design complies with the control and status register (CSR) specification, and that the value read from a register is always correct, both before and after power management insertion.
  5. Sequential equivalence to verify the equivalence of blocks before and after power management circuitry is inserted, as well as those subject to late-stage modification. Memory optimizations also need to be checked to make sure they do not compromise functionality. For example, where a memory is replaced by two low-power memories with a wrapper, the two memory models need to be equivalent to the original memory.
  6. X propagation to analyze and verify X’s at block outputs caused by power-down, as well as a comparison between output X behavior before and after application of the UPF/CPF specification.
  7. Connectivity verification to check RTL connections at the block and unit level, and after integration.

Formal verification offers the ability to accurately deliver the delicate balance of low power optimization that goes into creating a device that services all the functionality that consumers expect.

—Joe Hupcey III is director of product development at Jasper Design Automation.