Probabilistic Formal Verification Methodology for Decentralized Thermal Management in On-Chip Systems

Faiq Khalid Lodhi , Syed Rafay Hasan , Osman Hasan and Falah Awwad

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

Test vector insertion to obtain timing signature in MSMA

Experimental Results

nad

Distribution of Parameters (a) xj of pMOS (b) xj of nMOS (c) vth0 of pMOS (d) vth0 of nMOS (e) toxp of pMOS (f) toxp of nMOS

nad

Variation of the delay for Best Case ( when Test Vector is 0000 )

nad

Variation of the delay for Worst Case ( when Test Vector is 1011)

nad

Publications

  1. F. K. Lodhi, O. Hasan, S. R. Hasan and F. Awwad,”Hardware Trojan detection in soft error tolerant macro synchronous micro asynchronous (MSMA) pipeline, ” in IEEE International Midwest Symposium on Circuits and Systems (MWSCAS 2014), Aug. 2014, pp. 659 – 662.