Contributed Article
Formal verification checks IC power reduction features
By Kavita Snyder, Craig Deaton, and Doug Smith, Jasper Design Automation
09/03/08
With increasing densities and frequencies, power consumption has become a prevalent issue in design today. Dedicated power management schemes are designed into chips to conserve power consumed both statically and dynamically. Along with this comes the importance of verifying these power management schemes.
This article will examine the various issues and existing solutions surrounding the verification of power management schemes, and will discuss how SystemVerilog properties can be written for the formal verification of power management systems. This includes the verification of:
- Clock gating for power island power-down and power-up sequencing
- State and data retention
- Clock domain synchronization
- Clock domain data crossing synchronization
Lastly, this article will explore the emerging and evolving needs of IC designers facing ever-increasing consumer demands for greater speed and performance while balancing the need for power reduction now and in the future.
Types of power consumption
Traditionally, dynamic power has been the dominant concern for low-power CMOS design. Dynamic power (sometimes referred to as switching power) is the power consumed due to switching in the design. This power can be characterized as follows:
Figure 1 – Dynamic power
This power is directly proportional to the capacitance and frequency, and is proportional to the square of the voltage.
With the advancement of CMOS physical design, transistor channel widths have continued to shrink. With this comes the additional density of gates per square millimiter, as well as increased performance. Unfortunately, this has also caused a secondary element of power consumption, which has traditionally been ignored, but which has now become a dominant source of power consumption.
This secondary element is known as static or leakage power. It can be characterized as follows:
Figure 2 – Leakage power
Leakage power is the power consumed independently of switching in the design. In other words, leakage power is purely physical technology process dependent.
With gate channel widths greater than 90 nm, the leakage power consumption was minimal and could largely be ignored. With 90 nm gate channel widths technology, leakage power is approximately 30% of the power consumed.
With the latest 65 nm technologies, leakage power becomes the dominant power consumed in CMOS design. There is no easy formula to represent leakage power, but it is inversely proportional to the threshold voltage, which makes it directly proportional to performance, and it has a cubic dependency on Vdd. Therefore, as gate lengths get smaller, the power strategies must be devised to address static power consumption.
Methods of minimizing power consumption
There are some common methods for minimizing power consumption. Until recently, dynamic power was the focus in reducing overall power consumption. Despite lots of manual approaches, there are EDA tools available that focus on reducing the switching (or frequency) and reducing the voltage.
The most common approaches for reducing the switching are clock gating and data gating. The most common approach for addressing the voltage reduction involves manual/adaptive VDD scaling, along with using voltage islands. For static power, the approaches are many: power gating, input vector control (leveraging the stack effect), reverse body bias (RBB), variable thresholds CMOS (MTCMOS), multiple thresholds CMOS (MTCMOS), variable supply voltage. Of these, power gating is the functional approach that is most effective at limiting standby leakage.
Figure 3 – Power gating
With each of these approaches, however, come risks to the functionality of the design. For instance, clock frequency scaling introduces the possibility of issues in clock domain crossing, whereas power gating introduces the problems of undriven signals and loss of state. As a result, the challenge of verifying a given power management strategy lies not only in verifying that the strategy itself is implemented as intended, but in verifying that its side effects don’t adversely affect the overall functionality of the design.
The latter is by far the harder of the two tasks. With the addition of power management logic, it is possible to introduce unknown changes in functionality. Often these logical variances can manifest themselves in corner cases, so using traditional simulation-based verification can be inadequate to completely verify the design.
Formal verification for power management
There are two main tasks involved in verifying power management strategies:
1. Using low-level properties (properties that verify an implementation detail in the design) to verify that the clock/power sequencing is handled properly.
2. Using high-level requirements (end-to-end properties that verify a given functionality about the design - often these can be referred to as “specification-level properties”) to verify that the power management scheme doesn’t break the main functionality of the design.
For demonstration purposes, a design is assumed to have an island of logic called Power Island 1 with the following characteristics:
- Its power rail can be turned OFF or set at different voltage levels that allow the island to operate at different frequencies according to performance needs at any particular time.
- Power to the power island is switched ON in five time-sequenced steps to five separate parts of the island. This reduces the injection of switching spikes into the power rails, compared to what would occur if the whole island were powered on at the same time.
- The power island is only allowed to be powered down when operating in idle mode.
- The value of particular registered signals within the power island must be saved when powered down and then reinstated when power is restored. This reinstates the status of the power island when it was last powered down.
Verifying power-down
When Power Island 1 is operating in idle mode, and the value of island1_pwr_en goes low, then the three individual power enable signals within the power island logic must be turned off within four clock cycles, provided the island remains in idle mode -- that is, island1_idle_mode remains at logic 1.
Should the island become not idle, indicated by island1_idle_mode going to logic 0 during the four cycle power-down sequence, then the power down sequence is aborted and the five individual power enables must never actually be turned off.
This is realized by disabling the SystemVerilog property used to verify the power down sequence (Example 1).
Example 1 – Verifying power-down sequence requires disabling a property.
Verifying power-up sequence
The three separate power-on enable signals, island1_pwr_enbls[2:0], are turned ON in a timed sequence eight cycles apart to reduce power rail induced power surge spikes.
Example 2 shows a property where a rising edge on signal island1_pwr_en triggers the start of verifying the power-up sequence, while a falling edge on the same signal aborts the power-up sequence and disables the verifying property. The $rose and $fell SystemVerilog functions are used to detect the rising and falling edges on signal island1_pwr_en.
For this property, if the value of island1_pwr_en rises, and the power enables are turned OFF, then the power-on sequence begins. If the value falls while the power-on sequence is in progress, the power-on sequence is aborted.
Starting the first cycle after island1_pwr_en rises, the asserted property verifies the following assuming the sequence is not aborted:
island1_pwr_enbls[0] – Cycles 1-17 at logic 1.
island1_pwr_enbls[1] – Cycles 1-8 at logic 0. Cycles 9-17 at logic 1.
island1_pwr_enbls[2] – Cycles 1-16 at logic 0. Cycle 17 at logic 0.
Example 2 – Verifying power-up sequence. The same signal is used to trigger and disable a property.
The property shown in Example 2 is checking three signal values over 17 cycles. The three signals introduce three separate proof threads for the formal proof engines to prove. This fact, together with the fact the depth of the proof is 17 cycles, means this may not be the most efficient way to code this property for efficient proof. Such a property may formally prove quickly. However, if it doesn’t, the property might be better coded as multiple properties, where each property proves considerably faster. This is particularly useful for reducing regression proof run times.
In this case there are two options to make this particular property easier for the proof engines to prove:
- Code three separate properties, one for each bit of island1_subpwr_enbls.
- Code three properties, one for each stage of switching on an enable.
Split properties for this second option are shown in the Example 3. Note the actual assertion statements for these properties are not shown.
Example 3 – The three stages of the power-on sequence verified by three separate properties.
In many systems, the effect of the power management logic is intended to be orthogonal to that of the functional logic. That is, the functional logic should work the same whether the power management is enabled or not. This can be very difficult to verify, in that there are many corner cases created by the relative times at which power management may be invoked, such as the examples given here.
Traditional simulation-based approaches cannot cover or exercise every single potential corner case. Therefore, it is risky to rely only on such approaches to completely verify the power managed design. In order to fully verify that the power management scheme doesn’t break the functional logic, the safest approach is to:
- Prove that the functional logic (or some key portion of it) works as intended with the power management disabled.
- Model the effects of the power management scheme (clock effects, state loss, etc.) and re-prove that the functional logic still works as intended.
Obviously, this is a complex and challenging task, and only really bears fruit if full proofs can be obtained in both phases of the effort.
Clock domain synchronization/crossing
Problem: In designs containing multiple clock domains, functional errors may arise due to reconvergence, divergence, and data stability.
Solution:
- Capture design functionality as High Level Requirements (as normal)
- With logic belonging to more then one clock domain, you must verify the logic to behave correctly for all potential frequency and phase jitter conditions. The ratio between fast and slow clocks varies within a defined range instead of always being locked at the same value. This is known as frequency jitter. The data transfer at clock domain crossings can become non-deterministic due to many factors, such as signal propagation, flip-flop setup and hold times, metastability, and so on. This is known as phase jitter. Jasper Design Automation’s Proof Accelerator macro can model frequency and phase jitter issues arising from clock domain crossing and help exhaustively verify the logic at such domain crossings. Apart from this, it is impossible to verify such domain crossing logic exhaustively.
- Prove high-level requirements (HLRs) to verify that functionality is unaffected.
Clock gating
Problem: There are a variety of problems to be concerned about.
- Freezes: Clock gating must not occur during an ongoing operation or when another module is expecting a response. This typically requires feedback from random logic.
- Responsiveness: Design should wake up on external events.
- Multiple clock-gating domains: Generally requires multiple levels of gating hierarchy. The handshaking across domains can be complex.
Solution:
Gated clock verification can be done largely by proving the functional properties covering clock configurations such as:
- Rising edge, falling edge or both edge active clocks
- Clocks derived through gate enables or latch logic
- Multiple clocks with a known or unknown frequency factor between them
- Multiple clocks with or without phase relationships between the clocks
In addition, it may be productive to partition clock gating controls into request and grant and verify the clock controls independently of the module.
State retention
Problem: State retention devices are too large and slow to use for all flip-flops throughout a design. But for those important places where they are used, it is important to ensure that the power down state is properly preserved and properly restored.
Solution: Follow the steps below.
1. Capture design functionality as normal as High Level Requirements (HLRs)
2. Model state corruption introduced by power gating
3. Prove HLRs to verify that functionality is unaffected
The actual properties for state retention will be an adaption of the properties already shown for power sequencing.
Multicore, multi-voltage
Problem: In a multicore environment, putting individual cores into different power domains introduces new complexity into coherency verification. Coherence messages arriving from other non-sleep units need to be handled.
Solution: Traditionally, designers have put all the cores and L2 cache in the same power domain. However, verifying a design sharing an L2 cache with cores from different power domains can be done applying the following steps:
1. Capture coherence protocol functionality as normal into High Level Requirements (HLRs).
2. If possible, prove the coherence protocol without power management (sometimes it may not be possible to independently disable the power management).
3. Now, with enabled power management, prove HLRs to verify that functionality is unaffected. Here, using a liveness check is appropriate to ensure that enabling the power management does not create a deadlock in the coherence protocol.
Summary
Power management is a critical part of system design in today’s always-on, mobility-oriented world, and verifying the power management scheme is a critical part of any modern CMOS design.
In order to fully verify the power management scheme for a given design, it must be proven that the management scheme is implemented according to its spec and that it doesn’t interfere with the intended functionality of the system.
Proving that the power management scheme is implemented according to its spec is relatively easy, but proving that it doesn’t break the rest of the design can be quite challenging, in that it requires the ability to prove the overall design works as intended. Proving that the design works as intended is, in fact, possible. However, it requires a state-of-the-art formal tool that is capable of high-level, end-to-end proofs of properties that are readily correlated to the functional specification.
Kavita Snyder serves as director of field operations at Jasper Design Automation, and she has an extensive background in ASIC design and verification. She has managed field organizations in the past at CoWare, Atrenta, and Sequence Design. Prior to that, she has held technical application roles focusing on low power and verification.
Craig Deaton is senior methodologist at Jasper Design Automation. He was the key architect behind Jasper's freely available GamePlan™ Verification Planner, and is a strong advocate of verification planning in the global verification community. From 1993 until 2005, Mr. Deaton held positions of increasing verification responsibility at Texas Instruments. In his role as an ASIC verification engineer, he served on TI-wide methodology teams and was a key reviewer of new vendors and tools. He also served as the formal verification leader for TI Wireless in Dallas.
Douglas J. Smith currently works in the technical support organization at Jasper Design Automation. He has worked in chip design and EDA for more than 20 years. He has published many papers about chip design and is author of the book "HDL Chip Design."
Related articles