{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,11]],"date-time":"2026-06-11T16:04:33Z","timestamp":1781193873715,"version":"3.54.1"},"publisher-location":"Cham","reference-count":70,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032280787","type":"print"},{"value":"9783032280794","type":"electronic"}],"license":[{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"DOI":"10.1007\/978-3-032-28079-4_12","type":"book-chapter","created":{"date-parts":[[2026,6,11]],"date-time":"2026-06-11T15:33:45Z","timestamp":1781192025000},"page":"261-284","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Artificial Incorrectness: SMT and\u00a0LLMs in\u00a0Hardware Synthesis"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9404-2954","authenticated-orcid":false,"given":"Edward","family":"Wang","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0003-9697-9144","authenticated-orcid":false,"given":"Joe","family":"Walston","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5880-3151","authenticated-orcid":false,"given":"Luca","family":"Daniel","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0005-8341-2004","authenticated-orcid":false,"given":"Tony","family":"Tan","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2972-6695","authenticated-orcid":false,"given":"Yoni","family":"Zohar","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9522-3084","authenticated-orcid":false,"given":"Clark","family":"Barrett","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2026,6,12]]},"reference":[{"key":"12_CR1","doi-asserted-by":"crossref","unstructured":"Abate, A., David, C., Kesseli, P., Kroening, D., Polgreen, E.: Counterexample guided inductive synthesis modulo theories. In: Chockler, H., Weissenbacher, G. (eds.) Computer Aided Verification. pp. 270\u2013288. Springer International Publishing, Cham (2018). http:\/\/www.kroening.com\/papers\/cav2018-synthesis.pdf","DOI":"10.1007\/978-3-319-96145-3_15"},{"key":"12_CR2","doi-asserted-by":"publisher","unstructured":"Abdollahi, M., Yeganli, S.F., Baharloo, A., Baniasadi, A.: Hardware design and verification with large language models: a scoping review, challenges, and open issues. Electronics 14(1) (2025). https:\/\/doi.org\/10.3390\/electronics14010120, http:\/\/www.mdpi.com\/2079-9292\/14\/1\/120","DOI":"10.3390\/electronics14010120"},{"key":"12_CR3","doi-asserted-by":"crossref","unstructured":"Aggarwal, P., Madaan, A., Yang, Y., Mausam: Let\u2019s sample step by step: adaptive-consistency for efficient reasoning and coding with LLMs (2023). http:\/\/arxiv.org\/abs\/2305.11860","DOI":"10.18653\/v1\/2023.emnlp-main.761"},{"key":"12_CR4","doi-asserted-by":"crossref","unstructured":"Akyash, M., Azar, K., Kamali, H.: RTL++: Graph-enhanced LLM for RTL code generation (2025). http:\/\/arxiv.org\/abs\/2505.13479","DOI":"10.1109\/ICLAD65226.2025.00020"},{"issue":"3","key":"12_CR5","doi-asserted-by":"publisher","first-page":"2392","DOI":"10.1016\/j.jer.2024.08.001","volume":"13","author":"S Alsaqer","year":"2025","unstructured":"Alsaqer, S., Alajmi, S., Ahmad, I., Alfailakawi, M.: The potential of LLMs in hardware design. J. Eng. Res. 13(3), 2392\u20132404 (2025). https:\/\/doi.org\/10.1016\/j.jer.2024.08.001","journal-title":"J. Eng. Res."},{"key":"12_CR6","doi-asserted-by":"publisher","unstructured":"Alur, R., et al.: Syntax-guided synthesis. In: 2013 Formal Methods in Computer-Aided Design, pp.\u00a01\u20138 (2013). https:\/\/doi.org\/10.1109\/FMCAD.2013.6679385","DOI":"10.1109\/FMCAD.2013.6679385"},{"key":"12_CR7","unstructured":"Baartmans, R., Ensinger, A., Agostinelli, V., Chen, L.: ML for hardware design interpretability: challenges and opportunities. arXiv (2025)"},{"key":"12_CR8","doi-asserted-by":"publisher","unstructured":"Bachrach, J., et al.: Chisel: constructing hardware in a Scala embedded language. pp. 1216\u20131225. ACM (2012). https:\/\/doi.org\/10.1145\/2228360.2228584, http:\/\/people.eecs.berkeley.edu\/~krste\/papers\/chisel-dac2012.pdf","DOI":"10.1145\/2228360.2228584"},{"key":"12_CR9","unstructured":"Bailey, B.: What will that chip cost? (2023). http:\/\/web.archive.org\/web\/20240719072950\/https:\/\/semiengineering.com\/what-will-that-chip-cost\/"},{"key":"12_CR10","doi-asserted-by":"crossref","unstructured":"Barbosa, H., et al.: cvc5: a versatile and industrialstrength SMT solver. In: Fisman, D., Rosu, G. (eds.) Tools and Algorithms for the Construction and Analysis of Systems. pp. 415\u2013442. Springer International Publishing, Cham (2022). http:\/\/www-cs.stanford.edu\/\u00a0preiner\/publications\/2022\/BarbosaBBKLMMMN-TACAS22.pdf","DOI":"10.1007\/978-3-030-99524-9_24"},{"key":"12_CR11","unstructured":"Barendregt, H.P.: The quest for correctness. Amsterdam: Stichting Mathematisch Centrum (1996). http:\/\/repository.ubn.ru.nl\/bitstream\/handle\/2066\/17273\/13361.pdf"},{"key":"12_CR12","doi-asserted-by":"publisher","unstructured":"Barrett, C., Sebastiani, R., Seshia, S., Tinelli, C.: Satisfiability modulo theories. In: Biere, A., Heule, M.J.H., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability, Second Edition, Frontiers in Artificial Intelligence and Applications, vol.\u00a0336, chap.\u00a033, pp. 825\u2013885. IOS Press (2021). https:\/\/doi.org\/10.3233\/FAIA201017, http:\/\/theory.stanford.edu\/~barrett\/pubs\/BSST21.pdf","DOI":"10.3233\/FAIA201017"},{"key":"12_CR13","unstructured":"Benveniste, A., et al.: Contracts for systems design: theory. Research Report RR-8759, Inria Rennes Bretagne Atlantique ; INRIA (2015). http:\/\/inria.hal.science\/hal-01178467"},{"key":"12_CR14","doi-asserted-by":"publisher","unstructured":"Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) Tools and Algorithms for the Construction and Analysis of Systems, pp. 193\u2013207. Springer Berlin Heidelberg, Berlin, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-49059-0_14","DOI":"10.1007\/3-540-49059-0_14"},{"key":"12_CR15","doi-asserted-by":"publisher","unstructured":"Bozzano, M., et al.: Mathsat: Tight integration of sat and mathematical decision procedures. J. Autom. Reasoning 35(1), 265\u2013293 (2005). https:\/\/doi.org\/10.1007\/s10817-005-9004-z, http:\/\/brenta.dit.unitn.it\/~rseba\/papers\/jar_sat05.pdf","DOI":"10.1007\/s10817-005-9004-z"},{"key":"12_CR16","doi-asserted-by":"publisher","first-page":"168","DOI":"10.1007\/978-3-540-24730-2_15","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E Clarke","year":"2004","unstructured":"Clarke, E., Kroening, D., Lerda, F.: A tool for checking ANSI-C programs. In: Jensen, K., Podelski, A. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, pp. 168\u2013176. Springer, Berlin Heidelberg, Berlin, Heidelberg (2004)"},{"key":"12_CR17","unstructured":"Cook, H., Terpstra, W., Lee, Y.: Diplomatic design patterns: a TileLink case study. In: 1st Workshop on Computer Architecture Research with RISC-V, vol.\u00a023 (2017). http:\/\/carrv.github.io\/2017\/papers\/cook-diplomacy-carrv2017.pdf"},{"key":"12_CR18","doi-asserted-by":"publisher","unstructured":"Donda, K., Brahmkhatri, P., Zhu, Y., Dey, B., Slesarenko, V.: Machine learning for inverse design of acoustic and elastic metamaterials. Curr. Opin. Solid State Mater. Sci. 35, 101218 (2025). https:\/\/doi.org\/10.1016\/j.cossms.2025.101218, http:\/\/www.sciencedirect.com\/science\/article\/pii\/S1359028625000051","DOI":"10.1016\/j.cossms.2025.101218"},{"key":"12_CR19","unstructured":"Dutertre, B., De\u00a0Moura, L.: The yices SMT solver. SRI International Computer Science Laboratory Technical Reports (2006). http:\/\/yices.csl.sri.com\/papers\/tool-paper.pdf"},{"key":"12_CR20","doi-asserted-by":"publisher","unstructured":"Faghih, F., Bonakdarpour, B.: SMT-based synthesis of distributed self-stabilizing systems. ACM Trans. Auton. Adapt. Syst. 10(3) (2015). https:\/\/doi.org\/10.1145\/2767133","DOI":"10.1145\/2767133"},{"key":"12_CR21","doi-asserted-by":"publisher","unstructured":"Fei, W., et al.: Extending context window of large language models via semantic compression. In: Ku, L.W., Martins, A., Srikumar, V. (eds.) Findings of the Association for Computational Linguistics: ACL 2024, pp. 5169\u20135181. Association for Computational Linguistics, Bangkok, Thailand (2024). https:\/\/doi.org\/10.18653\/v1\/2024.findings-acl.306, http:\/\/aclanthology.org\/2024.findings-acl.306\/","DOI":"10.18653\/v1\/2024.findings-acl.306"},{"key":"12_CR22","unstructured":"Gadde, D.N., Kumar, A., Nalapat, T., Rezunov, E., Cappellini, F.: All artificial, less intelligence: GenAI through the lens of formal verification (2024). http:\/\/arxiv.org\/abs\/2403.16750"},{"key":"12_CR23","doi-asserted-by":"publisher","unstructured":"Gadde, D.N., et al.: Hey AI, generate me a hardware code, agentic AI-based hardware design and verification. In: 2025 38th SBC\/SBMicro\/IEEE Symposium on Integrated Circuits and Systems Design (SBCCI), pp.\u00a01\u20135 (2025). https:\/\/doi.org\/10.1109\/SBCCI66862.2025.11218681","DOI":"10.1109\/SBCCI66862.2025.11218681"},{"key":"12_CR24","unstructured":"Gao, Z., Boning, D.S.: A review of Bayesian methods in electronic design automation (2023). http:\/\/arxiv.org\/abs\/2304.09723"},{"key":"12_CR25","doi-asserted-by":"publisher","first-page":"579","DOI":"10.1007\/978-3-031-71162-6_30","volume-title":"Formal Methods","author":"B Greenman","year":"2025","unstructured":"Greenman, B., et al.: Misconceptions in finite-trace and infinite-trace linear temporal logic. In: Platzer, A., Rozier, K.Y., Pradella, M., Rossi, M. (eds.) Formal Methods, pp. 579\u2013599. Springer Nature Switzerland, Cham (2025)"},{"key":"12_CR26","doi-asserted-by":"publisher","unstructured":"Hitarth, S., Codel, C., Lachnitt, H., Dutertre, B.: Extending DRAT to SMT. In: 2024 Formal Methods in Computer-Aided Design (FMCAD), pp. 01\u201311 (2024). https:\/\/doi.org\/10.34727\/2024\/isbn.978-3-85448-065-5_8","DOI":"10.34727\/2024\/isbn.978-3-85448-065-5_8"},{"key":"12_CR27","unstructured":"Jayarama, K.: A case study on effective pipeline design in digital systems (2024), http:\/\/web.archive.org\/web\/20250522085640\/https:\/\/verilog-meetup.com\/2024\/06\/20\/a-case-study-on-effective-pipeline-design-in-digital-system\/"},{"key":"12_CR28","doi-asserted-by":"crossref","unstructured":"Kahng, A.B., Lienig, J., Markov, I.L., Hu, J.: VLSI Physical Design: from Graph Partitioning to Timing Closure, vol.\u00a0312. Springer (2011)","DOI":"10.1007\/978-90-481-9591-6"},{"key":"12_CR29","doi-asserted-by":"publisher","unstructured":"Karimi, P., et al.: Towards safer heuristics with XPlain. In: Proceedings of the 23rd ACM Workshop on Hot Topics in Networks, pp. 68\u201376. HotNets \u201924, Association for Computing Machinery, New York, NY, USA (2024). https:\/\/doi.org\/10.1145\/3696348.3696884","DOI":"10.1145\/3696348.3696884"},{"key":"12_CR30","doi-asserted-by":"publisher","unstructured":"Kern, C., Greenstreet, M.R.: Formal verification in hardware design: a survey. ACM Trans. Des. Autom. Electron. Syst. 4(2), 123\u2013193 (1999). https:\/\/doi.org\/10.1145\/307988.307989","DOI":"10.1145\/307988.307989"},{"key":"12_CR31","doi-asserted-by":"publisher","unstructured":"Konnov, I., Kukovec, J., Tran, T.H.: TLA+ model checking made symbolic. Proc. ACM Program. Lang. 3(OOPSLA) (2019). https:\/\/doi.org\/10.1145\/3360549","DOI":"10.1145\/3360549"},{"issue":"5","key":"12_CR32","doi-asserted-by":"publisher","first-page":"773","DOI":"10.1109\/5.381846","volume":"83","author":"E Lee","year":"1995","unstructured":"Lee, E., Parks, T.: Dataflow process networks. Proc. IEEE 83(5), 773\u2013801 (1995). https:\/\/doi.org\/10.1109\/5.381846","journal-title":"Proc. IEEE"},{"key":"12_CR33","doi-asserted-by":"publisher","unstructured":"Levy, A., Walston, J., Samanta, S., Raina, P., Diamantidis, S.: Fastpase: An ai-driven fast PPA speculation engine for RTL design space optimization. In: 2024 25th International Symposium on Quality Electronic Design (ISQED), pp.\u00a01\u20138 (2024). https:\/\/doi.org\/10.1109\/ISQED60706.2024.10528750","DOI":"10.1109\/ISQED60706.2024.10528750"},{"key":"12_CR34","unstructured":"Li, H.: Mill: A fast, scalable JVM build tool (2018). http:\/\/mill-build.org\/"},{"key":"12_CR35","doi-asserted-by":"publisher","first-page":"280","DOI":"10.1007\/978-3-031-65630-9_15","volume-title":"Computer Aided Verification","author":"Y Li","year":"2024","unstructured":"Li, Y., Parsert, J., Polgreen, E.: Guiding enumerative program synthesis with large language models. In: Gurfinkel, A., Ganesh, V. (eds.) Computer Aided Verification, pp. 280\u2013301. Springer Nature Switzerland, Cham (2024)"},{"key":"12_CR36","doi-asserted-by":"crossref","unstructured":"Makharev, V., Ivanov, V.: Code summarization beyond function level (2025)","DOI":"10.1109\/LLM4Code66737.2025.00024"},{"key":"12_CR37","doi-asserted-by":"publisher","first-page":"461","DOI":"10.1007\/978-3-030-81688-9_22","volume-title":"Computer Aided Verification","author":"M Mann","year":"2021","unstructured":"Mann, M., et al.: Pono: a flexible and extensible SMT-based model checker. In: Silva, A., Leino, K.R.M. (eds.) Computer Aided Verification, pp. 461\u2013474. Springer International Publishing, Cham (2021)"},{"key":"12_CR38","doi-asserted-by":"publisher","unstructured":"Melus, B., Suelzer, J., Hagedon, M., Reano, R.: Investigation of adjoint method inverse design applied to photonic integrated circuit fiber-to-chip edge couplers. In: Schr\u00f6der, H., Chen, R.T. (eds.) Optical Interconnects XXIV, pp.\u00a010. SPIE (2024). https:\/\/doi.org\/10.1117\/12.3001211","DOI":"10.1117\/12.3001211"},{"key":"12_CR39","doi-asserted-by":"publisher","unstructured":"Mendoza, D., Hahn, C., Trippel, C.: Translating natural language to temporal logics with large language models and model checkers. In: 2024 Formal Methods in Computer-Aided Design (FMCAD), pp. 1\u201311 (2024). https:\/\/doi.org\/10.34727\/2024\/isbn.978-3-85448-065-5_17","DOI":"10.34727\/2024\/isbn.978-3-85448-065-5_17"},{"key":"12_CR40","doi-asserted-by":"publisher","unstructured":"Meng, B., et al.: Towards a correct-by-construction design of integrated modular avionics. In: 2023 Formal Methods in Computer-Aided Design (FMCAD), pp. 221\u2013227 (2023). https:\/\/doi.org\/10.34727\/2023\/isbn.978-3-85448-060-0_30","DOI":"10.34727\/2023\/isbn.978-3-85448-060-0_30"},{"key":"12_CR41","unstructured":"Mohsin, A., Janicke, H., Wood, A., Sarker, I.H., Maglaras, L., Janjua, N.: Can we trust large language models\u2019 generated code? a framework for in-context learning, security patterns, and code evaluations across diverse LLMs (2024), http:\/\/arxiv.org\/abs\/2406.12513"},{"key":"12_CR42","doi-asserted-by":"publisher","unstructured":"Mondal, R., Tang, A., Beckett, R., Millstein, T., Varghese, G.: What do LLMs need to synthesize correct router configurations? In: Proceedings of the 22nd ACM Workshop on Hot Topics in Networks. pp. 189\u2013195. HotNets \u201923, Association for Computing Machinery, New York, NY, USA (2023). https:\/\/doi.org\/10.1145\/3626111.3628194","DOI":"10.1145\/3626111.3628194"},{"key":"12_CR43","doi-asserted-by":"crossref","unstructured":"de\u00a0Moura, L., Bj\u00f8rner, N.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, pp. 337\u2013340. Springer Berlin Heidelberg, Berlin, Heidelberg (2008). http:\/\/algos.inesc.pt\/projects\/nanotime\/ref12.pdf","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"12_CR44","doi-asserted-by":"publisher","unstructured":"Nelson, T., et al.: Forge: a tool and language for teaching formal methods. Proc. ACM Program. Lang. 8(OOPSLA1) (2024). https:\/\/doi.org\/10.1145\/3649833","DOI":"10.1145\/3649833"},{"key":"12_CR45","doi-asserted-by":"publisher","unstructured":"Neumann, A., Kirsten, E., Zafar, M.B., Singh, J.: Position is power: system prompts as a mechanism of bias in LLMs. In: Proceedings of the 2025 ACM Conference on Fairness, Accountability, and Transparency. pp. 573\u2013598. FAccT \u201925, Association for Computing Machinery, New York, NY, USA (2025). https:\/\/doi.org\/10.1145\/3715275.3732038","DOI":"10.1145\/3715275.3732038"},{"key":"12_CR46","doi-asserted-by":"crossref","unstructured":"Niemetz, A., Preiner, M.: Bitwuzla. In: Enea, C., Lal, A. (eds.) Computer Aided Verification (CAV), pp. 3\u201317. Springer Nature Switzerland, Cham (2023). http:\/\/cs.stanford.edu\/~preiner\/publications\/2023\/NiemetzP-CAV23.pdf","DOI":"10.1007\/978-3-031-37703-7_1"},{"key":"12_CR47","doi-asserted-by":"crossref","unstructured":"Niemetz, A., Preiner, M., Wolf, C., Biere, A.: Btor2, BtorMC and Boolector 3.0. In: Chockler, H., Weissenbacher, G. (eds.) Computer Aided Verification, pp. 587\u2013595. Springer International Publishing, Cham (2018)","DOI":"10.1007\/978-3-319-96145-3_32"},{"key":"12_CR48","doi-asserted-by":"publisher","unstructured":"Norman, C., Godbole, A., Manerkar, Y.A.: PipeSynth: automated synthesis of microarchitectural axioms for memory consistency. In: Proceedings of the 28th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 3, pp. 513\u2013527. ASPLOS 2023, Association for Computing Machinery, New York, NY, USA (2023). https:\/\/doi.org\/10.1145\/3582016.3582056","DOI":"10.1145\/3582016.3582056"},{"key":"12_CR49","doi-asserted-by":"publisher","unstructured":"Parker, J., Vazou, N., Hicks, M.: LWeb: information flow security for multi-tier web applications. Proc. ACM Program. Lang. 3(POPL) (2019). https:\/\/doi.org\/10.1145\/3290388","DOI":"10.1145\/3290388"},{"key":"12_CR50","unstructured":"Patel, A., Reddy, S., Bahdanau, D., Dasigi, P.: Evaluating in-context learning of libraries for code generation (2024). http:\/\/arxiv.org\/abs\/2311.09635"},{"key":"12_CR51","unstructured":"Pei, Z., Zhen, H.L., Yuan, M., Huang, Y., Yu, B.: BetterV: controlled Verilog generation with discriminative guidance. In: Proceedings of the 41st International Conference on Machine Learning, ICML\u201924, JMLR.org (2024)"},{"key":"12_CR52","doi-asserted-by":"publisher","unstructured":"Roy, T., Hsiao, M.: Reachability analysis in RTL circuits using k-induction bounded model checking. In: 2017 IEEE International High Level Design Validation and Test Workshop (HLDVT), pp. 9\u201316 (2017). https:\/\/doi.org\/10.1109\/HLDVT.2017.8167457","DOI":"10.1109\/HLDVT.2017.8167457"},{"key":"12_CR53","unstructured":"Sadigova, P.: SMT-based verification of building management systems. Ph.D. thesis, King\u2019s College London (2022). http:\/\/kclpure.kcl.ac.uk\/ws\/portalfiles\/portal\/270830485\/2024_Sadigova_Parvin_1272461_ethesis.pdf"},{"key":"12_CR54","unstructured":"Schoeberl, M., Andersen, S.T., Rasmussen, K.J.H., Lin, R.: Towards an open-source verification method with Chisel and Scala. In: Proceeding 3rd Workshop Open-Source EDA Technol (WOSET) (2020). http:\/\/woset-workshop.github.io\/PDFs\/2020\/a02.pdf"},{"key":"12_CR55","doi-asserted-by":"publisher","unstructured":"Schubert, M.F., Cheung, A.K.C., Williamson, I.A.D., Spyra, A., Alexander, D.H.: Inverse design of photonic devices with strict foundry fabrication constraints. ACS Photonics 9(7), 2327\u20132336 (2022). https:\/\/doi.org\/10.1021\/acsphotonics.2c00313","DOI":"10.1021\/acsphotonics.2c00313"},{"key":"12_CR56","unstructured":"Srikumar, P.: Fast and wrong: the case for formally specifying hardware with LLMs. In: WACI at ASPLOS (2023). http:\/\/asplos-conference.org\/wp-content\/uploads\/2023\/waci\/6-Fast-and-wrong-priya-srikumarpdf.pdf"},{"key":"12_CR57","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/978-3-031-65112-0_7","volume-title":"AI Verification","author":"C Sun","year":"2024","unstructured":"Sun, C., Sheng, Y., Padon, O., Barrett, C.: Clover: closed-loop verifiable code generation. In: Avni, G., Giacobbe, M., Johnson, T.T., Katz, G., Lukina, A., Narodytska, N., Schilling, C. (eds.) AI Verification, pp. 134\u2013155. Springer Nature Switzerland, Cham (2024)"},{"key":"12_CR58","unstructured":"Sun, W., et al.: Commenting higher-level code unit: full code, reduced code, or hierarchical code summarization (2025)"},{"key":"12_CR59","unstructured":"Synopsys: DesignWare library - datapath and building block IP, http:\/\/www.synopsys.com\/dw\/buildingblock.php"},{"key":"12_CR60","unstructured":"Tang, J., et al.: HiVeGen - hierarchical LLM-based Verilog generation for scalable chip design (2024). http:\/\/arxiv.org\/abs\/2412.05393"},{"key":"12_CR61","unstructured":"Wang, E., Daniel, L., Zohar, Y., Barrett, C.: How I learned to stop worrying and love physical design. In: 2024 Workshop on Languages, Tools, and Techniques for Accelerator Design (LATTE) (2024). http:\/\/capra.cs.cornell.edu\/latte24\/paper\/5.pdf"},{"key":"12_CR62","doi-asserted-by":"publisher","unstructured":"Wang, E., et al.: A methodology for reusable physical design. In: 2020 21st International Symposium on Quality Electronic Design (ISQED), pp. 243\u2013249 (2020). https:\/\/doi.org\/10.1109\/ISQED48828.2020.9136999","DOI":"10.1109\/ISQED48828.2020.9136999"},{"key":"12_CR63","doi-asserted-by":"publisher","unstructured":"Wei, J., et al.: Chain-of-thought prompting elicits reasoning in large language models. In: Proceedings of the 36th International Conference on Neural Information Processing Systems, NIPS \u201922, Curran Associates Inc., Red Hook, NY, USA (2022). https:\/\/doi.org\/10.5555\/3600270.3602070","DOI":"10.5555\/3600270.3602070"},{"key":"12_CR64","doi-asserted-by":"publisher","unstructured":"Weng, J., Liu, S., Dadu, V., Wang, Z., Shah, P., Nowatzki, T.: DSAGEN: synthesizing programmable spatial accelerators. In: 2020 ACM\/IEEE 47th Annual International Symposium on Computer Architecture (ISCA). pp. 268\u2013281 (2020). https:\/\/doi.org\/10.1109\/ISCA45697.2020.00032","DOI":"10.1109\/ISCA45697.2020.00032"},{"key":"12_CR65","unstructured":"Wolf, C., Glaser, J., Kepler, J.: Yosys - a free Verilog synthesis suite. In: Proceedings of the 21st Austrian Workshop on Microelectronics (Austrochip), vol.\u00a097 (2013). http:\/\/yosyshq.net\/yosys\/files\/yosys-austrochip2013.pdf"},{"key":"12_CR66","unstructured":"Xu, K., Qiu, R., Zhao, Z., Zhang, G.L., Schlichtmann, U., Li, B.: LLM-aided efficient hardware design automation. arXiv (2024)"},{"key":"12_CR67","doi-asserted-by":"publisher","unstructured":"Xu, R., Xiao, Y., Luo, J., Liang, Y.: HECTOR: a multi-level intermediate representation for hardware synthesis methodologies. In: Proceedings of the 41st IEEE\/ACM International Conference on Computer-Aided Design. ICCAD \u201922, Association for Computing Machinery, New York, NY, USA (2022). https:\/\/doi.org\/10.1145\/3508352.3549370","DOI":"10.1145\/3508352.3549370"},{"key":"12_CR68","unstructured":"Zhang, R., et al.: QiMeng: fully automated hardware and software design for processor chip (2025). http:\/\/arxiv.org\/abs\/2506.05007"},{"key":"12_CR69","unstructured":"Zheng, K., Han, J.M., Polu, S.: MiniF2F: a cross-system benchmark for formal olympiad-level mathematics. arXiv preprint arXiv:2109.00110 (2021). http:\/\/openreview.net\/pdf?id=9ZPegFuFTFv"},{"key":"12_CR70","unstructured":"Zhong, R., et al.: LLM4EDA: emerging progress in large language models for electronic design automation (2023)"}],"container-title":["Lecture Notes in Computer Science","NASA Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-28079-4_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,6,11]],"date-time":"2026-06-11T15:33:53Z","timestamp":1781192033000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-28079-4_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032280787","9783032280794"],"references-count":70,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-28079-4_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026]]},"assertion":[{"value":"12 June 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"NFM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"NASA Formal Methods Symposium","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Los Angeles, CA","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"USA","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2026","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"5 May 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 May 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"nfm2026","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/nfm2026.github.io\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}