The paper surveys how large language models (LLMs) are being used in hardware verification, covering tasks such as assertion generation, testbench creation, bug localization, and formal reasoning. It categorizes the literature by methodology, verification goal, tool interaction, benchmarks, and evaluation metrics, and distinguishes between inference-time techniques (prompting, retrieval, structured reasoning, agentic workflows) and training-time adaptation. The authors highlight that LLMs excel as semantic reasoning, search, and orchestration components within verification workflows, yet emphasize the need for semantic alignment, scalable integration, generalization, and rigorous evaluation to ensure true verification correctness.
By Hao Zheng, Jaime Rafael Imperial, Bardia Nadimi, Xiangfei Kong
NeuroAbs is a neuro‑symbolic framework designed to accelerate property checking in hardware verification by abstracting RTL designs. It employs large language model (LLM) assisted analysis to select signals for abstraction and combines LLM‑based abstraction with an AST‑based symbolic RTL representation to produce sound abstractions verified via SMT solving. When an abstraction is too coarse, NeuroAbs uses counterexample‑guided refinement (CEGAR) to iteratively improve the model, leading to significant efficiency gains across various verification tasks.
By Zhiyuan Yan, Xiaofeng Zhou, Ziyue Zheng, Ziyi Yang, Wenbin Che, Wei Zhang, Yangdi Lyu, Hongce Zhang
arXiv:2607. 28877v1 Announce Type: cross Abstract: Verification consumes the majority of modern chip design effort, yet the formal verification tools that provide mathematical guarantees of correctness remain expensive and restrictively licensed.
By Ha Trung Tran
CovR is an agentic framework that automates testbench generation for hardware verification by combining self-reflection loops with simulation-based feedback to maximize coverage. It builds a large dataset of 16,514 specification–RTL reasoning tuples and uses reinforcement learning with tool-derived rewards to train a student model, achieving high coverage scores on VerilogEval, RTLLM V2.0, and CVDP. When deployed as a plug-in stimulus engine, CovR boosts coverage by nearly 19% and improves mutation detection while uncovering previously undetected failures.
By Manar Abdelatty, Maryam Nouh, Sherief Reda
arXiv:2601.20055v3 Announce Type: replace-cross
Abstract: Despite the syntactic fluency of Large Language Models (LLMs), ensuring their logical correctness in high-stakes domains remains a fundamenta...
By Vikash Singh, Darion Cassel, Nathaniel Weir, Nick Feng, Sam Bayless
SkillForge is a framework that breaks down formal code synthesis into reusable atomic skills, each handling a specific subtask such as specification inference, body synthesis, invariant generation, error diagnosis, or repair. A verification-driven harness coordinates these skills by submitting candidates to the Dafny verifier, diagnosing failures, and routing them deterministically to the appropriate repair skill until correctness is achieved or a budget is reached. On a curated benchmark, SkillForge outperforms state‑of‑the‑art agentic and iterative baselines, requiring fewer tokens and lower latency, with ablation studies showing each skill’s measurable contribution and rapid convergence.
By Yanming Liu, Xinyue Peng, Jiannan Cao, Xinyi Wang, Jinbo Su
arXiv:2608. 02712v1 Announce Type: cross Abstract: Kernel generation for hardware accelerators such as GPUs and NPUs has become a proving ground for large language models (LLMs), and state-of-the-art systems raise correctness through pipelines that couple LLMs with agentic reinforcement learning and evolutionary search.
By Yansong Sun, Shenxiu Wu, Siyuan Chen, Runlin Hou, Junhao Qiu, Junming Cao, Shudi Shao, Zhichao Lu, Qingfu Zhang
The paper introduces a domain‑specific debugging agent for repairing near‑miss accelerator kernels, arguing that debugging is more efficient than regenerating kernels from scratch. It tackles knowledge scarcity, integrity, and cost control through pattern retrieval, anti‑cheat detection, and convergence safeguards. Empirical results show the debug agent achieves a 66.7% Pass@1 rate and uses 92.8% fewer tokens per success compared to traditional regeneration methods.
By Yansong Sun, Shenxiu Wu, Siyuan Chen, Runlin Hou, Junhao Qiu, Junming Cao, Shudi Shao, Zhichao Lu, Qingfu Zhang
arXiv:2606. 08976v1 Announce Type: new Abstract: LLM-based RTL generation and reasoning is a promising direction for hardware design automation.
By Jing Wang, Shang Liu, Wenji Fang, Yuchao Wu, Yugao Zhu, Zhiyao Xie
ProofEvolve is a neuro‑symbolic framework that evolves formally verified symbolic proof structures alongside neural models to expand the knowledge boundary in automated theorem proving. The neural component proposes variation operators such as decompositions, repairs, and schema recombinations, while the Lean kernel verifies every proof transition, ensuring formal soundness. Across three competition‑level Lean benchmarks, ProofEvolve achieves the highest average solve rate among evaluated proof systems.
By Wenqian Ye, Ziwei Guan, Eric Xie, Bohan Liu, Shivani Modi, Buyun Zhang, Ellie Dingqiao Wen, Henry Kautz, Aidong Zhang
FormalEvolve is a neuro‑symbolic evolutionary search framework that treats autoformalization as a budgeted test‑time search problem. It builds a compilation‑feasible archive of formal statements and expands it using LLM‑driven mutation, crossover, bounded patch repair, and symbolic AST rewrites to generate diverse, semantically accepted formalizations. In experiments on CombiBench and ProofNet, FormalEvolve achieves higher SH@100 scores and improves theorem‑complete proving under fixed prover budgets compared to no‑archive baselines.
By Haijian Lu, Wei Wang, Jing Liu
arXiv:2607. 26181v1 Announce Type: new Abstract: Functional verification dominates integrated circuit (IC) front-end engineering effort, and a single missed bug that escapes to silicon can trigger a costly respin.
By Xin Xin, Jincheng Lou, Junhui Li, Jinglin Yan, Panda Xiao, Di Wu, Haixiao Li, Weicong Lu, Weijian Fan, Xinyu Qu, Yuxiang Zhao, Min Yu, Zhixiong Di, Yibo Lin