Formal Methods to Verify the Power Manager for an Embedded Multiprocessor Cluster

Kesava R. Talupuru, MIPS Technologies Inc.
Sunnyvale, CA, USA

Abstract

With shrinking process geometries, static and dynamic power are increasing rapidly, forcing designers to use a variety of implementation techniques to control power. MIPS Technologies’ multicore processors such as the MIPS32® 1004K Coherent Processing System (CPS) designed for low power applications use multiple power modes and employ a Power Manager to ensure correct transitions between these modes. This paper focuses on the verification of the Power Manager in the context of the MIPS32® 1004K™ Coherent Processing System (CPS), in which various software and hardware events can control switching of power states. Without exhaustive verification of the Power Manager, power management functionality of the design cannot be guaranteed. This paper discusses how we successfully used formal methods to verify the Power Manager.

1. Introduction

Power consumption has become a critical issue in System-on-Chip (SoC) design. To reduce power numbers, designers use a variety of techniques: clock gating, multi-voltage, dynamic voltage scaling, and power gating [1] [3].  MIPS Technologies’ power-aware designs employ a Power Manager to identify the state of the system and ensure proper transitions to appropriate power states. The Power Manager is also needed to ensure that clocks, resets, isolation signals, etc. are all generated in an architecturally defined sequence. Typically, the Power Manager is a combination of hardware and software-based control logic.

The MIPS32® 1004K™ Coherent Processing System (CPS) implements low power techniques. As shown in Figure 1, the 1004K CPS consists of up to four microprocessor cores, and a Coherency Manager (CM) to route coherence traffic between the cores. The physical implementation of the 1004K CPS supports five distinct power domains - four CPUs and the CM.

As shown in Figure 2, the 1004K CPS Power Manager has three components that need to be verified. The first component is the Open Core Protocol (OCP) [5] interface which is used to communicate with other blocks within the SoC. The second component is the access control block which has global, local, and peer memory mapped registers that can be programmed by software. The third component is the finite state machine (and control logic) which controls the transition of power states.

Since the Power Manager is very critical to the overall functionality of the SoC, exhaustive verification of this block is a must. As power states can be altered by an array of possibilities, identifying and verifying all corner case scenarios will be challenging with a simulation based approach. Moreover, the simulation speeds are very slow at the SoC level. Formal verification fits best in this case, as the power manager block is full of control logic, and the formal proofs are very exhaustive.

The OCP interface was formally verified by reusing the OCP assertion kit described in [2], and will not be discussed in detail in this paper. All the properties in this paper are written using System Verilog Assertions (SVA) [4]. The rest of the paper will describe the following: Section 2 addresses verification of the access control block; Section 3 discusses verification of the Power Manager finite state machine; Section 4 delineates different bugs that were found; Section 5 discusses the integration of formal into system level simulation verification; and Section 6 discusses overall results using the Synopsys Magellan formal tool.

Figure 1. MIPS32® 1004K™ Coherent Processing System

2. Access Control Block Verification

This block consists of various 32-bit memory mapped registers which can be accessed by software.  Software can read these registers to query the status of the Power Manager, or write these registers with various power commands to control power transitions. If there are no writes from software, then the registers should hold the reset values or previously written data. This block communicates with the SoC through the OCP interface. Formal properties are deduced for this block based on the fact that the registers can be read and written, and should hold the current data if no writes occurred. The following properties written in SVA cover the verification of all the above mentioned functionality.

2.1 Reset Values

Some registers have read-only bits which reflect some configuration choices. These bits get set immediately after reset is de-asserted. The property below formally proves that these bits are set correctly the cycle after reset. The assertion checks that in the cycle where reset goes from one to zero, the register holds the data matching to the specifications. As the assertion is disabled during reset, a one cycle delayed version of reset needs to be used.

2.2 Write operation

 As shown in Figure 3, it takes two clock cycles to write the data into the appropriate register. The property is written from the OCP interface to the destination register. The assertion below makes sure that there is a write request, that the address is within the allowed address space, and that there are write permissions to the power domains. After two cycles, the register contents should match the data that appeared on OCP bus two cycles earlier.

Figure 2. Power Manager Components

2.3 Read operation

This is similar to the write operation. It takes one clock cycle for the data to appear on the OCP interface. The assertion below makes sure that there is a read request, and that the address is within the allowed address space. If few bits of the register are always zero, then those bits are directly compared to zero at OCP interface.

 

 

Figure 3. Write Logic Flow

 2.4 Hold Data

If there is no write request, then the data in the registers should not change. This property is proven by saying that if the data was changed this cycle, then there should have been a write request two cycles before that matches to this register. This property needs to be checked at least two cycles after reset as we check data two cycles past.

