Formal Verification of Power Intent

I can’t imagine that any SoC today is designed without taking intense interest in how much power the chip will consume, whether it is destined for a mobile phone or tethered in a cloud datacenter. One challenge with power is that adding features like voltage islands or power-down areas require changes to the netlist such as adding level-shifters or isolation cells.

A few years ago, two consortia developed the UPF and CPF power standards that make the power policy orthogonal with the functionality captured in the RTL/netlist. To add a voltage island does not require trawling through potentially large numbers of RTL files adding all the required level shifters explicity, and then, if we change our mind, going through and taking them all out again. Instead, the CPF/UPF file identifies which library elements are level shifters, where the voltage islands are, and so forth. Every EDA tool which reads the RTL/netlist needs to make the same changes to the netlist (level shifters affect timing, for example) whether a simulator, static timing, place and route and so on.

So the typical development methodology today is to use IP blocks and assemble the RTL for the complete SoC and get the functionality correct. As the design proceeds, the power policy can develop and various power optimizations such as clock shutoff, power shutoff or voltage islands can be added.

Of course, this leads to a new verification problem. It is no longer good enough to use formal techniques on the netlist alone, there are potentially errors in the way that the way the power policy has been implemented. It is typically not possible to decide the entire power policy ahead of time, it has to develop along with the floorplan since you can’t power down a block, for example, without it being an identifiable area on the floorplan with its own power grid. Plus, of course, there needs to be circuitry added to added to control shutting down and re-starting the block.

Normal design functionality should not be affected by the addition of the domains and the control registers. Before and after checking is necessary to ensure this. At the end of a power switching sequence the signals should all be generated correctly (with no additional unknowns). Switching off a power domain should not break connectivity between IP blocks.

The RTL before addition of power policy is a golden reference model. Power-aware verification requires a mix of architecture level verification, IP white box functional verification and analysis, exhaustive functional verification, sequential equivalence checking, control/status register verification, X-propagation analysis and connectivity checking.

Traditional power-aware verification relies on a mix of simulation and rule-checking. Typically problems are corner cases and, of course, these are just the areas where formal techniques tend to excel over simulation based verification.

The JasperGold Low-Power Verification (LPV) App automatically creates power-aware transformations and automatically generates a power-aware model that identifies power domains, the power supply network and switches, isolation rules and data retention rules. It does so by parsing and extracting relevant data from the UPF/CPF specification, RTL code and user-defined assertions. It then generates assertions that other Apps can use to verify that the power management circuitry does indeed conform to the UPF/CPF specification and does not corrupt the original RTL behavior.

The JasperGold LPV App is described in more detail in a new Jasper white paper Formal Verification of Power-Aware Designs Using the JasperGold Low-Power Verification App available here.

Related Blog