1. Verifying power domains and modal operation: One of the most effective techniques in power management is power shut-off (PSO), which switches off power to parts of the chip when not in use. Formal verification can be used to specify the situations in which various domains should be switched off, to confirm that no activities are generated when switched off, and that the chip works correctly with every combination of PSO for various domains.
2. Verifying state and sequence interactions for power architectures: Similar to modal operation, allows formal verification to confirm that state retention of key state elements performs properly, and the system can recover after powering up and down the various domains.
3. Full frequency / phase jitter: Clock tree optimization and clock gating, with possible asynchronous clock domain crossing, are typical in lower power architecture, since clock trees are large source of dynamic power. Because of the tricky timing to trigger frequency jitter and phase jitter, simulation typically cannot be relied upon for detection of function errors due to jitter. Formal technology can efficiently verify end-to-end properties in the presence of frequency jitter and phase jitter.

High value is derived from formal verification in verifying power domains and modal operation, as more and more designs become power-sensitive. The number of power domains and the number of different power modes is increasing, and despite standards like UPF and CPF, forging a new power analysis and verification path using formal certainly solves many problems.