Probabilistic Formal Verification Methodology for Decentralized Thermal Management in SOCs

Shafaq Iqtedar, Osman Hasan, Muhammad Shafique and Jörg Henkel

Abstract

The prevalence of Dynamic Thermal Management (DTM) schemes coupled with demands for high reliability motivate the rigorous verification and testing of these schemes before deployment. Conventionally, these schemes are analyzed using either simulations or by running on real systems. But these traditional analysis techniques cannot exhaustively validate the distributed DTM schemes and thus compromise on the accuracy of the analysis results. Moreover, the randomness due to task assignments, task completion times and re-mappings, is often ignored in the analysis of distributed DTM schemes. We propose to overcome both of these limitations by using probabilistic model checking, which is a formal method for modeling and verifying concurrent systems with randomized behaviors. The paper presents a case study on the formal verification of a state-of-the-art distributed DTM scheme using the PRISM model checker.

Methodology

nad

Proposed Methodology for probabilistic formal verification of DTM

Experimental Results

nad

Effect of tasks on the size of model at different values of as and ab

nad

Probability that a thermal hotspot will not be formed

nad

Comparison of verification time with traditional model checking

nad

Two agents continuously trading one free unit back and forth

Publications

  1. S. Iqtedar, O. Hasan, M. Shafique, J. Henkel, “Probabilistic Formal Verification Methodology for Decentralized Thermal Management in On-Chip Systems”, IEEE International Conference on Enabling Technologies: Infrastructures for Collaborative Enterprises (WETICE-2015), IEEE Computer Society, Larnaca, Cyprus. pp. 210-215.

  2. S. Iqtedar, O. Hasan, M. Shafique, J. Henkel, “Formal Probabilistic Analysis of Distributed Dynamic Thermal Management”, Design, Automation and Test in Europe (DATE-2015), March 9-13, Grenoble, France. pp. 1221-1224.