Low-power chip designs are essential for today's portable devices as well as products that must conform to "green" initiatives. The most common techniques for controlling power, including power shut-off, clock gating, and multiple voltage domains, complicate the chip verification process. This paper discusses the intersection of these low-power design techniques and the use of formal analysis for verification. Topics covered include proper handling of assertions crossing power domain boundaries, use of formal analysis to verify power control modules (PCMs), and the role of Common Power Format (CPF) specification for formal analysis. This paper leverages the experience of several Cadence customers in using Incisive Formal Verifier (IFV) for PCM verification as well as assertion technology developed within Cadence.