Design Article
Tell us What You Think
We want to know what you thought about this Design. Let us know by adding a comment.
Formal methods for power-aware verification
Lawrence Loh
12/17/2012 10:42 AM EST
Optimization and verification
Ongoing optimization and verification
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.
In the RTL flow, low-power management constructs are introduced at different phases in the SoC development, depending upon the data available and the optimizations required. For example, the team may initially employ clock gating after devising the initial power architecture. They may then apply additional power- and/or clock-gating after generation of the initial power estimate. Usually, a power controller (hardware and/or software) is inserted to switch off different power domains or to control the voltages to individual domains. Verification must ensure, for example, that:
The verification solution
Any verification solution must address the following diverse needs:
Ongoing optimization and verification
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.
In the RTL flow, low-power management constructs are introduced at different phases in the SoC development, depending upon the data available and the optimizations required. For example, the team may initially employ clock gating after devising the initial power architecture. They may then apply additional power- and/or clock-gating after generation of the initial power estimate. Usually, a power controller (hardware and/or software) is inserted to switch off different power domains or to control the voltages to individual domains. Verification must ensure, for example, that:
- Normal design functionality is not adversely affected by the addition of power domains and controls.
- A domain recovers the correct power states at the end of the power-switching sequence. An incorrect sequence combined with dependencies between power domains may incorrectly turn on the clock before removing isolation, corrupting the retention register.
- 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.
The verification solution
Any verification solution must address the following diverse needs:
- Analyze and verify architectural features that affect power-aware implementation, such as communication protocols.
- Analyze and verify common power-aware transformations such as power domains, supply network and power switching, isolation and retention.
- Analyze unfamiliar blocks — such as third-party IP blocks — to understand their behavior sufficiently to modify them according to the power management scheme.
- Verify power-related blocks such as clock controllers.
- Perform X-propagation analysis to verify X’s at block outputs due to power-down; and compare differences in output X behavior before and after application of the UPF/CPF specification.
- Verify the sequential equivalence of (a) blocks subject to late-stage modification and (b) blocks before and after power management circuitry is inserted.
- Verify connectivity after integration, and ensure that the design complies with the control and status register (CSR) specification, both before and after power management insertion.
- Verify power sequencing during design and after integration, including (a) sequence safety such as clock deactivation, block isolation and power down, and (b) state correctness.
- Verify that memory optimizations do not compromise functionality. For example, where the original memory is replaced by two low-power memories with a wrapper, we need to verify that the two memory models are equivalent to the original memory.
|
|
|
|
|
Navigate to related information