Simulation is the state-of-the-art analysis technique for distributed thermal management schemes. Due to the numerous parameters involved and the distributed nature of these schemes, such non-exhaustive verification may fail to catch functional bugs in the algorithm or may report misleading performance characteristics. To overcome these limitations, we propose a methodology to perform formal verification of distributed dynamic thermal management for many-core systems. The proposed methodology is based on the SPIN model checker and the Lamport timestamps algorithm. Our methodology allows specification and verification of both functional and timing properties in a distributed many-core system. In order to illustrate the applicability and benefits of our methodology, we perform a case study on a state-of-the-art agent-based distributed thermal management scheme.
- M. Ismail, O. Hasan, T. Ebi, M. Shafique and J. Henkel, ” Formal Verification of Distributed Dynamic Thermal Management” International Conference on Computer-Aided Design (ICCAD-2013) ,IEEE/ACM, Austin, Texas.
- M. Ismail, “Formal Analysis of TAPE: A Thermal Management Algorithm for ICs “, Masters Thesis, National University of Sciences and Technology (NUST), Islamabad, Pakistan. 2013.