Page loading . . .

 Category: SOCcentral Feature Articles & Columns: Feature Articles: Thursday, March 05, 2015
Low-Power Design Applications for Formal Verification  
Contributor: Jasper Design Automation
 Printer friendly
 E-Mail Item URL

May 7, 2010 -- 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 the 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, however, 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. Formal verification is essential for addressing these complexities and to obtain maximum verification confidence.

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 (Figure 1).

Figure 1. Smartphone block diagram.

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.

In addition, 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. Figure 2 below is the operating-mode table for the above chip, with 9 operating modes for 5 different power domains.

Figure 2. Power domains and power modes for the Smartphone chip.

The power domains are defined as the main processor, the transmit unit, display unit, image processing unit and the rest. The 9 different modes for the above chip 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 (See Figure 3.).

Figure 3. Hierarchical power domains with dependencies.

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.

Traditional verification methodologies and the changes needed

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. Let's now look at the formal verification concepts suited to 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 the 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 using the concept of "jitter."

In an article entitled "Formal Verification Checks IC Power Reduction Features," Kavita Snyder, Craig Deaton and Doug Smith of Jasper Design Automation 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.

In addition to frequency and phase jitter, we need to consider power supply jitter. Power supply jitter 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's now 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. 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 shut-down 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 – Errors 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 wake-up.

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.

    Figure 4: In this example, the clock could be stopped when the data is in Stage 2. Clock restoration without considering the hold-time of Stage 2 could results in data corruption.

  • 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 in which the chip could be operating. Designers have to verify if the states reachable are valid power states or not. Modeling power supply jitter is helpful in making 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 shut-down signal is restored. Power supply jitter must be modeled for the shut-down-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 – These errors occur when the power supply is changing from one voltage to another. 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.

    Figure 5. Examples of power sequence errors.

  • 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.

    Figure 6. State-retention register and the sequence.

Towards complete low-power design verification

Formal verification verifies low-power designs against these functional failures. Formal verification provides a complete and fool-proof methodology to verify against failures. We have applied all the above concepts to the following design.

Figure 7. Example of a low-power design with high verification complexity.

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. In addition, 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: 100MHz and 200MHz. When Clk1 is 100MHz, the voltage is lowered from 1.2V to 1.0V.

Power domain D uses a clock Clk2 with a fixed frequency of 200MHz 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.

Table 1: State table for the example 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.

Figure 8: Domain ordering graph for the design. Domains A and C are unrelated and hence no checking is needed.

The power-up sequence for this design is when going from state 0 to state 1. It has to follow PDA>PDC>PDB. The power-down sequence is !PDA>!PDCà>PDB. The 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 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.

Figure 9. Temporal checks for the example design.


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 identify all the design issues.

By Saptarshi Biswas.

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, India.

Go to the Jasper Design Automation website to learn more.

Keywords: ASICs, ASIC design, EDA, EDA tools, electronic design automation, formal verification, power analysis, power optimization, low power design, low-power design, SOCcentral, Jasper Design Automation,
488/31280 5/7/2010 5417 5417
Add a comment or evaluation (anonymous postings will be deleted)

Designer's Mall

 Search for:
            Site       Current Category  
   Search Options

Subscribe to SOCcentral's
SOC Explorer
and receive news, article, whitepaper, and product updates bi-weekly.


Verification Contortions

Dr. Lauro Rizzatti
Verification Consultant
Rizzatti, LLC

Real Talk

P2415: The New Power Standard for Unified Hardware Abstraction

Graham Bell
VP Marketing
Real Intent

SOCcentral Job Search

SOC Design
ASIC Design
ASIC Verification
FPGA Design
CPLD Design
PCB Design
DSP Design
RTOS Development
Digital Design

Analog Design
Mixed-Signal Design
IC Packaging

Special Topics/Feature Articles
3D Integrated Circuits
Analog & Mixed-Signal Design
Design for Manufacturing
Design for Test
ESL Design
Floorplanning & Layout
Formal Verification/OVM/UVM/VMM
Logic & Physical Synthesis
Low-Power Design
On-Chip Interconnect
Selecting & Integrating IP
Signal Integrity
Timing Analysis & Closure
Transaction Level Modeling (TLM)
Design Center
Tutorials, Whitepapers & App Notes
Archived Webcasts


Sponsorship/Advertising Information

The Home Port  EDA/EDA Tools  FPGAs/PLDs/CPLDs  Intellectual Property  Electronic System Level Design  Special Topics/Feature Articles  Vendor & Organization Directory
News  Major RSS Feeds  Articles Online  Tutorials, White Papers, etc.  Webcasts  Online Resources  Software   Tech Books   Conferences & Seminars  About
Copyright 2003-2013  Tech Pro Communications   1209 Colts Circle    Lawrenceville, NJ 08648    Phone: 609-477-6308
553.488  1.016113