Formal Verification for Challenging Low-Power Designs
Formal verification provides a complete and foolproof methodology to verify against functional failures in complex low-power designs.
Low-power designs have become ubiquitous in today’s world. Designers of consumer and mobile products create aggressive low-power designs to compete on extended battery life. Tethered device designers (e.g., servers and routers) want to reduce cost of ownership. Consumers are also more conscious of “green” design in every area of electronics. Today, low-power designs are so popular that nine of ten new designs implement one or more power management techniques. In fact, every consumer device employs low-power techniques such as clock gating, multiple threshold voltages, and power shut down.
Designers using advanced energy-efficient techniques increase the complexity of their designs. These techniques are defined at the architectural level and have a strong impact throughout the design process. Complexity induced by multi-power domain chips and advanced low-power techniques make verification a difficult task. For all these techniques, verification is becoming the biggest bottleneck.
Industry standards such as UPF and CPF help designers cope with these complexities, but still lag behind requirements. In this article we will discuss low-power design practices and changes required to achieve complete verification of such designs. Formal verification is essential for addressing these complexities and to obtain maximum verification confidence. This article also discusses requirements of a low-power verification approach and gives examples of how structural and temporal verification can be improved by using formal verification, with positive return on investment.
Low-Power Verification Complexity
The verification complexity of low-power designs comes from three main factors:
- Designs are becoming more complex due to high degree of system integration.
- The number of operating modes due to power management functions is increasing.
- Designs have complex power domains with nested and hierarchical power domains.
Consider the block diagram of a modern Smartphone in Figure 1.
The Smartphone chip contains a number of functional blocks such as graphics controller; A/V codecs; connectivity modules such as USB; memory interfaces such as SDRAM and Flash; receive/transmit unit; image processing engines; and an embedded microprocessor. Verification must ensure that all these components work together reliably at all times.
Additionally, a chip may have multiple operating modes. With ever-increasing power demands, chip designers are adding multiple operating modes to ensure lowest power when certain functional blocks are not needed. The following example is the operating mode table for the above chip with 9 operating modes for 5 different power domains (Figure 2).
The power domains are defined as the main processor, the transmit unit, display unit, image processing unit and the rest. The chip can operate in nine different modes as shown in Figure 2. The different modes are summarized as follows:
- Fully functional mode, where all the power domains are ON and working on full VDD
- A texting mode where the image processing and the rest are turned to a low voltage
- A phone mode when the transmit block is fully ON
- A PIM access mode when the image processing is turned off
- Camera mode when the image processing and the display units are ON
- Playback mode when the display unit is fully ON
- Game-playing mode when the processor and display units are turned ON
- A keep-alive mode when processor is ON and the transmit unit is in low voltage
- OFF mode when everything is turned OFF.
These numerous functional blocks and the interaction with the various power modes make verification an extremely arduous task. In his address at FMCAD 2009, Intel VP John Barton mentioned that the verification complexity of an i7 processor running iTunes was so large that many power modes were not verified.
Recent designs also capitalize on the design hierarchy to implement power management. Various blocks are designed hierarchically which enables better understanding of the design as well as easing the verification burden. Power domains are also constructed hierarchically. Thus power domains can reside within other power domains and the entire device can be controlled from the top level power domain. An example of such a chip is shown in Figure 3.
As low-power designs become more and more complex, designers are adopting better design practices that ease both implementation and verification. They combine all the power management functions within a single functional block called the power management unit (PMU). The PMU houses all the control signals and the associated logic for sequencing and controlling all the power domains. The structural elements like level-shifter cells and isolation cells are added into the power domains.
Today’s design methodologies make provisions for adding these cells logically during the architecture stages, but realize the actual physical cells at a much later implementation stage, like synthesis or physical optimization. Power domains are well defined so that their interactions can be made deterministic. Even though these changes appear common sense and should enable better low-power designs, the reality does not reflect this. Let us now examine the traditional verification methodologies and the changes needed to achieve complete verification.
Functional simulation makes use of vectors in order to test the system for the correct behavior and to weed out any faults. But for functional simulation to be effective, designers have to not only design the system carefully by specifying the passing conditions as well as documenting failures, but also carefully constructing the vectors to maximize coverage.
Advances in formal verification have enabled formal techniques to be used to shorten the verification cycle by eliminating the need for testbench development and easing some of the designer’s pain in rigorously specifying the system. Formal verification aids the power management verification as it deals with uncertainty exhaustively, as opposed to functional simulation. Formal verification builds hypotheses regarding the “good” conditions and “bad” conditions and attempts to prove if these hypotheses can be characterized as always true. Defects which cannot be found running many simulation cycles can easily be found using formal verification. In the next section, we will introduce formal verification concepts which are suited for verifying low-power designs with some examples.
Formal Verification for Low-Power Design
A PMU implements the low-power architecture for a chip. In order to design the PMU, architects have to make two decisions: which power technique(s) to use; and how to partition the design. For this, architects consider the overall power consumption of the chip for both average and instantaneous power; and the architectural worst case scenario for power. This is where formal verification techniques can be employed, as they can find the case in which the chip signals toggle the most or least.
Commonly used power techniques in any design are clock gating, power shut-down (power gating) and voltage scaling. Proper clock gating is necessary for data integration. If clock is not shut down properly for a piece of logic, the improper state signals and signal glitches can propagate and lead to data corruption as shown in the example (1) below:
In any design, verification of the PMU is the most important element. The PMU must be verified for the proper generation of control signals and the various power sequences that result in reliable operating modes. Today, most design verification solutions check these signals when they become active within the design blocks. Even though this method is accurate, it can lead to long design verification cycles due to the number of verification points in the design. A better methodology is to model the uncertainty in the delay through a concept called “jitter.”
The paper titled “Formal verification checks IC power reduction features” introduced the concepts of frequency and phase jitter for asynchronous clock verification. Frequency jitter is the variation of the ratio between fast clock and the slow clock in a defined range. Phase jitter is defined as the variation between data signal and clock signal within a clock period resulting in erroneous functionality. Along with these concepts, we need a third concept to ensure complete verification of low-power designs. It is called power supply jitter which is defined as the time period when a given power supply or sets of power supplies can vary, and any unintended change can result in functional errors. Usually, this will be several clock cycles long. Power supply jitter can be modeled by Jasper Design Automation’s proof accelerators. Let us examine the design failures that are typical for a low-power design and how they can be verified by the above concepts.
Low-Power Design Failure Mechanisms
Functional failures due to power management implementation can be grouped into two categories: structural failures and temporal failures.
Structural failures result when low-power techniques are incorrectly implemented by the designer. In order to verify the design for structural failures, the entire design needs to be taken into account. Such structural errors can be detected statically early in the design flow. These types of errors might seem trivial but their occurrence is very common and the consequences can be disastrous: ranging from functional bugs to electrical hazards. The failures could be further classified into:
- Missing low-power cells – The chip could be missing level shifters, isolation cells, retention cells, etc. These cells are critical for the proper implementation of power management and their absence can result in functional failures.
- Use of wrong cells – There could be the use of wrong cells such as wrong level shifters, wrong keeper cells, etc. Keeper cells provide input isolation to the shutdown power domains. Use of wrong keeper cells can result in wrong state when a power domain is powered up.
- Wrong order of protection cells – If there are a keeper cell and a level shifter cell connected in series, then the keeper cell should be placed before the level shifter to avoid electrical hazard conditions. Also, in case of back-to-back keeper cells, their ordering needs to be dependent on the hierarchy of the voltage domains they are placed in.
- Wrong physical location – There could be failures due to cells placed wrongly. For example, a cell belonging to power domain “A” could be placed in power domain “B” by automatic placers, making the logic fail if one of them is switched off. Synthesis optimizations can potentially move the cells around unless these cells are specified as “DONT_TOUCH.”
- Wrong signal / polarity connection – Final class of errors happens when the pins of low-power cells are connected to wrong signals. For example, an isolation enable signal may be connected to the power domain enable signal which may result in temporary logical errors during shutdown and permanent logic errors during wakeup.
Temporal failures are caused by incorrect sequencing of PMU-driven power control signals, e.g. power indicator, propagated resets, retention save and restore etc. The errors could be permanent or temporary depending upon when and how the failure mechanism gets activated. Temporal errors can be classified into the following:
- Clock interaction errors – A typical design may have a number of clock signals running at multiple frequencies. Since clock gating is the popular low-power design technique, low-power designs need to be verified for clock gating to be working. Failures can happen when clock gating is implemented incorrectly. For example, designers may have implemented a power saving scheme by which the clock is stopped in the middle of a pipeline computation due to invalid data. If the data is not flushed out before the computation resumes, the wrong data in the pipeline can result in functional failures. Understanding and modeling clock and phase jitter will help in verifying such failures.
- Power state errors – Power states are the various modes of operation as defined in the architecture. These are represented in a power-state table. They are a subset of all the states that the chip could be operating at. Designers have to verify if the states reachable are valid power states or not. Power supply jitter modeling is helpful in make this analysis.
- Power enable timing errors – This is a broad classification of errors which tries to model the timing dependencies of various power-enable signals. For example, isolation enable signal must be turned on before the shutdown enable signal and must be turned off only after the shutdown signal is restored. Power supply jitter must be modeled for the shutdown enable signal so that proper functionality can be assured. In this case, the modeling can be complicated enough to account for the physical topology and any timing delays through the network. This class of errors also represents errors due to wrong polarity of the enable signals. These errors are harder to find using conventional verification solutions.
- Power sequence errors – Errors when power supply is changing from one voltage to the other. A sequence error can also result from restrictions on which power states that a chip can traverse during power up and power down. Power supply jitter for the various power signals along with the defined power sequences could be used to verify the correctness of the design. This is represented by the Figure 5.
- Domain ordering errors - Ordering among voltage domains can be obtained from a power state table definition. Domain A is of the same order as domain B if and only if A and B are always at similar voltage states. If there is at least one power state where A is at a higher voltage state, and no power state where B is higher, A is of a higher order. Errors can happen if control signals of a higher order domain are routed through a domain of lower order.
- State retention errors – State retention errors are similar to clock interactions, when all state bits are not saved when a block goes to shutdown. There are a number of bits required to uniquely verify a particular state of the chip. If not all these bits are saved during shutdown, the chip when it is powered up could end up in an indeterminate or a wrong state. Moreover, within a state retention register, there may be multiple control signals to enable state retention. These signals have strict sequencing requirements, violation of which can lead to functional failure. The following example highlights the control signal sequencing requirements of a balloon-type state retention register.
Towards Complete Low-Power Design Verification
Formal verification verifies low-power designs against these functional failures. Formal verification provides a complete and foolproof methodology to verify against failures. We have applied all the above concepts to the following design.
This design has 4 power domains and domains A and C are within domain B. Power domains are turned on and off following the sequence mentioned in Figure 5. In this case, power domain B has a higher order than power domains A and C. EnA, EnB, EnC and EnD act as the enables for controlling the power turn on and off. Additionally, power domain C has state retention registers similar to Figure 6. SrC1 and SrC2 are the En1 and En2 respectively. Power domains A, B and C share a common clock Clk1 which can operate in two frequencies – 100 MHz and 200 MHz. When Clk1 is 100 MHz, the voltage is lowered from 1.2V to 1.0V.
Power domain D uses a clock Clk2 with a fixed frequency of 200 MHz and a voltage of 1.2V. This power domain could be turned off independently of A, B and C. Table 1 summarizes the operating states of the chip. There are 7 legal states out of 81 possible states (34) for this design.
With regards to state sequences, a state transition with only one power domain changing voltage is allowed, except to/from State 0 and to/from state 4. For example, State 2 to State 3 is not allowed. Same is the case for State 1 to State 5. The state transition diagram is shown in Figure 8.
Power up sequence for this design is when going from state 0 to state 1. It has to follow the following PDA-->PDC-->PDB. Power down sequence is !PDA-->!PDC-->!PDB. PMU generates additional control signals to control isolation cells and input keepers. Those complexities are not specified to focus on the PMU verification of the power management protocol.
All of the failure mechanisms described in the previous section are modeled in proof accelerators and verified against the design. Moreover, with the jitter concept, advanced formal verification systems can model the uncertainties due to various types of delays, which speed up verification. Figure 8 specifies the domain ordering for the design and proves that checks are not required for transition from A to C due to them being unrelated in nature. Figure 9 describes the formal verification temporal checks for the above design. These checks completely and formally verify this design for its correctness.
Formal verification is emerging as the appropriate solution for verifying several aspects of low power designs. Low- power design failures are caused by inherent design complexity interacting with multiple power modes for mitigating power consumption. Designers using simulation for verification often wonder if all the errors have been identified and fixed. Formal verification can help them in identifying all the issues due to low-power techniques and enable complete low-power design verification, including exhaustive PMU validation. Formal verification techniques are better than simulation for a number of temporal error classes because formal verification checks are often atomic in nature. They verify a whole class of errors with a few checks. Moreover, they are exhaustive and find all the errors in the design, unlike simulation. New concepts such as clock, phase and power supply jitter can help designers to model the design interactions efficiently. These models, along with easy debug and powerful formal verification engines can help to indentify all the design issues.
Saptarshi Biswas is an Applications Engineer with Jasper Design Automation. With six years experience in EDA and formal technologies in particular, he is committed to helping semiconductor companies achieve maximum ROI using Jasper’s formal solutions. Prior to Joining Jasper, he worked on low-power, front-end tool development for ArchPro (now Synopsys). Biswas started his career designing and verifying ICs at Texas Instruments, and holds a B Tech in Computer Science from IIT, Kharagpur.
Jasper Design Automation
- T.Hattori et.al, A Power Management Scheme Controlling 20 Power Domains for a Single-chip Mobile Processor, ISSCC, 2006
Formal verification checks IC power reduction features, Kavita Snyder, Craig Deaton, and Doug Smith, Jasper Design Automation, 09/03/2008, SCD Source (http://www.scdsource.com/article.php?id=309&page=2.)
Mountain View, CA