Formal methods for coverage analysis of architectural power states in power-managed designs

The architectural power intent of a design defines the intended global power states of a power-managed integrated circuit. Verification of the implementation of power management logic involves the task of checking whether only the intended power states are reached. Typically, the number of global power states reachable by the global power management strategy is significantly lesser than the possible number of global power states. In this paper, we present a formal method for determining the set of reachable global power states in a power-managed design. Our approach demonstrates how this task can be further constrained as required by the verification engineer. We highlight the efficacy of the proposed methods over several test-cases.