The JG-LPV App reads the RTL description and creates an internal power-aware formal model in accordance with the power partitioning specifications. The new App verifies power optimization structures, power management circuitry, power sequencing, and works with other JasperGold Apps to verify that the power optimizations do not corrupt the original design functionality. The JG-LPV App supports the standard UPF and CPF power intent specification formats. The App’s automated approach, together with the exhaustive nature of formal verification, can reduce verification time, cost, and risk compared to traditional power-aware verification approaches.
When adding low power features to a design, the basic functionality should not be affected. But making this happen is complex since power mode transitions often require complicated sequencing (for example, to minimize inrush current when powering a block back up) or controlling the changes in voltage and frequency over a significant number of clock cycles during DVFS (dynamic voltage and frequency scaling). Also there are requirements for introducing level shifters, retention registers and isolation cells that if done incorrectly can result in non-functional designs. All this needs to be checked.
Simulation is always one option, of course. But by its very nature, it is obscure corner cases in power management that are likely to be troublesome. Obscure corner cases are just the areas where formal techniques, proving that the design is correct, are most likely to escape detection and cause failure.
The LPV App works with other JasperGold Apps to perform a complete analysis of the design. Power is a chip-level attribute that inevitably interacts with many other areas of the design.