A previous post showed a very-high level view of low power design with UPF/CPF. Power gating, a must-do for mobile products, is still a very manual process, and verifying the correctness of its implementation is a very challenging task. In this follow-up post, I single out some aspects of the power-gating flow, and I hint at how they can be automated for the benefit of the designer.
I will focus on three items necessary for power gating: (1) the FSM that controls the sleep and wake-up sequences; (2) the retention flops used to restore the state of the device when it is awakened; and (3) the correctness of the power gating implementation. Items (1) and (2) are manually done via UPF/CPF directives and FSM hand-coding. Item (3) is carried out with customer-specific methods, even though the use of CPF together with Conformal produces a more solid verification flow.
Sleep/wake-up protocol synthesis
Items (1) and (2) must really be considered together to answer the following question: how to implement a sleep and wake-up sequences that use retention flip-flops to resume the device’s state? It is clear that answers to that question are different tradeoffs between the number of retention flops and the length of the sequences. The more retention flops, the shorter the sequences are, but the higher the price in terms of area and residual leakage power. In essence, one would like to be able to explore the possible tradeoffs and pick the best compromise, depending on the application. Also from the designer point of view, one should not have to manually decide which flip-flops must be shadowed, nor one should have to hand-code the FSMs for the sleep and wake-up sequences.
Instead, one should be able to synthesize the retention flip-flops and the sleep and wake-up FSMs directly from a power state table –what I call sleep/wake-up protocol synthesis. I would propose an extension of the power state table so that transitions can also be labeled with constraints: an upper bound on the sequence length (in terms of number of clock cycles or milliseconds), and an upper bound on the area taken by the retention flops (actual area or as a percentage of the element area). This way the designer can concentrate on the power management strategy and explore different tradeoffs, instead of having to figure out the implementation itself.
Sleep/wake-up protocol synthesis is no small task. I would look into information relevance and functional dependency analysis to derive a candidate set of retention flops. Compression and encoding methods can then be used to reduce this set. The final FSM synthesis would implement the decoder. Looking into techniques coming from DFT, simulation, and formal verification could prove very helpful.
Item (3) is verifying the correctness of the power gating implementation. There are two aspects here. One is purely physical, and consists of checking that level shifters, isolation cells, and power switches have been properly inserted. The insertion of these cells can be automated, and verifying that their insertion obey basic physical rules in not a problem (this is supported for both UPF and CPF).
The main issue is to verify the functional correctness of the sleep/wake-up sequences, namely that the device meets some operational expectation once re-activated (e.g., the pre-sleep state is fully restored). Intensive simulation will give some coverage, but cannot be exhaustive in general. Sequential formal verification or property checker can then be used for a proof of correctness. For instance the property would go something like “if the device goes to sleep and then is re-activated, its state is fully restored to its pre-sleep state in less than one second”. To be manageable, such a property must be broken down in smaller or more abstract expressions. The same synthesis system that takes care of items (1) and (2) should generate the properties that a 3rd party property checker can independently verify to guarantee the correctness of the sleep/wake-up protocol. This is no different than a RTL synthesis tool giving hints to an equivalence checker to simplify the proof.
Given the complexity of today’s sleep/wake-up protocol design and verification, it is somewhat surprising that no EDA tool is really tackling the problem today. Is it because of user unawareness, or because of the size of the challenge? Regardless of the reason, the first company to offer sleep/wake up protocol synthesis and verification will make a major impact in the low power design community.