Verifying dynamic power management schemes using statistical model checking

Jayanand Asok Kumar, Shobha Vasudevan

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

Dynamic power management (DPM) schemes, such as power gating, are important runtime strategies for saving power in multicore architectures. Safety and efficiency are probabilistic properties which need to be verified in order to evaluate a DPM scheme. In this work, we employ statistical model checking to verify probabilistic properties on Register Transfer Level (RTL) descriptions of multicores. Statistical model checking performs a system-level verification of the DPM scheme by simulating several sample paths of the entire RTL design until the verification results lie within tolerable bounds of error. We illustrate our approach on the RTL of OpenSPARC T2, a publicly available industry-strength multicore processor. We verify the safety and efficiency properties of several power gating schemes by considering the power manageable blocks in the floating-point graphics unit

Original languageEnglish (US)
Title of host publicationASP-DAC 2012 - 17th Asia and South Pacific Design Automation Conference
Pages579-584
Number of pages6
DOIs
StatePublished - Apr 26 2012
Event17th Asia and South Pacific Design Automation Conference, ASP-DAC 2012 - Sydney, NSW, Australia
Duration: Jan 30 2012Feb 2 2012

Publication series

NameProceedings of the Asia and South Pacific Design Automation Conference, ASP-DAC

Other

Other17th Asia and South Pacific Design Automation Conference, ASP-DAC 2012
CountryAustralia
CitySydney, NSW
Period1/30/122/2/12

Fingerprint

Model checking
Statistical Models
Power management
Industry

ASJC Scopus subject areas

  • Computer Science Applications
  • Computer Graphics and Computer-Aided Design
  • Electrical and Electronic Engineering

Cite this

Kumar, J. A., & Vasudevan, S. (2012). Verifying dynamic power management schemes using statistical model checking. In ASP-DAC 2012 - 17th Asia and South Pacific Design Automation Conference (pp. 579-584). [6165023] (Proceedings of the Asia and South Pacific Design Automation Conference, ASP-DAC). https://doi.org/10.1109/ASPDAC.2012.6165023

Verifying dynamic power management schemes using statistical model checking. / Kumar, Jayanand Asok; Vasudevan, Shobha.

ASP-DAC 2012 - 17th Asia and South Pacific Design Automation Conference. 2012. p. 579-584 6165023 (Proceedings of the Asia and South Pacific Design Automation Conference, ASP-DAC).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Kumar, JA & Vasudevan, S 2012, Verifying dynamic power management schemes using statistical model checking. in ASP-DAC 2012 - 17th Asia and South Pacific Design Automation Conference., 6165023, Proceedings of the Asia and South Pacific Design Automation Conference, ASP-DAC, pp. 579-584, 17th Asia and South Pacific Design Automation Conference, ASP-DAC 2012, Sydney, NSW, Australia, 1/30/12. https://doi.org/10.1109/ASPDAC.2012.6165023
Kumar JA, Vasudevan S. Verifying dynamic power management schemes using statistical model checking. In ASP-DAC 2012 - 17th Asia and South Pacific Design Automation Conference. 2012. p. 579-584. 6165023. (Proceedings of the Asia and South Pacific Design Automation Conference, ASP-DAC). https://doi.org/10.1109/ASPDAC.2012.6165023
Kumar, Jayanand Asok ; Vasudevan, Shobha. / Verifying dynamic power management schemes using statistical model checking. ASP-DAC 2012 - 17th Asia and South Pacific Design Automation Conference. 2012. pp. 579-584 (Proceedings of the Asia and South Pacific Design Automation Conference, ASP-DAC).
@inproceedings{545ec66694e546b7b3918750316746c3,
title = "Verifying dynamic power management schemes using statistical model checking",
abstract = "Dynamic power management (DPM) schemes, such as power gating, are important runtime strategies for saving power in multicore architectures. Safety and efficiency are probabilistic properties which need to be verified in order to evaluate a DPM scheme. In this work, we employ statistical model checking to verify probabilistic properties on Register Transfer Level (RTL) descriptions of multicores. Statistical model checking performs a system-level verification of the DPM scheme by simulating several sample paths of the entire RTL design until the verification results lie within tolerable bounds of error. We illustrate our approach on the RTL of OpenSPARC T2, a publicly available industry-strength multicore processor. We verify the safety and efficiency properties of several power gating schemes by considering the power manageable blocks in the floating-point graphics unit",
author = "Kumar, {Jayanand Asok} and Shobha Vasudevan",
year = "2012",
month = "4",
day = "26",
doi = "10.1109/ASPDAC.2012.6165023",
language = "English (US)",
isbn = "9781467307727",
series = "Proceedings of the Asia and South Pacific Design Automation Conference, ASP-DAC",
pages = "579--584",
booktitle = "ASP-DAC 2012 - 17th Asia and South Pacific Design Automation Conference",

}

TY - GEN

T1 - Verifying dynamic power management schemes using statistical model checking

AU - Kumar, Jayanand Asok

AU - Vasudevan, Shobha

PY - 2012/4/26

Y1 - 2012/4/26

N2 - Dynamic power management (DPM) schemes, such as power gating, are important runtime strategies for saving power in multicore architectures. Safety and efficiency are probabilistic properties which need to be verified in order to evaluate a DPM scheme. In this work, we employ statistical model checking to verify probabilistic properties on Register Transfer Level (RTL) descriptions of multicores. Statistical model checking performs a system-level verification of the DPM scheme by simulating several sample paths of the entire RTL design until the verification results lie within tolerable bounds of error. We illustrate our approach on the RTL of OpenSPARC T2, a publicly available industry-strength multicore processor. We verify the safety and efficiency properties of several power gating schemes by considering the power manageable blocks in the floating-point graphics unit

AB - Dynamic power management (DPM) schemes, such as power gating, are important runtime strategies for saving power in multicore architectures. Safety and efficiency are probabilistic properties which need to be verified in order to evaluate a DPM scheme. In this work, we employ statistical model checking to verify probabilistic properties on Register Transfer Level (RTL) descriptions of multicores. Statistical model checking performs a system-level verification of the DPM scheme by simulating several sample paths of the entire RTL design until the verification results lie within tolerable bounds of error. We illustrate our approach on the RTL of OpenSPARC T2, a publicly available industry-strength multicore processor. We verify the safety and efficiency properties of several power gating schemes by considering the power manageable blocks in the floating-point graphics unit

UR - http://www.scopus.com/inward/record.url?scp=84859945148&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84859945148&partnerID=8YFLogxK

U2 - 10.1109/ASPDAC.2012.6165023

DO - 10.1109/ASPDAC.2012.6165023

M3 - Conference contribution

SN - 9781467307727

T3 - Proceedings of the Asia and South Pacific Design Automation Conference, ASP-DAC

SP - 579

EP - 584

BT - ASP-DAC 2012 - 17th Asia and South Pacific Design Automation Conference

ER -