3. Power Manager FSM

The Power Manager Finite State Machine (FSM) controls the power modes of CPUs based on the software and hardware events that it receives. Typical software commands are: Power-Down, Power Up, Clock Off, and Reset. The hardware events are triggered by toggling different external pins: Power Up and Interrupt pins. As shown in Figure 4, the power manager can make each individual CPU assume one of four modes of operation - Coherent, Non-Coherent, Clock-Off and PowerDown.

Coherent Mode: In this mode, the CPU operates as a member of an L1 cache coherent domain and exchanges coherence messages with processor peers to maintain cache coherence. To avoid corruption of coherent data in the caches, power and clock must not be disabled while the CPU is in this mode.

Non-Coherent Mode: In this mode, the CPU operates outside the coherent domain and does not exchange coherent messages with peer cores.

Clock-Off Mode: Any CPU operating outside of the coherent domain can assume clock-off mode. Clock distribution towards this CPU is cut at the clock generator level.

Power-Down Mode: In this mode, the CPU is electrically isolated from its surroundings, and the supply voltage is removed. Other cores in Power-Up mode will continue to operate.

FSM state transitions between operating levels are depicted in Figure 4. Each transition points toward a possible command target state. However, the Power Manager FSM will step through a series of transitional states to maintain power integrity. Each programmable transition is outlined below:

Coherent to Non-Coherent Mode transition:

The core leaves the coherent domain and starts operating independently. Software must flush dirty data from data cache, and invalidate all clean data cache lines.

Non-Coherent to Coherent Mode transition: An independently operating core becomes a member of the coherent cluster, and the data cache lines are invalidated as the core will be participating in coherency.

Non-Coherent to Power-Down Mode transition: A core which is not member of the coherent domain is powered down, and the Power Manager will initiate the clock and power shutdown sequence.

Non-Coherent to Clock-Off Mode transition: The clock tree root is disabled for this core, and dynamic power consumption is removed.

Clock-Off to Power-Down Mode transition: The power supply is removed for the disconnected core. Dynamic and leakage power are removed. The Power Manager initiates the power shutdown sequence.

Clock-Off to Non-Coherent Mode transition:

When a power-up or reset command is given to the Power Manager, the FSM initiates a sequence to make the core operational.

Power-Down to Non-Coherent Mode transition: When the Power Manager receives a power-up command, the FSM initiates a power-up sequence and the core becomes operational.

In each mode of operation, we need to verify that conditions related to clock, reset, isolation, etc. are met. Additionally, there are a wide variety of protocols that must be checked. Some of the important Power Manager properties that must be checked are listed below.

3.1 Power Manager Output Signals Check

In all of the different power modes, the Power Manager should make sure that isolation, clock enables, resets, etc are all driven with appropriate values as shown in Table 1. This can be verified by writing a common property as shown below and then instantiating that property for each power mode.

Table 1: FSM State Outputs

The property below takes two inputs for each power manager output. One input value is the current RTL value, and the other input is the expected value passed by the user based on specification.

Figure 4 Cluster CPU States

The property is instantiated for each Power Manager state, and expected values are passed in the instance. The property below is the instance for power-down.

3.2 Power Manager FSM Valid Transitions

The Power Manager FSM should transition from the current state only to valid next states. For example, as shown in Figure 4, if the current state is Clock-Off, then the valid next states are Non-Coherent, Power-Down and Clock-Off. The property below checks the valid transitions for all of the power modes.

3.3 Power Manager FSM Valid Transition Triggers

Power Manager FSM will change from one power domain to another only if the valid transition trigger command is received. For example, as shown in Figure 4, the FSM will transition from Power-Down mode to Non-Coherent mode only if the reset trigger is issued.

3.3 Power Manager FSM Valid Transition Triggers

Power Manager FSM will change from one power domain to another only if the valid transition trigger command is received. For example, as shown in Figure 4, the FSM will transition from Power-Down mode to Non-Coherent mode only if the reset trigger is issued.

3.4 FSM States Reachability

This property can be checked either by writing a cover point and enabling coverage in a formal tool, or by writing an assertion which specifies that the state can never be reached. If the assertion passes, then that state is never reachable.

3.5 Checking Power Manager States

Power modes can be changed as a result of the occurrence of different events. If multiple events occur at the same time, then the power mode is switched based on priority. The property below checks that if reset, power down, and interrupt are received at the same time, and if the Power Manager is currently in a coherent state, then all the events will be ignored and the power domain will not change.

3.6 Coherent Core Shutdown

