{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:16:47Z","timestamp":1750220207394,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":26,"publisher":"ACM","license":[{"start":{"date-parts":[[2022,10,30]],"date-time":"2022-10-30T00:00:00Z","timestamp":1667088000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"This work was supported by the Applications Driving Architectures (ADA) Research Center, a JUMP Center co-sponsored by SRC and DARPA. This research is also funded in part by NSF award number 1628926, XPS: FULL: Hardware Software Abstractions: Addressing Specification and Verification Gaps in Accelerator-Oriented Parallelism, and the DARPA POSH Program Project: Upscale: Scaling up formal tools for POSH Open Source Hardware."}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2022,10,30]]},"DOI":"10.1145\/3508352.3549391","type":"proceedings-article","created":{"date-parts":[[2022,12,22]],"date-time":"2022-12-22T12:10:54Z","timestamp":1671711054000},"page":"1-9","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Usage-Based RTL Subsetting for Hardware Accelerators"],"prefix":"10.1145","author":[{"given":"Qinhan","family":"Tan","sequence":"first","affiliation":[{"name":"Princeton University"}]},{"given":"Aarti","family":"Gupta","sequence":"additional","affiliation":[{"name":"Princeton University"}]},{"given":"Sharad","family":"Malik","sequence":"additional","affiliation":[{"name":"Princeton University"}]}],"member":"320","published-online":{"date-parts":[[2022,12,22]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"Syntax-Guided Synthesis. FMCAD 2013 Formal Methods in Computer-Aided Design","author":"Alur Rajeev","year":"2013","unstructured":"Rajeev Alur, Rastislav Bodik, Garvit Juniwal, Milo MK Martin, Mukund Raghothaman, Sanjit A Seshia, Rishabh Singh, Armando Solar-Lezama, Emina Torlak, and Abhishek Udupa. 2013. Syntax-Guided Synthesis. FMCAD 2013 Formal Methods in Computer-Aided Design (2013), 1."},{"key":"e_1_3_2_1_2_1","unstructured":"Apple. 2020. Apple M1 Chip. https:\/\/www.apple.com\/newsroom\/2020\/11\/apple-unleashes-m1"},{"key":"e_1_3_2_1_3_1","unstructured":"asinghani. 2020. Crypto Accelerator Chip. https:\/\/github.com\/asinghani\/crypto-accelerator-chip"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129511000193"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/774572.774687"},{"key":"e_1_3_2_1_6_1","volume-title":"Property-driven Automatic Generation of Reduced-ISA Hardware. In 2021 58th ACM\/IEEE Design Automation Conference (DAC). IEEE, 349--354","author":"Bleier Nathan","year":"2021","unstructured":"Nathan Bleier, John Sartori, and Rakesh Kumar. 2021. Property-driven Automatic Generation of Reduced-ISA Hardware. In 2021 58th ACM\/IEEE Design Automation Conference (DAC). IEEE, 349--354."},{"key":"e_1_3_2_1_7_1","unstructured":"Cadence. 2022. JasperGold Formal Verification Platform. https:\/\/www.cadence.com\/en_US\/home\/tools\/system-design-and-verification\/formal-and-static-verification\/jasper-gold-verification-platform.html"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54792-8_15"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-2009-0393"},{"key":"e_1_3_2_1_10_1","volume-title":"IODINE: Verifying Constant-Time Execution of Hardware. In 28th USENIX Security Symposium (USENIX Security 19)","author":"Gleissenthall Klaus","year":"2019","unstructured":"Klaus v Gleissenthall, Rami G\u00f6khan K\u0131c\u0131, Deian Stefan, and Ranjit Jhala. 2019. IODINE: Verifying Constant-Time Execution of Hardware. In 28th USENIX Security Symposium (USENIX Security 19). 1411--1428."},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"crossref","unstructured":"Sumit Gulwani Oleksandr Polozov Rishabh Singh et al. 2017. Program synthesis. Foundations and Trends\u00ae in Programming Languages 4 1--2 (2017) 1--119.","DOI":"10.1561\/2500000010"},{"volume-title":"Testing of digital systems","author":"Jha Niraj K","key":"e_1_3_2_1_12_1","unstructured":"Niraj K Jha and Sandeep Gupta. 2003. Testing of digital systems. Cambridge University Press."},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1109\/CVPR.2015.7298965"},{"key":"e_1_3_2_1_14_1","unstructured":"Susumu Mashimo. 2017. Ridecore. https:\/\/github.com\/ridecore\/ridecore"},{"key":"e_1_3_2_1_15_1","unstructured":"Jamil Mazzawi and Ziyad Hanna. 2012. Formal Analysis of Security Data Paths in RTL Design (Slides). https:\/\/pdfs.semanticscholar.org\/2fb2\/96590738460f020ad786163bd90d7e2d3abf.pdf"},{"volume-title":"Hardware and Software: Verification and Testing (HVC12)","author":"Mazzawi Jamil","key":"e_1_3_2_1_16_1","unstructured":"Jamil Mazzawi and Ziyad Hanna. 2013. Formal Analysis of Security Data Paths in RTL Design (Abstract). In Hardware and Software: Verification and Testing (HVC12), Armin Biere, Amir Nahir, and Tanja Vos (Eds.). Springer Berlin Heidelberg."},{"key":"e_1_3_2_1_17_1","unstructured":"Nvidia. 2018. NVIDIA Deep Learning Accelerator. http:\/\/nvdla.org\/primer.html"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1109\/MM.2020.2996145"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2010.26"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3352460.3358302"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1109\/ISSCC42613.2021.9366062"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/1508244.1508258"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-96142-2_11"},{"key":"e_1_3_2_1_24_1","volume-title":"Automation & Test in Europe Conference & Exhibition (DATE). IEEE, 460--465","author":"Zeng Yu","year":"2022","unstructured":"Yu Zeng, Aarti Gupta, and Sharad Malik. 2022. Automatic generation of architecture-level models from RTL designs for processors and accelerators. In 2022 Design, Automation & Test in Europe Conference & Exhibition (DATE). IEEE, 460--465."},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD51958.2021.9643584"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICASID.2018.8693202"}],"event":{"name":"ICCAD '22: IEEE\/ACM International Conference on Computer-Aided Design","sponsor":["SIGDA ACM Special Interest Group on Design Automation","IEEE-EDS Electronic Devices Society","IEEE CAS","IEEE CEDA"],"location":"San Diego California","acronym":"ICCAD '22"},"container-title":["Proceedings of the 41st IEEE\/ACM International Conference on Computer-Aided Design"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3508352.3549391","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3508352.3549391","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T19:02:57Z","timestamp":1750186977000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3508352.3549391"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,10,30]]},"references-count":26,"alternative-id":["10.1145\/3508352.3549391","10.1145\/3508352"],"URL":"https:\/\/doi.org\/10.1145\/3508352.3549391","relation":{},"subject":[],"published":{"date-parts":[[2022,10,30]]},"assertion":[{"value":"2022-12-22","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}