{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,3]],"date-time":"2026-07-03T09:02:38Z","timestamp":1783069358433,"version":"3.54.6"},"reference-count":42,"publisher":"Association for Computing Machinery (ACM)","issue":"6","funder":[{"name":"German Federal Ministry of Education and Research","award":["01IW22002"],"award-info":[{"award-number":["01IW22002"]}]},{"name":"PaSVer","award":["16ME0855"],"award-info":[{"award-number":["16ME0855"]}]},{"name":"SASPIT","award":["16KIS1852K"],"award-info":[{"award-number":["16KIS1852K"]}]},{"name":"ECXLplus","award":["01IW24001"],"award-info":[{"award-number":["01IW24001"]}]},{"name":"Scale4Edge","award":["16ME0127"],"award-info":[{"award-number":["16ME0127"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Des. Autom. Electron. Syst."],"published-print":{"date-parts":[[2025,11,30]]},"abstract":"<jats:p>\n            As technology continues to advance, it becomes increasingly integrated into daily life facilitating complex tasks across a range of environments. While some applications such as smartphones and smartwatches are less critical, others like healthcare devices and autonomous vehicles demand bug-free performance to prevent financial loss or harm. Traditionally, simulation-based testing and formal verification played a major role in ensuring a bug-free device. However, the simulation of bigger systems is limited to a definite number of scenarios on the\n            <jats:italic toggle=\"yes\">Design under Verification<\/jats:italic>\n            \u00a0(DUV). Hence, it is unable to explore all possible inputs that can occur. Formal verification, on the other hand, offers a higher level of assurance through mathematical proofs but is both time-consuming and suffers from scalability issues, especially as designs grow in complexity. Recently,\n            <jats:italic toggle=\"yes\">Large Language Models<\/jats:italic>\n            \u00a0(LLMs) have shown promise in tasks previously limited to human expertise. Their natural language processing capabilities can assist in handling extensive specifications and source code, particularly in debugging hardware descriptions and analyzing security and functionality. The utilization of\n            <jats:italic toggle=\"yes\">Retrieval Augmented Generation<\/jats:italic>\n            \u00a0(RAG) has further enhanced LLMs by incorporating large specification or source code bases, thereby improving their bug-identification and correction capabilities. While recent advancements in LLMs, particularly with RAG, have yielded promising results in bug identification and correction for a small class of hardware bugs, significant gaps remain in their full potential for systematically addressing a wide range of hardware bugs. For instance, existing LLM methodologies struggle to detect bugs involving incorrect constant values, i.e., the use of wrong constants in source code. This limitation underscores the need for further exploration in utilizing LLMs to fully optimize the verification process. To bridge this gap, we propose a 3-phased 4-stage LLM-assisted systematic bug closure methodology that focuses on functional bugs in Verilog HDL rather than structural or syntactic issues. Our approach extracts functional properties of the DUV and systematically breaks down complex expressions into smaller sub-expressions to facilitate bug detection and correction. By employing RAG, the LLM is guided using the functional specifications and source code to identify and correct bugs. If the initial guidance through RAG is insufficient, our methodology initiates an iterative bug closure process. This includes incorporating more extensive information from the specifications, fetching additional lines of code for bug localization, and breaking down complex Verilog HDL expressions. In our comprehensive evaluation, we assess the LLM\u2019s capabilities using 9 different categories of bugs. As benchmarks, we use 5 OpenTitan\n            <jats:italic toggle=\"yes\">Intellectual Property<\/jats:italic>\n            \u00a0(IP) cores to demonstrate the scalability and effectiveness of our bug closure methodology where \u2248 60% of the bugs were corrected. Specifically, we evaluate OpenAI\u2019s GPT-4 in its ability to identify and correct functional bugs in Verilog HDL code.\n          <\/jats:p>","DOI":"10.1145\/3733237","type":"journal-article","created":{"date-parts":[[2025,5,7]],"date-time":"2025-05-07T07:13:45Z","timestamp":1746602025000},"page":"1-28","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":8,"title":["LLM-assisted Bug Identification and Correction for Verilog HDL"],"prefix":"10.1145","volume":"30","author":[{"ORCID":"https:\/\/orcid.org\/0009-0004-7408-8399","authenticated-orcid":false,"given":"Khushboo","family":"Qayyum","sequence":"first","affiliation":[{"name":"Cyber Physical Systems, DFKI","place":["Bremen, Germany"]}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7237-5878","authenticated-orcid":false,"given":"Chandan Kumar","family":"Jha","sequence":"additional","affiliation":[{"name":"FB3, University of Bremen","place":["Bremen, Germany"]}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4000-6207","authenticated-orcid":false,"given":"Sallar","family":"Ahmadi-Pour","sequence":"additional","affiliation":[{"name":"Group of Computer Architecture, University of Bremen Faculty 3 Mathematics and Computer Science","place":["Bremen, Germany"]}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4217-3079","authenticated-orcid":false,"given":"Muhammad","family":"Hassan","sequence":"additional","affiliation":[{"name":"Cyber Physical Systems, DFKI","place":["Bremen, Germany"]},{"name":"Faculty 03 Mathematics and Computer Science, Computer Science, University of Bremen","place":["Bremen, Germany"]}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9872-1740","authenticated-orcid":false,"given":"Rolf","family":"Drechsler","sequence":"additional","affiliation":[{"name":"Computer Science, University of Bremen Faculty 03 Mathematics and Computer Science","place":["Bremen, Germany"]},{"name":"Cyber Physical Systems, DFKI","place":["Bremen, Germany"]}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,10,17]]},"reference":[{"key":"e_1_3_3_2_2","unstructured":"[n. d.]. LangChain. ([n. d.]). Retrieved October 5 2024 from https:\/\/python.langchain.com\/docs\/get_started"},{"key":"e_1_3_3_3_2","doi-asserted-by":"publisher","DOI":"10.1109\/TIFS.2024.3374558"},{"key":"e_1_3_3_4_2","doi-asserted-by":"publisher","DOI":"10.1145\/3503222.3507763"},{"key":"e_1_3_3_5_2","doi-asserted-by":"publisher","unstructured":"Mohammad Akyash and Hadi Mardani Kamali. 2024. Self-HWDebug: Automation of LLM self-instructing for hardware security verification. In 2024 IEEE Computer Society Annual Symposium on VLSI (ISVLSI). IEEE Computer Society Los Alamitos CA USA 391\u2013396. 10.1109\/ISVLSI61997.2024.00077","DOI":"10.1109\/ISVLSI61997.2024.00077"},{"key":"e_1_3_3_6_2","unstructured":"all-MiniLM-L6-v2. 2023. all-MiniLM-L6-v2. (2023). https:\/\/huggingface.co\/sentence-transformers\/all-MiniLM-L6-v2"},{"key":"e_1_3_3_7_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.comnet.2010.05.010"},{"key":"e_1_3_3_8_2","unstructured":"Jitendra Bhandari Johann Knechtel Ramesh Narayanaswamy Siddharth Garg and Ramesh Karri. 2024. LLM-aided testbench generation and bug detection for finite-state machines. arXiv preprint arXiv:2406.17132 (2024)."},{"key":"e_1_3_3_9_2","unstructured":"Jitendra Bhandari Rajat Sadhukhan Prashanth Krishnamurthy Farshad Khorrami and Ramesh Karri. 2024. SENTAUR: Security EnhaNced trojan assessment using LLMs against undesirable revisions. arXiv preprint arXiv:2407.12352 (2024)."},{"issue":"11","key":"e_1_3_3_10_2","doi-asserted-by":"crossref","first-page":"7015","DOI":"10.1109\/TITS.2020.3000797","article-title":"Autonomous vehicle: Security by design","volume":"22","author":"Chattopadhyay Anupam","year":"2020","unstructured":"Anupam Chattopadhyay, Kwok-Yan Lam, and Yaswanth Tavva. 2020. Autonomous vehicle: Security by design. IEEE Transactions on Intelligent Transportation Systems 22, 11 (2020), 7015\u20137029.","journal-title":"IEEE Transactions on Intelligent Transportation Systems"},{"key":"e_1_3_3_11_2","doi-asserted-by":"publisher","DOI":"10.1109\/C-M.1978.218136"},{"key":"e_1_3_3_12_2","unstructured":"DocArray. 2024. DocArray - The data structure for multimodal data. (2024). Retrieved from https:\/\/github.com\/docarray\/docarray"},{"key":"e_1_3_3_13_2","doi-asserted-by":"publisher","DOI":"10.1007\/b105236"},{"key":"e_1_3_3_14_2","volume-title":"Formal Verification of Circuits","author":"Drechsler Rolf","year":"2013","unstructured":"Rolf Drechsler. 2013. Formal Verification of Circuits. Springer Science and Business Media."},{"key":"e_1_3_3_15_2","doi-asserted-by":"publisher","DOI":"10.1137\/S0036144595293959"},{"key":"e_1_3_3_16_2","doi-asserted-by":"crossref","unstructured":"Wenji Fang Mengming Li Min Li Zhiyuan Yan Shang Liu Hongce Zhang and Zhiyao Xie. 2024. Assertllm: Generating and evaluating hardware verification assertions from design specifications via multi-llms. arXiv preprint arXiv:2402.00386 (2024).","DOI":"10.1109\/LAD62341.2024.10691792"},{"key":"e_1_3_3_17_2","first-page":"640","volume-title":"ASP-DAC 2004: Asia and South Pacific Design Automation Conference 2004 (IEEE Cat. No. 04EX753)","author":"Fey G\u00f6rschwin","year":"2004","unstructured":"G\u00f6rschwin Fey and Rolf Drechsler. 2004. Improving simulation-based verification by means of formal methods. In ASP-DAC 2004: Asia and South Pacific Design Automation Conference 2004 (IEEE Cat. No. 04EX753). IEEE, 640\u2013643."},{"issue":"2","key":"e_1_3_3_18_2","doi-asserted-by":"crossref","first-page":"176","DOI":"10.1109\/TC.2010.165","article-title":"Simulation-based verification of floating-point division","volume":"60","author":"Guralnik Elena","year":"2010","unstructured":"Elena Guralnik, Merav Aharoni, Ariel J. Birnbaum, and Anatoly Koyfman. 2010. Simulation-based verification of floating-point division. IEEE Transactions on Computers 60, 2 (2010), 176\u2013188.","journal-title":"IEEE Transactions on Computers"},{"key":"e_1_3_3_19_2","article-title":"LLM-guided formal verification coupled with mutation testing","author":"Hassan Muhammad","year":"2024","unstructured":"Muhammad Hassan, Sallar Ahmadi-Pour, Khushboo Qayyum, Chandan Kumar Jha, and Rolf Drechsler. 2024. LLM-guided formal verification coupled with mutation testing. DATE (2024).","journal-title":"DATE"},{"issue":"5","key":"e_1_3_3_20_2","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/3337791","article-title":"Security modeling of autonomous systems: A survey","volume":"52","author":"Jahan Farha","year":"2019","unstructured":"Farha Jahan, Weiqing Sun, Quamar Niyaz, and Mansoor Alam. 2019. Security modeling of autonomous systems: A survey. ACM Computing Surveys 52, 5 (2019), 1\u201334.","journal-title":"ACM Computing Surveys"},{"key":"e_1_3_3_21_2","doi-asserted-by":"publisher","DOI":"10.1109\/TIFS.2024.3372809"},{"key":"e_1_3_3_22_2","doi-asserted-by":"publisher","unstructured":"Aman Kumar and Deepak Narayan Gadde. 2024. Generative AI augmented induction-based formal verification. 1\u20132. 10.1109\/SOCC62300.2024.10737803","DOI":"10.1109\/SOCC62300.2024.10737803"},{"key":"e_1_3_3_23_2","unstructured":"lowRISC CIC. 2024. OpenTitan: Open source silicon root of trust. (2024). Retrieved September 23 2024 from https:\/\/github.com\/lowRISC\/opentitan"},{"key":"e_1_3_3_24_2","doi-asserted-by":"publisher","unstructured":"Ruiyang Ma Yuxin Yang Ziqian Liu Jiaxi Zhang Min Li Junhua Huang and Guojie Luo. 2024. VerilogReader: LLM-Aided hardware test generation. In 2024 IEEE LLM Aided Design Workshop (LAD). 1\u20135. 10.1109\/LAD62341.2024.10691801","DOI":"10.1109\/LAD62341.2024.10691801"},{"key":"e_1_3_3_25_2","first-page":"1","volume-title":"Proceedings of the 2024 IEEE 8th International Test Conference India","author":"Maddala Karthik","year":"2024","unstructured":"Karthik Maddala, Bhabesh Mali, and Chandan Karfa. 2024. LAAG-RV: LLM assisted assertion generation for RTL design verification. In Proceedings of the 2024 IEEE 8th International Test Conference India. IEEE, 1\u20136."},{"key":"e_1_3_3_26_2","doi-asserted-by":"crossref","first-page":"351","DOI":"10.1109\/ISVLSI.2018.00071","volume-title":"Proceedings of the 2018 IEEE Computer Society Annual Symposium on VLSI.","author":"Mahzoon Alireza","year":"2018","unstructured":"Alireza Mahzoon, Daniel Gro\u00dfe, and Rolf Drechsler. 2018. Combining symbolic computer algebra and boolean satisfiability for automatic debugging and fixing of complex multipliers. In Proceedings of the 2018 IEEE Computer Society Annual Symposium on VLSI.IEEE, 351\u2013356."},{"key":"e_1_3_3_27_2","doi-asserted-by":"publisher","unstructured":"Bhabesh Mali Karthik Maddala Vatsal Gupta Sweeya Reddy Chandan Karfa and Ramesh Karri. 2024. ChIRAAG: ChatGPT informed rapid and automated assertion generation. In 2024 IEEE Computer Society Annual Symposium on VLSI (ISVLSI). 680\u2013683. 10.1109\/ISVLSI61997.2024.00130","DOI":"10.1109\/ISVLSI61997.2024.00130"},{"key":"e_1_3_3_28_2","unstructured":"Kim Martineau AI Explainable and AI Generative. 2023. What is retrieval-augmented generation? https:\/\/research.ibm.com\/blog\/retrieval-augmented-generation-RAG"},{"key":"e_1_3_3_29_2","unstructured":"Xingyu Meng Amisha Srivastava Ayush Arunachalam Avik Ray Pedro Henrique Silva Rafail Psiakis Yiorgos Makris and Kanad Basu. 2023. Unlocking hardware security assurance: The potential of LLMs. arXiv preprint arXiv:2308.11042 (2023)."},{"key":"e_1_3_3_30_2","unstructured":"OpenAI. 2024. OpenAI - flagship models. (2024). Retrieved October 5 2024 from https:\/\/platform.openai.com\/docs\/models"},{"key":"e_1_3_3_31_2","unstructured":"Marcelo Orenes-Vera Margaret Martonosi and DavidWentzlaff. 2023. From RTL to SVA: LLM-assisted generation of Formal Verification Testbenches. arXiv preprint arXiv:2309.09437 (2023)."},{"key":"e_1_3_3_32_2","doi-asserted-by":"publisher","DOI":"10.1145\/3649476.3660393"},{"key":"e_1_3_3_33_2","doi-asserted-by":"publisher","DOI":"10.1109\/SP46215.2023.10179420"},{"key":"e_1_3_3_34_2","doi-asserted-by":"crossref","unstructured":"Vaishnavi Pulavarthi Deeksha Nandal Soham Dan and Debjit Pal. 2024. AssertionBench: A benchmark to evaluate large-language models for assertion generation. arXiv preprint arXiv:2406.18627 (2024).","DOI":"10.18653\/v1\/2025.findings-naacl.449"},{"key":"e_1_3_3_35_2","article-title":"From bugs to fixes: HDL bug identification and patching using LLMs and RAG","author":"Qayyum Khushboo","year":"2024","unstructured":"Khushboo Qayyum, Muhammad Hassan, Sallar Ahmadi-Pour, Chandan Kumar Jha, and Rolf Drechsler. 2024. From bugs to fixes: HDL bug identification and patching using LLMs and RAG. LAD (2024).","journal-title":"LAD"},{"key":"e_1_3_3_36_2","article-title":"Late breaking results: LLM-assisted automated incremental proof generation for hardware verification","author":"Qayyum Khushboo","year":"2024","unstructured":"Khushboo Qayyum, Muhammad Hassan, Sallar Ahmadi-Pour, Chandan Kumar Jha, and Rolf Drechsler. 2024. Late breaking results: LLM-assisted automated incremental proof generation for hardware verification. DAC (2024).","journal-title":"DAC"},{"key":"e_1_3_3_37_2","doi-asserted-by":"publisher","DOI":"10.1145\/3670474.3685956"},{"key":"e_1_3_3_38_2","doi-asserted-by":"crossref","unstructured":"Dipayan Saha Shams Tarek Katayoon Yahyaei Sujan Kumar Saha Jingbo Zhou Mark Tehranipoor and Farimah Farahmandi. 2023. LLM for SoC security: A paradigm shift. arXiv:2310.06046. Retrieved from https:\/\/arxiv.org\/abs\/2310.06046","DOI":"10.1109\/ACCESS.2024.3427369"},{"key":"e_1_3_3_39_2","volume-title":"DAV","author":"Sun Chuyue","year":"2023","unstructured":"Chuyue Sun, Christopher Hahn, and Caroline Trippel. 2023. Towards improving verification productivity with circuit-aware translation of natural language to SystemVerilog assertions. In DAV."},{"key":"e_1_3_3_40_2","doi-asserted-by":"publisher","unstructured":"Yunda Tsai Mingjie Liu and Haoxing Ren. 2024. RTLFixer: Automatically fixing rtl syntax errors with large language model. In Proceedings of the 61st ACM\/IEEE Design Automation Conference (San Francisco CA USA) (DAC\u201924). Association for Computing Machinery New York NY USA Article 53 6 pages. 10.1145\/3649329.3657353","DOI":"10.1145\/3649329.3657353"},{"key":"e_1_3_3_41_2","doi-asserted-by":"publisher","unstructured":"Ke Xu Jialin Sun Yuchen Hu Xinwei Fang Weiwei Shan Xi Wang and Zhe Jiang. 2025. MEIC: Re-thinking RTL debug automation using LLMs. In Proceedings of the 43rd IEEE\/ACM International Conference on Computer-Aided Design (Newark Liberty International Airport Marriott New York NY USA) (ICCAD\u201924). Association for Computing Machinery New York NY USA Article 100 9 pages. 10.1145\/3676536.3676801","DOI":"10.1145\/3676536.3676801"},{"key":"e_1_3_3_42_2","doi-asserted-by":"crossref","unstructured":"Xufeng Yao Haoyang Li Tsz Ho Chan Wenyi Xiao Mingxuan Yuan Yu Huang Lei Chen and Bei Yu. 2024. HDLdebugger: Streamlining HDL debugging with large language models. arXiv:2403.11674. Retrieved from https:\/\/arxiv.org\/abs\/2403.11674","DOI":"10.1145\/3735638"},{"key":"e_1_3_3_43_2","unstructured":"Zixi Zhang Greg Chadwick Hugo McNally Yiren Zhao and Robert Mullins. 2023. LLM4DV: Using large language models for hardware test stimuli generation. arXiv preprint arXiv:2310.04535 (2023)."}],"container-title":["ACM Transactions on Design Automation of Electronic Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3733237","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,17]],"date-time":"2025-10-17T14:02:26Z","timestamp":1760709746000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3733237"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,10,17]]},"references-count":42,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2025,11,30]]}},"alternative-id":["10.1145\/3733237"],"URL":"https:\/\/doi.org\/10.1145\/3733237","relation":{},"ISSN":["1084-4309","1557-7309"],"issn-type":[{"value":"1084-4309","type":"print"},{"value":"1557-7309","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,10,17]]},"assertion":[{"value":"2024-10-05","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-04-10","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-10-17","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}