Formal methods for power-aware verification
The imperative for reducing power consumption now pervades application spaces ranging from mobile appliances with limited battery life to big-box electronics that consume large amounts of increasingly expensive power. Consequently, power reduction and management methods are now used extensively throughout the chip design flow from architectural design, through RTL implementation to physical design.
The design team must verify not only that the inserted power management circuitry functions correctly, but also that it does not corrupt the chip’s functionality. Ideally, the team would have power estimates early enough in the design flow to deploy and verify the appropriate reduction techniques, minimizing or even completely avoiding late-stage redesign. Generally, though, really accurate power estimates become available only at physical layout, where design changes — even small ones — ripple back through design flow. Consequently, power-aware design often requires iterative optimization up and down the flow. Moreover, because many optimizations are performed late in the design flow, verification effort and risk increase, and debug becomes even more tedious and time-consuming. Consequently, power-aware design can appreciably increase design and verification time and cost. The challenge is to achieve the target power consumption while limiting the cost of doing so.
Our ultimate objective is to verify not only the chip’s functionality, but also that we have completely and correctly implemented the power intent described in Unified Power Format (UPF) [1] or Common Power Format (CPF) [2] descriptions. This article concludes that an “apps” approach is the best way to apply formal methods to power-aware verification.
We first address the challenges in devising and verifying the power management scheme and power optimizations necessary to achieve this ultimate objective. Firstly, how is the power management scheme devised?
Power management scheme
Initially, the system architects devise an implementation-independent functional specification to meet the product requirements, and then partition the functionality across hardware and software. They may also devise an initial power management scheme at this architectural level. However, the architectural scheme defines only which functionality may or should be deactivated for any given use case, not how it should be deactivated.
Consequently, how it should be deactivated is decided at the RTL implementation stage by the RTL team, that is, by a different group of engineers. The team decides whether and how to use a multiplicity of power reduction methods such as power domains and clock gating to achieve the requisite low power characteristics. These decisions must comprehend both hardware- and software-controlled circuit activity. They then implement the functional hardware, making extensive use and reuse of pre-designed silicon intellectual property (IP) blocks, together with new RTL blocks, some of which are under the control of software stacks.
However, although the RTL team’s decisions may be informed by a physical floorplan, they do not (and cannot) comprehend the final partitioning at place and route (P&R), where accurate power estimates are made. A common outcome is that the power management scheme must be modified and re-verified after P&R.
Clearly, the power management scheme is a moving target, and requires design optimization, verification and re-verification at every stage of the design flow — architecture, RTL implementation and physical design. However, implementing any scheme is often subject to significant constraints, such as the impact on IP use and re-use and on the use of design-for-test (DFT) circuitry.
Other design factors
The impact on IP use and reuse
In an ideal power reduction world, there would be a dedicated IP block for any particular chip function. The power management scheme could then be implemented on an IP block basis. For instance, “switch off video streaming” is implemented simply by switching off the associated video processing and control blocks.
However, in the real world, a given IP block may implement several functions, so switching off the block would disable more than the one function that should be disabled. Therefore, the team must devise a means of switching off only part of the IP block, for example by adding interfaces to the power-control registers or signals. This can be problematic in the case of third-party IP, where the team may have only black box information about its behavior. In any case, the verification challenge now includes re-verifying the redesigned IP block(s) as well as verifying the power management circuitry.
The effects of design-for-test circuitry
Design-for-test circuitry (DFT) presents an additional complication. Conventional DFT assumes that the whole chip design operates with all functions up-and-running in order to minimize test pattern count and test time. 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 design requirements
The five principal design requirements for implementing and verifying a low power scheme (see Figure 1) are:
- Sufficiently accurate power estimations using representative waveforms, both pre- and post-route.
- Accurate analysis and visibility of the white box behavior of third-party IP prior to its modification and reuse.
- The deployment and ongoing optimization of appropriate power reduction techniques, both pre- and post-integration.
- Exhaustive functional verification at the architectural and RTL levels, both before and after the deployment of power optimization circuitry.
- Verification of hardware functionality compliance with software control sequences.
The first two requirements can be addressed using commercially-available tools that use simulation, formal methods and behavioral indexing. But how do we tackle the remaining three requirements?
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:
- 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.
How to apply formal methods
Formal methods are used throughout the design flow from architectural validation, through RTL implementation, to post-silicon debug — and this applies to power-aware verification, too (see figure 2).
The question is: what is the optimum approach for applying formal methods to power-aware verification? The traditional approach to using formal technology is to license a general purpose, all-in-one formal verification tool suite and acquire the broad and deep expertise to use it. However, many teams want to apply formal to only a subset of the verification challenges, then expand their formal capabilities later as the challenges expand and diversify [3].
The “apps” approach to formal verification supports this need [4]. An app targets an individual formal verification application. It provides all of the tool functionality and formal methodology necessary to perform its intended application-specific task, such as architectural validation and clock domain verification. This approach requires the user to acquire only the expertise necessary for the particular task at hand. JasperGold Apps can be applied throughout the power-aware verification flow, enabling the team to apply formal methods only as needed, and at a pace that suits the team’s project requirements and expertise.
That’s how you apply formal methods to power-aware verification.
About the author
Lawrence Loh is vice president of Worldwide Applications Engineering at Jasper Design Automation. Loh has been with Jasper for nine years. Prior experience includes verification and emulation engineering for MIPS, and Verification Manager for Infineon’s successful LAN Business Unit. Loh is a graduate of California Polytechnic State University (BSEE) and San Diego State for his MSEE. He holds four U.S. Patents on formal technologies.
References
[1] P1801 – Standard for Design and Verification of Low Power Integrated Circuits. IEEE.
[2] Si2 Common Power Format Specification (CPF)
[3] We need a simpler and faster approach to formal verification by Rajeev Ranjan. EE Times.
[4] Interoperable Application-Specific Solutions for Formal Verification Throughout the Design Flow. Jasper Design Automation.
If you enjoyed this article, you will like the following ones: don't miss them by subscribing to :
