Formal Verification of Hardware / Software Power Management Strategies

Complex low power integrated circuits use global power management strategies to orchestrate the switching between power states of multiple power domains. One of the primary challenges in verifying such power management architectures stems from the mixed implementation of such strategies, where the local power controllers are in hardware and the global power management is implemented in software/firmware. In this paper we present an approach for using formal methods for verifying such hardware / software power management implementations. To the best of our knowledge, this is the first approach for formal verification of such implementations.