{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:53:12Z","timestamp":1750308792931,"version":"3.41.0"},"reference-count":59,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2010,2,1]],"date-time":"2010-02-01T00:00:00Z","timestamp":1264982400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Des. Autom. Electron. Syst."],"published-print":{"date-parts":[[2010,2]]},"abstract":"<jats:p>Overheating of computer chips leads to degradation of performance and reliability. Therefore, preventing chips from overheating in spite of increased performance requirements has emerged as a major challenge. Since the cost of cooling has been rising steadily, various architecture and application design techniques are used to prevent chip overheating. Temperature-aware task scheduling has emerged as an important application design methodology for addressing this problem in multiprocessor SoC systems.<\/jats:p>\n          <jats:p>\n            In this work we present the formulation and implementation of a method for analyzing the thermal (chip heating) behavior of a MPSoC task schedule, during the early stages of the design. We highlight the challenges in developing such a framework and propose solutions for tackling them. Due to nondeterminism in task execution times and decision branches, multiprocessor applications cannot be evaluated accurately by the current state-of-the-art\n            <jats:italic>thermal<\/jats:italic>\n            <jats:italic>simulation<\/jats:italic>\n            and\n            <jats:italic>steady-state<\/jats:italic>\n            analysis methods. Hence an analysis covering nondeterministic execution behaviors is required for thermal analysis of MPSoC task schedules. To address this issue we propose a model checking-based approach for solving the thermal analysis problem and formulate it as a hybrid automata reachability verification problem. We present an algorithm for constructing this hybrid automata given the task schedule, a set of power profiles of tasks, and the Compact Thermal Model (CTM) of the chip. Information about task power consumption is inferred from Markov chains which are learned from power profiles of tasks, obtained from simulation or emulation runs. A numerical analysis-based algorithm which uses CounterExample-Guided Abstraction Refinement (CEGAR) is developed for reachability analysis of this hybrid automata. We propose a directed simulation methodology which uses results of a time-bounded analysis of the hybrid automata modeling thermal behavior of the application, to simulate the expected worst-case execution runs of the same. The algorithms presented in this work have been implemented in a prototype tool called\n            <jats:italic>HeatCheck<\/jats:italic>\n            . We present experimental results and analysis of thermal behavior of a set of task schedules executing on a MPSoC system.\n          <\/jats:p>","DOI":"10.1145\/1698759.1698765","type":"journal-article","created":{"date-parts":[[2010,3,2]],"date-time":"2010-03-02T19:20:32Z","timestamp":1267557632000},"page":"1-52","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Thermal analysis of multiprocessor SoC applications by simulation and verification"],"prefix":"10.1145","volume":"15","author":[{"given":"Dipankar","family":"Das","sequence":"first","affiliation":[{"name":"Indian Institute of Technology Kharagpur, India"}]},{"given":"P. P.","family":"Chakrabarti","sequence":"additional","affiliation":[{"name":"Indian Institute of Technology Kharagpur, India"}]},{"given":"Rajeev","family":"Kumar","sequence":"additional","affiliation":[{"name":"Indian Institute of Technology Kharagpur, India"}]}],"member":"320","published-online":{"date-parts":[[2010,3,2]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/1132357.1132363"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.5555\/646880.759760"},{"volume-title":"Proceedings of the IEEE International Symposium on Computer-Aided Control Systems Design. 1582--1587","author":"Asarin E.","key":"e_1_2_2_3_1","unstructured":"Asarin , E. , Dang , T. , Frehse , G. , Girard , A. , Le Guernic , C. , and Maler , O . 2006. Recent progress in continuoushybrid reachability analysis . In Proceedings of the IEEE International Symposium on Computer-Aided Control Systems Design. 1582--1587 . Asarin, E., Dang, T., Frehse, G., Girard, A., Le Guernic, C., and Maler, O. 2006. Recent progress in continuoushybrid reachability analysis. In Proceedings of the IEEE International Symposium on Computer-Aided Control Systems Design. 1582--1587."},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.5555\/646880.710595"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1109\/2.982917"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/643120.643122"},{"key":"e_1_2_2_7_1","doi-asserted-by":"crossref","unstructured":"Bowman H. Faconti G. P. and Massink M. 1998. Specification and verification of media constraints using UPPAAL. In Design Specification and Verification of Interactive Systems P. Markopoulos and P. Johnson Eds. Springer 261--277.  Bowman H. Faconti G. P. and Massink M. 1998. Specification and verification of media constraints using UPPAAL. In Design Specification and Verification of Interactive Systems P. Markopoulos and P. Johnson Eds. Springer 261--277.","DOI":"10.1007\/978-3-7091-3693-5_17"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/339647.339657"},{"key":"e_1_2_2_9_1","first-page":"155","article-title":"Ptolemy: A framework for simulating and prototyping heterogenous systems","volume":"4","author":"Buck J.","year":"1994","unstructured":"Buck , J. , Ha , S. , Lee , E. A. , and Messerschmitt , D. G. 1994 . Ptolemy: A framework for simulating and prototyping heterogenous systems . Int. J. Comput. Simul. 4 , 2, 155 -- 182 . Buck, J., Ha, S., Lee, E. A., and Messerschmitt, D. G. 1994. Ptolemy: A framework for simulating and prototyping heterogenous systems. Int. J. Comput. Simul. 4, 2, 155--182.","journal-title":"Int. J. Comput. Simul."},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/1283780.1283826"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1011276507260"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/876638.876643"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/1278349.1278357"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/1529255.1529259"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/296333.296338"},{"volume-title":"Proceedings of the 20th International Symposium on Parallel and Distributed Processing (IPDPS'06)","author":"Drake M.","key":"e_1_2_2_16_1","unstructured":"Drake , M. and Hoffmann , H. R. R. A. S. 2006. Mpeg-2 decoding in a stream pro-gramming language . In Proceedings of the 20th International Symposium on Parallel and Distributed Processing (IPDPS'06) . Drake, M. and Hoffmann, H. R. R. A. S. 2006. Mpeg-2 decoding in a stream pro-gramming language. In Proceedings of the 20th International Symposium on Parallel and Distributed Processing (IPDPS'06)."},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/1176760.1176807"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/1189756.1189757"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31954-2_17"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31954-2_19"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.5555\/1128020.1128563"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/s100090050008"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/1151074.1151078"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1109\/TVLSI.2006.876103"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1109\/DATE.2005.310"},{"key":"e_1_2_2_26_1","unstructured":"Ignowski J. S. Bostak C. and Parks W. H. 2008. Power estimation for a semiconductor device. US Patent application US20080234953.  Ignowski J. S. Bostak C. and Parks W. H. 2008. Power estimation for a semiconductor device. US Patent application US20080234953."},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/1272998.1273005"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1109\/MICRO.2006.8"},{"volume-title":"Proceedings of the IEEE International Conference on Computer-Aided Design (ICCAD'08)","author":"Jayaseelan R.","key":"e_1_2_2_29_1","unstructured":"Jayaseelan , R. and Mitra , T . 2008. Temperature aware task sequencing and voltage scaling . In Proceedings of the IEEE International Conference on Computer-Aided Design (ICCAD'08) , S. R. Nassif and J. S. Roychowdhury, Eds. IEEE, 618--623. Jayaseelan, R. and Mitra, T. 2008. Temperature aware task sequencing and voltage scaling. In Proceedings of the IEEE International Conference on Computer-Aided Design (ICCAD'08), S. R. Nassif and J. S. Roychowdhury, Eds. IEEE, 618--623."},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/998300.997173"},{"volume-title":"Proceedings of the 9th International Symposium on Quality Electronic Design (ISQED'08)","author":"Jung H.","key":"e_1_2_2_31_1","unstructured":"Jung , H. and Pedram , M . 2008. Improving the efficiency of power management techniques by using bayesian classification . In Proceedings of the 9th International Symposium on Quality Electronic Design (ISQED'08) . IEEE Computer Society, 178--183. Jung, H. and Pedram, M. 2008. Improving the efficiency of power management techniques by using bayesian classification. In Proceedings of the 9th International Symposium on Quality Electronic Design (ISQED'08). IEEE Computer Society, 178--183."},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2005.858276"},{"volume-title":"Proceedings of the Conference on Design, Automation and Test in Europe (DATE'07)","author":"Liu Y.","key":"e_1_2_2_33_1","unstructured":"Liu , Y. , Dick , R. P. , Shang , L. , and Yang , H . 2007. Accurate temperature-dependent integrated circuit leakage power estimation is easy . In Proceedings of the Conference on Design, Automation and Test in Europe (DATE'07) . 1526--1531. Liu, Y., Dick, R. P., Shang, L., and Yang, H. 2007. Accurate temperature-dependent integrated circuit leakage power estimation is easy. In Proceedings of the Conference on Design, Automation and Test in Europe (DATE'07). 1526--1531."},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/1274858.1274869"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/378239.378553"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/1142980.1142983"},{"volume-title":"Machine Learning","author":"Mitchell T. M.","key":"e_1_2_2_37_1","unstructured":"Mitchell , T. M. 1997. Machine Learning . McGraw-Hill Higher Education . Mitchell, T. M. 1997. Machine Learning. McGraw-Hill Higher Education."},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1109\/MSPEC.2006.1572345"},{"key":"e_1_2_2_39_1","volume-title":"Eds","author":"Morari M.","year":"2005","unstructured":"Morari , M. and Thiele , L. , Eds . 2005 . Proceedings of the 8th International Workshop on Hybrid Systems : Computation and Control (HSCC'05). Lecture Notes in Computer Science, vol. 3414 . Springer . Morari, M. and Thiele, L., Eds. 2005. Proceedings of the 8th International Workshop on Hybrid Systems: Computation and Control (HSCC'05). Lecture Notes in Computer Science, vol. 3414. Springer."},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1109\/40.768496"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/232807.232809"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/1142980.1142984"},{"key":"e_1_2_2_43_1","volume-title":"C: The Art of Scientific Computing","author":"Press W. H.","year":"1992","unstructured":"Press , W. H. , Teukolsky , S. A. , Vetterling , W. T. , and Flannery , B. P . 1992 . Numerical Recipes in C: The Art of Scientific Computing . Cambridge University Press , UK. Press, W. H., Teukolsky, S. A., Vetterling, W. T., and Flannery, B. P. 1992. Numerical Recipes in C: The Art of Scientific Computing. Cambridge University Press, UK."},{"volume-title":"Proceedings of the IEEE\/ACM International Conference on Computer-Aided Design (ICCAD '08)","author":"Rao R.","key":"e_1_2_2_44_1","unstructured":"Rao , R. and Vrudhula , S . 2008. Efficient online computation of core speeds to maximize the throughput of thermally constrained multi-core processors . In Proceedings of the IEEE\/ACM International Conference on Computer-Aided Design (ICCAD '08) . IEEE Press, 537--542. Rao, R. and Vrudhula, S. 2008. Efficient online computation of core speeds to maximize the throughput of thermally constrained multi-core processors. In Proceedings of the IEEE\/ACM International Conference on Computer-Aided Design (ICCAD '08). IEEE Press, 537--542."},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/1283780.1283824"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00114008"},{"volume-title":"Compile time task and resource allocation of concurrent applications to multiprocessor systems. Tech. rep. UCB\/EECS-2009-19","author":"Satish N. R.","key":"e_1_2_2_47_1","unstructured":"Satish , N. R. 2009. Compile time task and resource allocation of concurrent applications to multiprocessor systems. Tech. rep. UCB\/EECS-2009-19 , University of California Berkeley . Satish, N. R. 2009. Compile time task and resource allocation of concurrent applications to multiprocessor systems. Tech. rep. UCB\/EECS-2009-19, University of California Berkeley."},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1109\/MICRO.2004.35"},{"key":"e_1_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.1109\/DSN.2007.8"},{"key":"e_1_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/980152.980157"},{"key":"e_1_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/871506.871529"},{"key":"e_1_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICVD.2005.155"},{"key":"e_1_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/1108956.1108957"},{"volume-title":"Proceedings of the 23rd Annual IEEE Symposium on Semiconductor Thermal Measurement and Management (SemiTherm'07)","author":"Wang X.","key":"e_1_2_2_54_1","unstructured":"Wang , X. , Shakouri , A. , Farsiu , S. , and Milanfar , P . 2007. Extraction of power dissipation profile in an ic chip from temperature map . In Proceedings of the 23rd Annual IEEE Symposium on Semiconductor Thermal Measurement and Management (SemiTherm'07) . 51--56. Wang, X., Shakouri, A., Farsiu, S., and Milanfar, P. 2007. Extraction of power dissipation profile in an ic chip from temperature map. In Proceedings of the 23rd Annual IEEE Symposium on Semiconductor Thermal Measurement and Management (SemiTherm'07). 51--56."},{"key":"e_1_2_2_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/1347375.1347389"},{"key":"e_1_2_2_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/1391469.1391658"},{"key":"e_1_2_2_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/1188275.1188277"},{"volume-title":"Proceedings of the IEEE\/ACM International Conference on Computer-Aided Design (ICCAD'05)","author":"Zhan Y.","key":"e_1_2_2_58_1","unstructured":"Zhan , Y. and Sapatnekar , S. S . 2005. A high efficiency full-chip thermal simulation algorithm . In Proceedings of the IEEE\/ACM International Conference on Computer-Aided Design (ICCAD'05) . IEEE Computer Society, 635--638. Zhan, Y. and Sapatnekar, S. S. 2005. A high efficiency full-chip thermal simulation algorithm. In Proceedings of the IEEE\/ACM International Conference on Computer-Aided Design (ICCAD'05). IEEE Computer Society, 635--638."},{"volume-title":"Proceedings of the IEEE\/ACM International Conference on Computer-Aided Design (ICCAD'07)","author":"Zhang S.","key":"e_1_2_2_59_1","unstructured":"Zhang , S. and Chatha , K. S . 2007. Approximation algorithm for the temperature-aware scheduling problem . In Proceedings of the IEEE\/ACM International Conference on Computer-Aided Design (ICCAD'07) . IEEE Press, 281--288. Zhang, S. and Chatha, K. S. 2007. Approximation algorithm for the temperature-aware scheduling problem. In Proceedings of the IEEE\/ACM International Conference on Computer-Aided Design (ICCAD'07). IEEE Press, 281--288."}],"container-title":["ACM Transactions on Design Automation of Electronic Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1698759.1698765","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1698759.1698765","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T20:22:58Z","timestamp":1750278178000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1698759.1698765"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,2]]},"references-count":59,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2010,2]]}},"alternative-id":["10.1145\/1698759.1698765"],"URL":"https:\/\/doi.org\/10.1145\/1698759.1698765","relation":{},"ISSN":["1084-4309","1557-7309"],"issn-type":[{"type":"print","value":"1084-4309"},{"type":"electronic","value":"1557-7309"}],"subject":[],"published":{"date-parts":[[2010,2]]},"assertion":[{"value":"2008-03-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2009-11-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2010-03-02","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}