If any of the cores is participating in coherency, then that core will remain in coherent power domain to respond to peer CPU requests, and will ignore any triggers trying to change the power state. The property below checks that if current state is coherent and if the power down command is issued, the manager will still maintain the coherent mode.

3.7 Software Reset Deadlock Avoidance

When software issues a reset command for a domain, the command will be captured in the command register. Once the Power Manager resets the domain, then the command register contents should be squashed by the manager. If the reset command is not squashed, then the Power Manager will keep resetting the domain assuming that a new reset command has been issued.

3.8 JTAG Check

The JTAG interfaces of each core are connected in a daisy chain. So, if JTAG is connected to the system, then none of the cores can be in Power-Down mode. They should be in Clock-Off mode so that the JTAG chain is not broken.

In addition to the above properties, there are some other properties that must be checked. For example, the CM cannot wake up if all the cores are in Power-Down mode; and if the coherent IO port is enabled, then the CM cannot power down.
 
4. Bugs Uncovered

Following are the various kinds of bugs uncovered by proving the above mentioned properties using formal tools.

a) Finite state machines progress based on the target state. Target state is calculated based on the power commands received. If no new command is received, then the target state should hold. But, because of a functional bug, the design was changing the target state to current intermediate state. This can create deadlocks in the FSM.

b) When the coherent IO port is enabled, the CM should remain powered up even if all of the cores are in Power-Down mode. But the bug was that the CM was shutting down even when the coherent IO port was enabled.

c) Reset priority bugs – The Power Manager can do a cold or warm reset of a power domain. For a warm reset, certain status register contents will be preserved. Based on the current state, the FSM should decide whether to do a warm or cold reset. The design had a bug in selecting the reset priority.

d) If Coherency is disabled for a particular core, then it should go to non-coherent mode. The bug was that the design stayed in coherent mode even when coherency is turned off.

e) The cores cannot shut down if there are pending transactions. The design bug was that the cores were shutting down with out completing the pending transactions when it receives power down command.

f) If the reset command is issued, the FSM should stop progressing once it reaches the reset state. But, in this case the FSM is in the reset loop.

5. Integrating Block-Level Formal Verification into System-Level Verification

Block-level formal verification fits well into overall system-level power verification. System-level simulation-based verification uncovered three bugs in the Power Manager. The bugs are mainly related to keeping the JTAG chain alive. These bugs were missed in formal verification, as the specifications for this JTAG chain were not complete. With system-level power-aware simulations, we found bugs outside of the Power Manager. It took six weeks of effort for the complete formal verification of the Power Manager, and about 20 weeks of effort for the system-level verification. Formal verification environment set up took a week, but for simulation, a major effort was put into preparing the test bench environment.

6. Results

The Power Manager was formally proved by using the Synopsys Magellan [6] [7] tool. It took less than a week to get the formal setup working so that the properties could be proven. The formal tool found many bugs in the early design phases when the simulation environment was not ready. The power manager was almost bug-free by the time the simulation environment was up and running. The simulation environment did find some bugs at the system-level as the formal tool could not handle the system level proofs.

Table 2: Results with Magellan Tool

The results for different numbers of power domains are listed in Table 2. For a single power domain, the tool was able to prove all the properties in 42 minutes. For two power domains, the tool was able to prove all but two assertions in two hours. For all the five power domains, the tool was able to prove 521 assertions completely, whereas the remaining 141 assertions were proved partially for around 60 cycles.

7. Conclusions

Since the Power Manager is such a critical component of the low-power SoC, exhaustive proof of correctness is desirable for this unit. Formal verification helped to exhaustively prove the correctness of the Power Manager in our environment. With a combination of formal and power-aware simulation-based verification, low power designs can be made bug free.

8. REFERENCES

[1]  Freddy Bembaron, Rudra Mukherjee, Sachin Kakkar, and Amit Srivastava .  “Low Power Verification Methodology using UPF”. DVCon 2009

[2] Ali Habibi, Jithendra Madala, Mandar Munishwar, and Haihui Chen.  “Verifying MIPS designs using Magellan”. SNUG 2008

[3]  Srikanth Jadcherla, Janick Bergeron, Yoshio Inoue, and David Flynn. “Verification Methodology Manual for Low Power”.

[4] IEEE, IEEE Standard for Property System Verilog, IEEE Std 1800-2005 (2005).

[5] OCP-IP Association, Open Core Protocol Specification, Release 2.2, 2006

[6] Synopsys, Discovery Visual Environment User Guide, Version Y-2006.06-SP1, April 2007.

[7] Synopsys, Magellan User Guide, Version MG_2009.03-5, March 2009