{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,15]],"date-time":"2026-04-15T07:46:56Z","timestamp":1776239216408,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":60,"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-nc-sa\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2024,4,27]]},"DOI":"10.1145\/3622781.3674170","type":"proceedings-article","created":{"date-parts":[[2025,4,10]],"date-time":"2025-04-10T15:31:01Z","timestamp":1744299061000},"page":"63-78","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Control Logic Synthesis: Drawing the Rest of the OWL"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0009-0003-8349-7701","authenticated-orcid":false,"given":"Zachary D.","family":"Sisco","sequence":"first","affiliation":[{"name":"University of California, Santa Barbara, Santa Barbara, United States of America"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0001-6987-5724","authenticated-orcid":false,"given":"Andrew David","family":"Alex","sequence":"additional","affiliation":[{"name":"University of California, Santa Barbara, Santa Barbara, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0001-6315-1952","authenticated-orcid":false,"given":"Zechen","family":"Ma","sequence":"additional","affiliation":[{"name":"University of California, Santa Barbara, Santa Barbara, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7700-5112","authenticated-orcid":false,"given":"Yeganeh","family":"Aghamohammadi","sequence":"additional","affiliation":[{"name":"University of California, Santa Barbara, Santa Barbara, United States of America"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0007-8373-9685","authenticated-orcid":false,"given":"Boming","family":"Kong","sequence":"additional","affiliation":[{"name":"University of California, Santa Barbara, Santa Barbara, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7046-4589","authenticated-orcid":false,"given":"Benjamin","family":"Darnell","sequence":"additional","affiliation":[{"name":"University of Illinois Urbana-Champaign, Champaign, Illinois, United States of America"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6550-6075","authenticated-orcid":false,"given":"Timothy","family":"Sherwood","sequence":"additional","affiliation":[{"name":"University of California, Santa Barbara, Santa Barbara, United States of America"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0008-1199-6129","authenticated-orcid":false,"given":"Ben","family":"Hardekopf","sequence":"additional","affiliation":[{"name":"University of California, Santa Barbara, Santa Barbara, United States of America"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1443-1373","authenticated-orcid":false,"given":"Jonathan","family":"Balkind","sequence":"additional","affiliation":[{"name":"University of California, Santa Barbara, Santa Barbara, United States of America"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2025,4,10]]},"reference":[{"key":"e_1_3_2_1_1_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_2_1","volume-title":"Proc. 46th ACM SIGPLAN Symposium on Principles of Programming Languages, January 2019. Proc. ACM Program. Lang. 3, POPL, Article 71","author":"Armstrong Alasdair","unstructured":"Alasdair Armstrong, Thomas Bauereiss, Brian Campbell, Alastair Reid, Kathryn E. Gray, Robert M. Norton, Prashanth Mundkur, Mark Wassell, Jon French, Christopher Pulte, Shaked Flur, Ian Stark, Neel Krishnaswami, and Peter Sewell. ISA semantics for ARMv8-A, RISC-V, and CHERI-MIPS. In Proc. 46th ACM SIGPLAN Symposium on Principles of Programming Languages, January 2019. Proc. ACM Program. Lang. 3, POPL, Article 71."},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1145\/3341301.3359661","volume-title":"Proceedings of the 27th ACM Symposium on Operating Systems Principles","author":"Athalye Anish","year":"2019","unstructured":"Anish Athalye, Adam Belay, M. Frans Kaashoek, Robert Morris, and Nickolai Zeldovich. Notary: A device for secure transaction approval. In Proceedings of the 27th ACM Symposium on Operating Systems Principles, page 97--113, New York, NY, USA, 2019. Association for Computing Machinery."},{"key":"e_1_3_2_1_4_1","first-page":"503","volume-title":"16th USENIX Symposium on Operating Systems Design and Implementation (OSDI 22)","author":"Athalye Anish","year":"2022","unstructured":"Anish Athalye, M. Frans Kaashoek, and Nickolai Zeldovich. Verifying hardware security modules with Information-Preserving refinement. In 16th USENIX Symposium on Operating Systems Design and Implementation (OSDI 22), pages 503--519, Carlsbad, CA, July 2022. USENIX Association."},{"key":"e_1_3_2_1_5_1","first-page":"1","volume-title":"Automation Test in Europe Conference Exhibition (DATE)","author":"Becker A.","year":"2014","unstructured":"A. Becker, D. Novo, and P. 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_6_1","doi-asserted-by":"crossref","first-page":"391","DOI":"10.1109\/ACSSC.2013.6810303","volume-title":"2013 Asilomar Conference on Signals, Systems and Computers","author":"Becker Andrew","year":"2013","unstructured":"Andrew Becker, David Novo, and Paolo Ienne. Automated circuit elaboration from incomplete architectural descriptions. In 2013 Asilomar Conference on Signals, Systems and Computers, pages 391--395. IEEE, 2013."},{"key":"e_1_3_2_1_7_1","volume-title":"Proc. ACM Program. Lang., 2(OOPSLA)","author":"Bornholt James","year":"2018","unstructured":"James Bornholt and Emina Torlak. Finding code that explodes under symbolic evaluation. Proc. ACM Program. Lang., 2(OOPSLA), October 2018."},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"crossref","first-page":"24","DOI":"10.1007\/978-3-642-14295-6_5","volume-title":"Computer Aided Verification","author":"Brayton Robert","year":"2010","unstructured":"Robert Brayton and Alan Mishchenko. ABC: An academic industrial-strength verification tool. In Tayssir Touili, Byron Cook, and Paul Jackson, editors, Computer Aided Verification, pages 24--40, Berlin, Heidelberg, 2010. Springer Berlin Heidelberg."},{"key":"e_1_3_2_1_9_1","first-page":"1","volume-title":"Automation & Test in Europe Conference & Exhibition (DATE)","author":"Bruns Niklas","year":"2023","unstructured":"Niklas Bruns, Vladimir Herdt, and Rolf Drechsler. Processor verification using symbolic execution: A RISC-V case-study. In 2023 Design, Automation & Test in Europe Conference & Exhibition (DATE), pages 1--6, 2023."},{"key":"e_1_3_2_1_10_1","first-page":"68","volume-title":"Proceedings of the 6th International Conference on Computer Aided Verification, CAV '94","author":"Jerry","year":"1994","unstructured":"Jerry R. Burch and David L. Dill. Automatic verification of pipelined microprocessor control. In Proceedings of the 6th International Conference on Computer Aided Verification, CAV '94, page 68--80, Berlin, Heidelberg, 1994. Springer-Verlag."},{"key":"e_1_3_2_1_11_1","first-page":"41","volume-title":"Proceedings of the 44th Annual International Symposium on Computer Architecture, ISCA '17","author":"Cherupalli Hari","year":"2017","unstructured":"Hari Cherupalli, Henry Duwe, Weidong Ye, Rakesh Kumar, and John Sartori. Bespoke processors for applications with ultra-low area and power constraints. In Proceedings of the 44th Annual International Symposium on Computer Architecture, ISCA '17, page 41--54, New York, NY, USA, 2017. Association for Computing Machinery."},{"key":"e_1_3_2_1_12_1","first-page":"1","volume-title":"2017 27th International Conference on Field Programmable Logic and Applications (FPL)","author":"Clow J.","year":"2017","unstructured":"J. Clow, G. Tzimpragos, D. Dangwal, S. Guo, J. McMahan, and T. Sherwood. A pythonic approach for rapid hardware prototyping and instrumentation. In 2017 27th International Conference on Field Programmable Logic and Applications (FPL), pages 1--7, 2017."},{"key":"e_1_3_2_1_13_1","volume-title":"GCN","author":"Cui Ang","year":"2022","unstructured":"Ang Cui. The next frontier in cyberwar: Embedded devices. GCN, 2022."},{"key":"e_1_3_2_1_14_1","first-page":"1","volume-title":"2021 IEEE Nordic Circuits and Systems Conference (NorCAS)","author":"Dobis Andrew","year":"2021","unstructured":"Andrew Dobis, Tjark Petersen, Hans Jakob Damsgaard, Kasper Juul Hesse Rasmussen, Enrico Tolotto, Simon Thye Andersen, Richard Lin, and Martin Schoeberl. Chiselverify: An open-source hardware verification library for chisel and scala. In 2021 IEEE Nordic Circuits and Systems Conference (NorCAS), pages 1--7, 2021."},{"key":"e_1_3_2_1_15_1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"68","DOI":"10.1007\/978-3-540-78163-9_10","volume-title":"Verification, Model Checking, and Abstract Interpretation (VMCAI)","author":"D'Silva Vijay","year":"2008","unstructured":"Vijay D'Silva, Mitra Purandare, and Daniel Kroening. Approximation refinement for interpolation-based model checking. In Verification, Model Checking, and Abstract Interpretation (VMCAI), volume 4905 of Lecture Notes in Computer Science, pages 68--82. Springer, 2008."},{"key":"e_1_3_2_1_16_1","volume-title":"Wilson research group functional verification study. https:\/\/blogs.sw.siemens.com\/verificationhorizons\/2020\/10\/27\/prologue-the-2020-wilson-research-group-functional-verification-study\/","author":"Foster Harry","year":"2020","unstructured":"Harry Foster. Wilson research group functional verification study. https:\/\/blogs.sw.siemens.com\/verificationhorizons\/2020\/10\/27\/prologue-the-2020-wilson-research-group-functional-verification-study\/, 2020."},{"key":"e_1_3_2_1_17_1","first-page":"24","volume-title":"2021 Formal Methods in Computer Aided Design (FMCAD)","author":"Gao Dapeng","year":"2021","unstructured":"Dapeng Gao and Tom Melham. End-to-end formal verification of a risc-v processor extended with capability pointers. In 2021 Formal Methods in Computer Aided Design (FMCAD), pages 24--33, 2021."},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"crossref","first-page":"413","DOI":"10.1007\/978-3-030-45190-5_23","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Goel Aman","year":"2020","unstructured":"Aman Goel and Karem Sakallah. Avr: Abstractly verifying reachability. In Armin Biere and David Parker, editors, Tools and Algorithms for the Construction and Analysis of Systems, pages 413--422, Cham, 2020. Springer International Publishing."},{"issue":"2","key":"e_1_3_2_1_19_1","doi-asserted-by":"crossref","first-page":"60","DOI":"10.1109\/40.848473","article-title":"a configurable and extensible processor","volume":"20","author":"Gonzalez R.E.","year":"2000","unstructured":"R.E. Gonzalez. Xtensa: a configurable and extensible processor. IEEE Micro, 20(2):60--70, 2000.","journal-title":"IEEE Micro"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"crossref","first-page":"521","DOI":"10.1007\/10722167_39","volume-title":"Computer Aided Verification","author":"Hosabettu Ravi","year":"2000","unstructured":"Ravi Hosabettu, Ganesh Gopalakrishnan, and Mandayam Srivas. Verifying advanced microarchitectures that support speculation and exceptions. In E. Allen Emerson and Aravinda Prasad Sistla, editors, Computer Aided Verification, pages 521--537, Berlin, Heidelberg, 2000. Springer Berlin Heidelberg."},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"crossref","first-page":"679","DOI":"10.1145\/3466752.3480087","volume-title":"MICRO-54:  54th Annual IEEE\/ACM International Symposium on Microarchitecture, MICRO '21","author":"Hsiao Yao","year":"2021","unstructured":"Yao Hsiao, Dominic P. Mulligan, Nikos Nikoleris, Gustavo Petri, and Caroline Trippel. Synthesizing formal models of hardware from RTL for efficient verification of memory model implementations. In MICRO-54: 54th Annual IEEE\/ACM International Symposium on Microarchitecture, MICRO '21, page 679--694, New York, NY, USA, 2021. Association for Computing Machinery."},{"key":"e_1_3_2_1_22_1","volume-title":"https:\/\/github.com\/PrincetonUniversity\/IMDb-Archive","author":"Huang Bo-Yuan","year":"2018","unstructured":"Bo-Yuan Huang. Imdb-archive. https:\/\/github.com\/PrincetonUniversity\/IMDb-Archive, 2018."},{"key":"e_1_3_2_1_23_1","first-page":"91","volume-title":"Proc. Design Automation Conference","author":"Huang Bo-Yuan","year":"2018","unstructured":"Bo-Yuan Huang, Sayak Ray, Aarti Gupta, Jason M. Fung, and Sharad Malik. Formal Security Verification of Concurrent Firmware in SoCs using Instruction-Level Abstraction for Hardware. In Proc. Design Automation Conference, page 91, 2018."},{"key":"e_1_3_2_1_24_1","first-page":"351","volume-title":"Proc. Int. Conf. Tools and Algorithms for the Construction and Analysis of Systems","author":"Huang Bo-Yuan","year":"2019","unstructured":"Bo-Yuan Huang, Hongce Zhang, Aarti Gupta, and Sharad Malik. ILAng: A Modeling and Verification Platform for SoCs using Instruction-Level Abstractions. In Proc. Int. Conf. Tools and Algorithms for the Construction and Analysis of Systems, pages 351--357, 2019."},{"key":"e_1_3_2_1_25_1","volume-title":"Instruction-level abstraction (ila): A uniform specification for system-on-chip (soc) verification. ACM Trans. Des. Autom. Electron. Syst., 24(1), dec","author":"Huang Bo-Yuan","year":"2018","unstructured":"Bo-Yuan Huang, Hongce Zhang, Pramod Subramanyan, Yakir Vizel, Aarti Gupta, and Sharad Malik. Instruction-level abstraction (ila): A uniform specification for system-on-chip (soc) verification. ACM Trans. Des. Autom. Electron. Syst., 24(1), dec 2018."},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"crossref","first-page":"396","DOI":"10.1007\/3-540-44585-4_40","volume-title":"Proceedings of the 13th International Conference on Computer Aided Verification, CAV '01","author":"Jhala Ranjit","year":"2001","unstructured":"Ranjit Jhala and Kenneth L. McMillan. Microarchitecture verification by compositional model checking. In Proceedings of the 13th International Conference on Computer Aided Verification, CAV '01, page 396--410, Berlin, Heidelberg, 2001. Springer-Verlag."},{"key":"e_1_3_2_1_27_1","first-page":"79","volume-title":"Proceedings of the Third International Workshop on Bounded Model Checking (BMC 2005","volume":"144","author":"Kroening Daniel","year":"2006","unstructured":"Daniel Kroening. Computing over-approximations with bounded model checking. In Proceedings of the Third International Workshop on Bounded Model Checking (BMC 2005), volume 144, pages 79--92, January 2006."},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"crossref","first-page":"1041","DOI":"10.1145\/3314221.3314622","volume-title":"Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2019","author":"L\u00f6\u00f6w Andreas","year":"2019","unstructured":"Andreas L\u00f6\u00f6w, Ramana Kumar, Yong Kiam Tan, Magnus O. Myreen, Michael Norrish, Oskar Abrahamsson, and Anthony Fox. Verified compilation on a verified processor. In Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2019, page 1041--1053, New York, NY, USA, 2019. Association for Computing Machinery."},{"key":"e_1_3_2_1_29_1","volume-title":"Ibex: An embedded 32 bit RISC-V CPU core. https:\/\/ibex-core.readthedocs.io\/en\/latest\/","author":"RISC.","year":"2018","unstructured":"lowRISC. Ibex: An embedded 32 bit RISC-V CPU core. https:\/\/ibex-core.readthedocs.io\/en\/latest\/, 2018."},{"key":"e_1_3_2_1_30_1","volume-title":"https:\/\/docs.opentitan.org\/","author":"Opentitan RISC.","year":"2022","unstructured":"lowRISC. Opentitan. https:\/\/docs.opentitan.org\/, 2022."},{"key":"e_1_3_2_1_31_1","volume-title":"Soc protocol implementation verification using instruction-level abstraction specifications. ACM Trans. Des. Autom. Electron. Syst., 28(6), oct","author":"Lu Huaixi","year":"2023","unstructured":"Huaixi Lu, Yue Xing, Aarti Gupta, and Sharad Malik. Soc protocol implementation verification using instruction-level abstraction specifications. ACM Trans. Des. Autom. Electron. Syst., 28(6), oct 2023."},{"issue":"3","key":"e_1_3_2_1_32_1","doi-asserted-by":"crossref","first-page":"72","DOI":"10.1109\/MM.2015.47","article-title":"Verifying correct microarchitectural enforcement of memory consistency models","volume":"35","author":"Lustig Daniel","year":"2015","unstructured":"Daniel Lustig, Michael Pellauer, and Margaret Martonosi. Verifying correct microarchitectural enforcement of memory consistency models. IEEE Micro, 35(3):72--82, 2015.","journal-title":"IEEE Micro"},{"key":"e_1_3_2_1_33_1","first-page":"233","volume-title":"Proceedings of the Twenty-First International Conference on Architectural Support for Programming Languages and Operating Systems, ASPLOS '16","author":"Lustig Daniel","year":"2016","unstructured":"Daniel Lustig, Geet Sethi, Margaret Martonosi, and Abhishek Bhattacharjee. COATCheck: Verifying memory ordering at the hardware-OS interface. In Proceedings of the Twenty-First International Conference on Architectural Support for Programming Languages and Operating Systems, ASPLOS '16, page 233--247, New York, NY, USA, 2016. Association for Computing Machinery."},{"key":"e_1_3_2_1_34_1","first-page":"463","volume-title":"Proceedings of the 50th Annual IEEE\/ACM International Symposium on Microarchitecture, MICRO-50 '17","author":"Manerkar Yatin A.","year":"2017","unstructured":"Yatin A. Manerkar, Daniel Lustig, Margaret Martonosi, and Michael Pellauer. RTLcheck: Verifying the memory consistency of RTL designs. In Proceedings of the 50th Annual IEEE\/ACM International Symposium on Microarchitecture, MICRO-50 '17, page 463--476, New York, NY, USA, 2017. Association for Computing Machinery."},{"key":"e_1_3_2_1_35_1","first-page":"26","volume-title":"2015 48th Annual IEEE\/ACM International Symposium on Microarchitecture (MICRO)","author":"Manerkar Yatin A.","year":"2015","unstructured":"Yatin A. Manerkar, Daniel Lustig, Michael Pellauer, and Margaret Martonosi. CCICheck: Using \u03bchb graphs to verify the coherence-consistency interface. In 2015 48th Annual IEEE\/ACM International Symposium on Microarchitecture (MICRO), pages 26--37, 2015."},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"crossref","first-page":"461","DOI":"10.1007\/978-3-030-81688-9_22","volume-title":"Computer Aided Verification","author":"Mann Makai","year":"2021","unstructured":"Makai Mann, Ahmed Irfan, Florian Lonsing, Yahan Yang, Hongce Zhang, Kristopher Brown, Aarti Gupta, and Clark Barrett. Pono: A flexible and extensible smt-based model checker. In Alexandra Silva and K. Rustan M. Leino, editors, Computer Aided Verification, pages 461--474, Cham, 2021. Springer International Publishing."},{"issue":"4","key":"e_1_3_2_1_37_1","doi-asserted-by":"crossref","first-page":"353","DOI":"10.1109\/TVLSI.2008.918120","article-title":"A refinement-based compositional reasoning framework for pipelined machine verification","volume":"16","author":"Manolios Panagiotis","year":"2008","unstructured":"Panagiotis Manolios and Sudarshan K. Srinivasan. A refinement-based compositional reasoning framework for pipelined machine verification. IEEE Transactions on Very Large Scale Integration (VLSI) Systems, 16(4):353--364, 2008.","journal-title":"IEEE Transactions on Very Large Scale Integration (VLSI) Systems"},{"key":"e_1_3_2_1_38_1","first-page":"1","volume-title":"2018 Formal Methods in Computer Aided Design (FMCAD)","author":"Mattarei Cristian","year":"2018","unstructured":"Cristian Mattarei, Makai Mann, Clark Barrett, Ross G. Daly, Dillon Huff, and Pat Hanrahan. CoSA: Integrated verification for agile hardware design. In 2018 Formal Methods in Computer Aided Design (FMCAD), pages 1--5, 2018."},{"key":"e_1_3_2_1_39_1","volume-title":"A methodology for hardware verification using compositional model checking. Sci. Comput. Program., 37(1--3):279--309, may","author":"McMillan K. L.","year":"2000","unstructured":"K. L. McMillan. A methodology for hardware verification using compositional model checking. Sci. Comput. Program., 37(1--3):279--309, may 2000."},{"key":"e_1_3_2_1_40_1","first-page":"7","volume-title":"IEEE Computer Society Annual Symposium on VLSI","author":"Mukherjee Rajdeep","year":"2015","unstructured":"Rajdeep Mukherjee, Daniel Kroening, and Tom Melham. Hardware verification using software analyzers. In IEEE Computer Society Annual Symposium on VLSI, pages 7--12. IEEE, 2015."},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"crossref","first-page":"225","DOI":"10.1145\/3341301.3359641","volume-title":"Proceedings of the 27th ACM Symposium on Operating Systems Principles, SOSP '19","author":"Nelson Luke","year":"2019","unstructured":"Luke Nelson, James Bornholt, Ronghui Gu, Andrew Baumann, Emina Torlak, and Xi Wang. Scaling symbolic evaluation for automated verification of systems code with serval. In Proceedings of the 27th ACM Symposium on Operating Systems Principles, SOSP '19, page 225--242, New York, NY, USA, 2019. Association for Computing Machinery."},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1109\/MEMCOD.2004.1459818","volume-title":"Proceedings. Second ACM and IEEE International Conference on Formal Methods and Models for Co-Design, 2004. MEMOCODE '04.","author":"Nikhil R.","year":"2004","unstructured":"R. Nikhil. Bluespec System Verilog: Efficient, correct RTL from high level specifications. In Proceedings. Second ACM and IEEE International Conference on Formal Methods and Models for Co-Design, 2004. MEMOCODE '04., pages 69--70, 2004."},{"key":"e_1_3_2_1_43_1","first-page":"42","volume-title":"Computer Aided Verification","author":"Reid Alastair","year":"2016","unstructured":"Alastair Reid, Rick Chen, Anastasios Deligiannis, David Gilday, David Hoyes, Will Keen, Ashan Pathirane, Owen Shepherd, Peter Vrabel, and Ali Zaidi. End-to-end verification of processors with isa-formal. In Swarat Chaudhuri and Azadeh Farzan, editors, Computer Aided Verification, pages 42--58, Cham, 2016. Springer International Publishing."},{"key":"e_1_3_2_1_44_1","first-page":"110","volume-title":"2023 Formal Methods in Computer Aided Design (FMCAD)","author":"Ryan Kaki","year":"2023","unstructured":"Kaki Ryan and Cynthia Sturton. Sylvia: Countering the path explosion problem in the symbolic execution of hardware designs. In 2023 Formal Methods in Computer Aided Design (FMCAD), pages 110--121, 2023."},{"issue":"2","key":"e_1_3_2_1_45_1","doi-asserted-by":"crossref","first-page":"187","DOI":"10.1023\/A:1014122630277","article-title":"Verification of FM9801: An out-of-order microprocessor model with speculative execution, exceptions, and program-modifying capability","volume":"20","author":"Sawada Jun","year":"2002","unstructured":"Jun Sawada and Warren A Hunt. Verification of FM9801: An out-of-order microprocessor model with speculative execution, exceptions, and program-modifying capability. Formal Methods in System Design, 20(2):187--222, 2002.","journal-title":"Formal Methods in System Design"},{"issue":"337","key":"e_1_3_2_1_46_1","first-page":"a64","article-title":"Supervised autonomous robotic soft tissue surgery","volume":"8","author":"Shademan Azad","year":"2016","unstructured":"Azad Shademan, Ryan S. Decker, Justin D. Opfermann, Simon Leonard, Axel Krieger, and Peter C. W. Kim. Supervised autonomous robotic soft tissue surgery. Science Translational Medicine, 8(337):337ra64--337ra64, 2016.","journal-title":"Science Translational Medicine"},{"key":"e_1_3_2_1_47_1","volume-title":"Proc. ACM Program. Lang., 7(PLDI), jun","author":"Sisco Zachary D.","year":"2023","unstructured":"Zachary D. Sisco, Jonathan Balkind, Timothy Sherwood, and Ben Hardekopf. Loop rerolling for hardware decompilation. Proc. ACM Program. Lang., 7(PLDI), jun 2023."},{"key":"e_1_3_2_1_48_1","first-page":"160","volume-title":"Sharad Malik. Template-based Synthesis of Instruction-Level Abstractions for SoC Verification. In Proceedings of the Conference on Formal Methods in Computer-Aided Design","author":"Subramanyan Pramod","year":"2017","unstructured":"Pramod Subramanyan, Yakir Vizel, Sayak Ray, and Sharad Malik. Template-based Synthesis of Instruction-Level Abstractions for SoC Verification. In Proceedings of the Conference on Formal Methods in Computer-Aided Design, pages 160--167, 2017."},{"key":"e_1_3_2_1_49_1","volume-title":"Inc.","author":"Systems Cadence Design","year":"2016","unstructured":"Cadence Design Systems. TIE language---the fast path to high-performance embedded SoC processing. Technical report, Cadence Design Systems, Inc., San Jose, CA, USA, 2016."},{"key":"e_1_3_2_1_50_1","doi-asserted-by":"crossref","first-page":"135","DOI":"10.1145\/2509578.2509586","volume-title":"Proceedings of the 2013 ACM International Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software, Onward! 2013","author":"Torlak Emina","year":"2013","unstructured":"Emina Torlak and Rastislav Bodik. Growing solver-aided languages with Rosette. In Proceedings of the 2013 ACM International Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software, Onward! 2013, page 135--152, New York, NY, USA, 2013. Association for Computing Machinery."},{"issue":"6","key":"e_1_3_2_1_51_1","doi-asserted-by":"crossref","first-page":"530","DOI":"10.1145\/2666356.2594340","article-title":"A lightweight symbolic virtual machine for solver-aided host languages","volume":"49","author":"Torlak Emina","year":"2014","unstructured":"Emina Torlak and Rastislav Bodik. A lightweight symbolic virtual machine for solver-aided host languages. SIGPLAN Not., 49(6):530--541, June 2014.","journal-title":"SIGPLAN Not."},{"key":"e_1_3_2_1_52_1","first-page":"429","volume-title":"Proceedings of the 2021 ACM SIGSAC Conference on Computer and Communications Security, CCS '21","author":"v. Gleissenthall Klaus","year":"2021","unstructured":"Klaus v. Gleissenthall, Rami G\u00f6khan K\u0131c\u0131, Deian Stefan, and Ranjit Jhala. Solver-aided constant-time hardware verification. In Proceedings of the 2021 ACM SIGSAC Conference on Computer and Communications Security, CCS '21, page 429--444, New York, NY, USA, 2021. Association for Computing Machinery."},{"key":"e_1_3_2_1_53_1","first-page":"112","volume-title":"Proceedings of the 37th Annual Design Automation Conference, DAC '00","author":"Miroslav","year":"2000","unstructured":"Miroslav N. Velev and Randal E. Bryant. Formal verification of super-scale microprocessors with multicycle functional units, exception, and branch prediction. In Proceedings of the 37th Annual Design Automation Conference, DAC '00, page 112--117, New York, NY, USA, 2000. Association for Computing Machinery."},{"key":"e_1_3_2_1_54_1","volume-title":"Yosys Open SYnthesis Suite. https:\/\/yosyshq.net\/yosys\/","author":"Wolf Claire","year":"2022","unstructured":"Claire Wolf. Yosys Open SYnthesis Suite. https:\/\/yosyshq.net\/yosys\/, 2022."},{"key":"e_1_3_2_1_55_1","volume-title":"Proceedings of the 50th Annual International Symposium on Computer Architecture, ISCA '23","author":"Yang Yuheng","year":"2023","unstructured":"Yuheng Yang, Thomas Bourgeat, Stella Lau, and Mengjia Yan. Pensieve: Microarchitectural modeling for security evaluation. In Proceedings of the 50th Annual International Symposium on Computer Architecture, ISCA '23, New York, NY, USA, 2023. Association for Computing Machinery."},{"key":"e_1_3_2_1_56_1","volume-title":"https:\/\/github.com\/YosysHQ\/sby","author":"Symbiyosys HQ.","year":"2022","unstructured":"YosysHQ. Symbiyosys. https:\/\/github.com\/YosysHQ\/sby, 2022."},{"key":"e_1_3_2_1_57_1","volume-title":"Proceedings of the 43rd ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2022","author":"Zagieboylo Drew","year":"2022","unstructured":"Drew Zagieboylo, Charles Sherk, Edward Suh, and Andrew Myers. PDL a high-level hardware design language for pipelined processors. In Proceedings of the 43rd ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2022, New York, NY, USA, 6 2022. Association for Computing Machinery."},{"key":"e_1_3_2_1_58_1","first-page":"1","volume-title":"Sharad Malik. ILA-MCM: Integrating Memory Consistency Models with Instruction-Level Abstractions for Heterogeneous System-on-Chip Verification. In Proc. Conf. Formal Methods in Computer-Aided Design","author":"Zhang Hongce","year":"2018","unstructured":"Hongce Zhang, Caroline Trippel, Yatin A Manerkar, Aarti Gupta, Margaret Martonosi, and Sharad Malik. ILA-MCM: Integrating Memory Consistency Models with Instruction-Level Abstractions for Heterogeneous System-on-Chip Verification. In Proc. Conf. Formal Methods in Computer-Aided Design, pages 1--10, 2018."},{"key":"e_1_3_2_1_59_1","first-page":"202","volume-title":"Synthesizing environment invariants for modular hardware verification","author":"Zhang Hongce","year":"2020","unstructured":"Hongce Zhang, Weikun Yang, Grigory Fedyukovich, Aarti Gupta, and Sharad Malik. Synthesizing environment invariants for modular hardware verification. In Dirk Beyer and Damien Zufferey, editors, Verification, Model Checking, and Abstract Interpretation, pages 202--225, Cham, 2020. Springer International Publishing."},{"key":"e_1_3_2_1_60_1","first-page":"14","article-title":"Simulation and satisfiability in logic synthesis","volume":"7","author":"Zhang Jin S","year":"2005","unstructured":"Jin S Zhang, Subarna Sinha, Alan Mishchenko, Robert K Brayton, and Malgorzata Chrzanowska-Jeske. Simulation and satisfiability in logic synthesis. Computing, 7:14, 2005.","journal-title":"Computing"}],"event":{"name":"ASPLOS '24: 29th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 4","location":"Hilton La Jolla Torrey Pines La Jolla CA USA","acronym":"ASPLOS '24","sponsor":["SIGOPS ACM Special Interest Group on Operating Systems","SIGPLAN ACM Special Interest Group on Programming Languages","SIGARCH ACM Special Interest Group on Computer Architecture","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 4"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3622781.3674170","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3622781.3674170","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:37:03Z","timestamp":1750178223000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3622781.3674170"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,4,27]]},"references-count":60,"alternative-id":["10.1145\/3622781.3674170","10.1145\/3622781"],"URL":"https:\/\/doi.org\/10.1145\/3622781.3674170","relation":{},"subject":[],"published":{"date-parts":[[2024,4,27]]},"assertion":[{"value":"2025-04-10","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}