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