UPF-based formal verification of low power techniques in modern processors

Ensuring from the correctness of system on a chip (SoC) designs after the insertion of high level power management strategies that are disconnected from low level controlling signals, is a serious challenge to be addressed. This paper proposes a methodology for formally verifying dynamic power management strategies on implementations in modern processors. The proposed methodology is based on correspondence checking between a golden model without power features as a specification and a pipelined implementation with various power management strategies. Our main contributions in this paper are: 1) extracting Power Management Unit (PMU) from Unified Power Format (UPF) and Global Power Management (GPM), 2) automatically integrating PMU into the implementation and 3) checking the correspondence between two models with efficient symbolic simulation. The experimental results show that our method enables the designers to verify the designs with different power management strategies up to several thousands of lines of Register Transfer Level (RTL) code in minutes. In comparison with existing methods such as [7], our method reduces the number of state variables, the number of clauses, the number of symbolic simulation steps, and the CPU time by 11.04×, 17.57×, 2.08× and 13.71×, respectively.