{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,21]],"date-time":"2026-04-21T15:15:01Z","timestamp":1776784501484,"version":"3.51.2"},"publisher-location":"New York, NY, USA","reference-count":50,"publisher":"ACM","license":[{"start":{"date-parts":[[2024,4,27]],"date-time":"2024-04-27T00:00:00Z","timestamp":1714176000000},"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":[],"published-print":{"date-parts":[[2024,4,27]]},"DOI":"10.1145\/3620665.3640387","type":"proceedings-article","created":{"date-parts":[[2024,4,22]],"date-time":"2024-04-22T14:18:06Z","timestamp":1713795486000},"page":"416-432","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["FPGA Technology Mapping Using Sketch-Guided Program Synthesis"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9754-233X","authenticated-orcid":false,"given":"Gus Henry","family":"Smith","sequence":"first","affiliation":[{"name":"University of Washington, Seattle, United States of America"}]},{"ORCID":"https:\/\/orcid.org\/0009-0009-2504-1582","authenticated-orcid":false,"given":"Benjamin","family":"Kushigian","sequence":"additional","affiliation":[{"name":"University of Washington, Seattle, United States of America"}]},{"ORCID":"https:\/\/orcid.org\/0009-0001-5418-1279","authenticated-orcid":false,"given":"Vishal","family":"Canumalla","sequence":"additional","affiliation":[{"name":"University of Washington, Seattle, USA"}]},{"ORCID":"https:\/\/orcid.org\/0009-0006-0661-2640","authenticated-orcid":false,"given":"Andrew","family":"Cheung","sequence":"additional","affiliation":[{"name":"University of Washington, Seattle, USA"}]},{"ORCID":"https:\/\/orcid.org\/0009-0003-6747-7014","authenticated-orcid":false,"given":"Steven","family":"Lyubomirsky","sequence":"additional","affiliation":[{"name":"OctoAI, Seattle, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3900-5602","authenticated-orcid":false,"given":"Sorawee","family":"Porncharoenwase","sequence":"additional","affiliation":[{"name":"University of Washington, Seattle, United States of America"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5982-275X","authenticated-orcid":false,"given":"Ren\u00e9","family":"Just","sequence":"additional","affiliation":[{"name":"University of Washington, Seattle, United States of America"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3016-1169","authenticated-orcid":false,"given":"Gilbert Louis","family":"Bernstein","sequence":"additional","affiliation":[{"name":"University of Washington, Seattle, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4731-0124","authenticated-orcid":false,"given":"Zachary","family":"Tatlock","sequence":"additional","affiliation":[{"name":"University of Washington, Seattle, United States of America"}]}],"member":"320","published-online":{"date-parts":[[2024,4,27]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"Can not correctly infer \"A*B+C\" to DSP48E2. https:\/\/support.xilinx.com\/s\/question\/0D54U00006AqPXFSA3\/can-not-correctly-infer-abc-to-dsp48e2?language=en_US. Accessed: 2023-12-07."},{"key":"e_1_3_2_1_2_1","unstructured":"DSP48E2 inference for convolution\/multiplication of 8-bit operands. https:\/\/support.xilinx.com\/s\/question\/0D52E00006hpnGVSAY\/dsp48e2-inference-for-convolutionmultiplication-of-8bit-operands?language=en_US. Accessed: 2023-12-07."},{"key":"e_1_3_2_1_3_1","unstructured":"Eia-is-103 : Library of parameterized modules (lpm)."},{"key":"e_1_3_2_1_4_1","unstructured":"Inferring SIMD accumulator with Xilinx DSP48e2. https:\/\/old.reddit.com\/r\/FPGA\/comments\/tr9vzn\/inferring_simd_accumulator_with_xilinx_dsp48e2\/. Accessed: 2023-12-07."},{"key":"e_1_3_2_1_5_1","unstructured":"The simple theorem prover."},{"key":"e_1_3_2_1_6_1","unstructured":"Altera. Lpm quick reference guide."},{"key":"e_1_3_2_1_7_1","first-page":"1623","volume-title":"Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security, CCS '19","author":"Ardeshiricham Armaiti","year":"2019","unstructured":"Armaiti Ardeshiricham, Yoshiki Takashima, Sicun Gao, and Ryan Kastner. Verisketch: Synthesizing secure hardware designs with timing-sensitive information flow properties. In Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security, CCS '19, page 1623--1638, New York, NY, USA, 2019. Association for Computing Machinery."},{"key":"e_1_3_2_1_8_1","first-page":"415","volume-title":"cvc5: A Versatile and Industrial-Strength SMT Solver","author":"Barbosa Haniel","year":"2022","unstructured":"Haniel Barbosa, Clark Barrett, Martin Brain, Gereon Kremer, Hanna Lachnitt, Makai Mann, Abdalrhman Mohamed, Mudathir Mohamed, Aina Niemetz, Andres N\u00f6tzli, Alex Ozdemir, Mathias Preiner, Andrew Reynolds, Ying Sheng, Cesare Tinelli, and Yoni Zohar. cvc5: A Versatile and Industrial-Strength SMT Solver, pages 415--442. 01 2022."},{"key":"e_1_3_2_1_9_1","first-page":"1","volume-title":"Automation & Test in Europe Conference & Exhibition (DATE)","author":"Becker Andrew","year":"2014","unstructured":"Andrew Becker, David Novo, and Paolo Ienne. Sketchilog: Sketching combinational circuits. In 2014 Design, Automation & Test in Europe Conference & Exhibition (DATE), pages 1--4, 2014."},{"key":"e_1_3_2_1_10_1","volume-title":"Workshop on Languages, Tools, and Techniques for Accelerator Design (LATTE)","author":"Bernstein Gilbert Louis","year":"2021","unstructured":"Gilbert Louis Bernstein and Jonathan Ragan-Kelley. What are the semantics of hardware? In Workshop on Languages, Tools, and Techniques for Accelerator Design (LATTE), 2021."},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3140587.3062353"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3385965"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1109\/FCCM.2012.25"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14295-6_5"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110268"},{"key":"e_1_3_2_1_16_1","first-page":"139","volume-title":"Priyanka Raina, Clark Barrett, and Pat Hanrahan. Synthesizing instruction selection rewrite rules from rtl using smt. In CONFERENCE ON FORMAL METHODS IN COMPUTER-AIDED DESIGN-FMCAD","author":"Daly Ross","year":"2022","unstructured":"Ross Daly, Caleb Donovick, Jackson Melchert, Rajsekhar Setaluri, Nestan Tsiskaridze Bullock, Priyanka Raina, Clark Barrett, and Pat Hanrahan. Synthesizing instruction selection rewrite rules from rtl using smt. In CONFERENCE ON FORMAL METHODS IN COMPUTER-AIDED DESIGN-FMCAD 2022, page 139, 2022."},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_49"},{"key":"e_1_3_2_1_19_1","unstructured":"Bruno Dutertre and Leonardo De Moura. The yices smt solver."},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3127323"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3365609.3365858"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1561\/9781680832938"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3373087.3375310"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1109\/FCCM.2010.31"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1109\/FPL.2005.1515739"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3445814.3446755"},{"key":"e_1_3_2_1_28_1","volume-title":"FPGA, page 271","author":"Lysecky Roman L","year":"2005","unstructured":"Roman L Lysecky, Kris Miller, Frank Vahid, and Kees A Vissers. Firm-core virtual fpga for just-in-time fpga compilation. In FPGA, page 271, 2005."},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.7551\/mitpress\/4529.001.0001"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2006.887925"},{"key":"e_1_3_2_1_31_1","volume-title":"Bitwuzla at the smt-comp","author":"Niemetz Aina","year":"2020","unstructured":"Aina Niemetz and Mathias Preiner. Bitwuzla at the smt-comp 2020. arXiv preprint arXiv:2006.01621, 2020."},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-37703-7_1"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-96145-3_32"},{"key":"e_1_3_2_1_34_1","first-page":"69","volume-title":"Proceedings of the Second ACM\/IEEE International Conference on Formal Methods and Models for Co-Design, MEMOCODE '04","author":"Nikhil Rishiyur","year":"2004","unstructured":"Rishiyur Nikhil. Bluespec system verilog: Efficient, correct rtl from high level specifications. In Proceedings of the Second ACM\/IEEE International Conference on Formal Methods and Models for Co-Design, MEMOCODE '04, page 69--70, USA, 2004. IEEE Computer Society."},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/2666356.2594339"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498709"},{"key":"e_1_3_2_1_37_1","volume-title":"ABC: A system for sequential synthesis and verification","author":"Berkeley Logic Synthesis and Verification Group","year":"2005","unstructured":"Berkeley Logic Synthesis and Verification Group. ABC: A system for sequential synthesis and verification, 2005. http:\/\/www.eecs.berkeley.edu\/~alanmi\/abc."},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/2145694.2145708"},{"key":"e_1_3_2_1_39_1","volume-title":"Workshop on Languages, Tools, and Techniques for Accelerator Design-LATTE 2022","author":"Sisco Zachary D.","year":"2022","unstructured":"Zachary D. Sisco, Jonathan Balkind, Timothy Sherwood, and Ben Hardekopf. A position on program synthesis for processor development. In Workshop on Languages, Tools, and Techniques for Accelerator Design-LATTE 2022, 2022."},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/3591237"},{"key":"e_1_3_2_1_41_1","volume-title":"Program synthesis by sketching","author":"Solar-Lezama Armando","year":"2008","unstructured":"Armando Solar-Lezama. Program synthesis by sketching. University of California, Berkeley, 2008."},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1109\/FPL.2019.00065"},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1109\/FPL53798.2021.00085"},{"key":"e_1_3_2_1_44_1","first-page":"264","volume-title":"Proceedings of the 36th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '09","author":"Tate Ross","year":"2009","unstructured":"Ross Tate, Michael Stepp, Zachary Tatlock, and Sorin Lerner. Equality saturation: A new approach to optimization. In Proceedings of the 36th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '09, page 264--276, New York, NY, USA, 2009. Association for Computing Machinery."},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/2509578.2509586"},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/2666356.2594340"},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-53291-8_29"},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/3445814.3446707"},{"key":"e_1_3_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454075"},{"key":"e_1_3_2_1_50_1","volume-title":"Proceedings of the 21st Austrian Workshop on Microelectronics (Austrochip)","author":"Wolf Clifford","year":"2013","unstructured":"Clifford Wolf, Johann Glaser, and Johannes Kepler. Yosys-a free verilog synthesis suite. In Proceedings of the 21st Austrian Workshop on Microelectronics (Austrochip), 2013."},{"key":"e_1_3_2_1_51_1","volume-title":"Ultrascale architecture DSP slice user guide","year":"2021","unstructured":"Xilinx. Ultrascale architecture DSP slice user guide, 2021. https:\/\/docs.xilinx.com\/v\/u\/en-US\/ug579-ultrascale-dsp."}],"event":{"name":"ASPLOS '24: 29th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 2","location":"La Jolla CA USA","acronym":"ASPLOS '24","sponsor":["SIGARCH ACM Special Interest Group on Computer Architecture","SIGOPS ACM Special Interest Group on Operating Systems","SIGPLAN ACM Special Interest Group on Programming Languages","SIGBED ACM Special Interest Group on Embedded Systems"]},"container-title":["Proceedings of the 29th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 2"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3620665.3640387","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3620665.3640387","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T00:03:42Z","timestamp":1750291422000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3620665.3640387"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,4,27]]},"references-count":50,"alternative-id":["10.1145\/3620665.3640387","10.1145\/3620665"],"URL":"https:\/\/doi.org\/10.1145\/3620665.3640387","relation":{},"subject":[],"published":{"date-parts":[[2024,4,27]]},"assertion":[{"value":"2024-04-27","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}