{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T05:05:50Z","timestamp":1750309550386,"version":"3.41.0"},"reference-count":36,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2025,1,10]],"date-time":"2025-01-10T00:00:00Z","timestamp":1736467200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Des. Autom. Electron. Syst."],"published-print":{"date-parts":[[2025,3,31]]},"abstract":"<jats:p>\n            Graphics Processing Units (GPUs) are becoming widespread, even in safety-critical applications. In that case, it is imperative to guarantee that the probability of producing critical failures due to hardware faults is lower than a given threshold. To detect possible permanent hardware faults as soon as they appear during the operational phase (e.g., due to aging), Software Test Libraries (STLs) have gained significant traction as a widely adopted test solution due to their effectiveness in terms of fault detection capabilities, test application time, and flexibility. However, a major drawback of this solution is the lack of automation in the STL generation phase. As a result, high manual labor is required for their generation. This becomes even more arduous in complex architectures that require in-depth knowledge to cover hard-to-test faults. In this article, we introduce a methodology based on Bounded Model Checking to support the generation and improvement of stuck-at-oriented STLs for hard-to-test units in GPUs, showing that we can enhance the test coverage achieved by pre-existing STLs while also identifying a set of functionally untestable faults. To experimentally validate the proposed method\u2019s effectiveness, we use the\n            <jats:monospace>FlexGripPlus<\/jats:monospace>\n            GPU model to target two hard-to-test units, one medium to low complexity sub-unit and one high complexity sub-unit, as study cases. For both units, we had pre-existing STLs written for the stuck-at model. Resorting to the proposed method, the STLs\u2019 test coverage was increased by 9.57% and 2.19%, respectively. In addition, the method also identified a significant number of functionally untestable faults.\n          <\/jats:p>","DOI":"10.1145\/3706635","type":"journal-article","created":{"date-parts":[[2024,12,4]],"date-time":"2024-12-04T10:59:56Z","timestamp":1733309996000},"page":"1-24","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Enhancing the Effectiveness of STLs for GPUs via Bounded Model Checking"],"prefix":"10.1145","volume":"30","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-7948-3361","authenticated-orcid":false,"given":"Nikolaos","family":"Deligiannis","sequence":"first","affiliation":[{"name":"Control and Computer Engineering (DAUIN), Politecnico di Torino, Torino, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0864-077X","authenticated-orcid":false,"given":"Tobias","family":"Faller","sequence":"additional","affiliation":[{"name":"University of Freiburg, Freiburg im Breisgau, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5957-5624","authenticated-orcid":false,"given":"Josie Esteban","family":"Rodriguez Condia","sequence":"additional","affiliation":[{"name":"Control and Computer Engineering (DAUIN), Politecnico di Torino, Torino, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1745-5293","authenticated-orcid":false,"given":"Riccardo","family":"Cantoro","sequence":"additional","affiliation":[{"name":"Control and Computer Engineering (DAUIN), Politecnico di Torino, Torino, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4031-3258","authenticated-orcid":false,"given":"Bernd","family":"Becker","sequence":"additional","affiliation":[{"name":"Albert-Ludwigs-Universitat Freiburg, Freiburg, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2899-7669","authenticated-orcid":false,"given":"Matteo","family":"Sonza Reorda","sequence":"additional","affiliation":[{"name":"Control and Computer Engineering (DAUIN), Politecnico di Torino, Torino, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2025,1,10]]},"reference":[{"key":"e_1_3_1_2_2","doi-asserted-by":"publisher","DOI":"10.1109\/AERO.2019.8741765"},{"key":"e_1_3_1_3_2","doi-asserted-by":"publisher","DOI":"10.23919\/DATE.2019.8715177"},{"key":"e_1_3_1_4_2","doi-asserted-by":"publisher","DOI":"10.1109\/MM.2018.2873870"},{"key":"e_1_3_1_5_2","doi-asserted-by":"publisher","DOI":"10.1109\/IRPS45951.2020.9129519"},{"key":"e_1_3_1_6_2","doi-asserted-by":"publisher","DOI":"10.23919\/DATE51398.2021.9474060"},{"key":"e_1_3_1_7_2","doi-asserted-by":"publisher","DOI":"10.7873\/DATE.2013.298"},{"key":"e_1_3_1_8_2","doi-asserted-by":"publisher","DOI":"10.3233\/978-1-58603-929-5-457"},{"key":"e_1_3_1_9_2","doi-asserted-by":"publisher","DOI":"10.1109\/VLSI-SoC.2018.8644846"},{"key":"e_1_3_1_10_2","doi-asserted-by":"publisher","DOI":"10.1109\/ACCESS.2020.2968139"},{"key":"e_1_3_1_11_2","doi-asserted-by":"publisher","DOI":"10.1109\/MM.2023.3256796"},{"key":"e_1_3_1_12_2","doi-asserted-by":"publisher","DOI":"10.1109\/IOLTS.2019.8854463"},{"key":"e_1_3_1_13_2","doi-asserted-by":"publisher","DOI":"10.1109\/VLSI-SOC46417.2020.9344088"},{"key":"e_1_3_1_14_2","unstructured":"Brett W. Coon John R. Nickolls John Erik Lindholm and D. Svetoslav Tzvetkov. 2009. Structured Programming Control Flow using a Disable Mask in a SIMD Architecture. US Patent 7 617 384."},{"key":"e_1_3_1_15_2","doi-asserted-by":"publisher","DOI":"10.1109\/ATS56056.2022.00027"},{"key":"e_1_3_1_16_2","doi-asserted-by":"publisher","DOI":"10.1109\/ETS.2013.6569353"},{"key":"e_1_3_1_17_2","doi-asserted-by":"publisher","DOI":"10.1109\/IOLTS.2018.8474174"},{"key":"e_1_3_1_18_2","doi-asserted-by":"publisher","DOI":"10.1109\/ETS56758.2023.10174156"},{"key":"e_1_3_1_19_2","doi-asserted-by":"publisher","DOI":"10.1109\/LATS53581.2021.9651819"},{"key":"e_1_3_1_20_2","doi-asserted-by":"publisher","DOI":"10.1109\/DDECS52668.2021.9417025"},{"key":"e_1_3_1_21_2","doi-asserted-by":"publisher","DOI":"10.23919\/DATE54114.2022.9774597"},{"key":"e_1_3_1_22_2","doi-asserted-by":"publisher","DOI":"10.1109\/ITC50671.2022.00065"},{"key":"e_1_3_1_23_2","doi-asserted-by":"publisher","DOI":"10.1109\/DSD.2019.00064"},{"key":"e_1_3_1_24_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-011-0122-4"},{"key":"e_1_3_1_25_2","doi-asserted-by":"publisher","DOI":"10.1109\/MM.2008.31"},{"key":"e_1_3_1_26_2","unstructured":"NVIDIA Corporation. 2023. Industrial-Scale AI. Retrieved 12-Dec-2024 from https:\/\/www.nvidia.com\/en-us\/industries\/industrial-sector\/"},{"key":"e_1_3_1_27_2","doi-asserted-by":"publisher","DOI":"10.1109\/IECON.2018.8591540"},{"key":"e_1_3_1_28_2","doi-asserted-by":"publisher","DOI":"10.1145\/3549526"},{"key":"e_1_3_1_29_2","doi-asserted-by":"publisher","DOI":"10.1109\/MDT.2010.5"},{"key":"e_1_3_1_30_2","doi-asserted-by":"publisher","DOI":"10.1109\/TVLSI.2016.2538800"},{"key":"e_1_3_1_31_2","doi-asserted-by":"publisher","DOI":"10.1109\/MDAT.2022.3188573"},{"key":"e_1_3_1_32_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.microrel.2020.113660"},{"key":"e_1_3_1_33_2","unstructured":"Silvaco. 2011. Silvaco 45nm Open Cell Library. Retrieved 12-Dec-2024 from https:\/\/si2.org\/open-cell-library"},{"key":"e_1_3_1_34_2","doi-asserted-by":"publisher","DOI":"10.1145\/2749469.2750375"},{"key":"e_1_3_1_35_2","unstructured":"Synopsys. 2023. Silicon Lifecycle Management. Retrieved 12-Dec-2024 from https:\/\/www.synopsys.com\/solutions\/silicon-lifecycle-management.html"},{"key":"e_1_3_1_36_2","doi-asserted-by":"publisher","DOI":"10.1109\/HPCA.2014.6835939"},{"key":"e_1_3_1_37_2","doi-asserted-by":"publisher","DOI":"10.1109\/TVLSI.2022.3186946"}],"container-title":["ACM Transactions on Design Automation of Electronic Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3706635","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3706635","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T01:18:46Z","timestamp":1750295926000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3706635"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,1,10]]},"references-count":36,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2025,3,31]]}},"alternative-id":["10.1145\/3706635"],"URL":"https:\/\/doi.org\/10.1145\/3706635","relation":{},"ISSN":["1084-4309","1557-7309"],"issn-type":[{"type":"print","value":"1084-4309"},{"type":"electronic","value":"1557-7309"}],"subject":[],"published":{"date-parts":[[2025,1,10]]},"assertion":[{"value":"2024-08-02","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-11-30","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-01-10","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}