Formal Hardware Verification

Follow this topic Ask about this topic

The field develops methods to prove that hardware designs meet their specifications, find design bugs, and establish equivalence between implementations. Core techniques include bounded model checking, IC3, SMT-based reasoning, abstraction and refinement, and checking SystemVerilog assertions. Current work also uses learned models and LLM-based agents to generate properties, guide searches, close coverage gaps, and repair RTL, with evaluation on suites such as HWMCC and RTL assertion benchmarks. A central challenge is ensuring that generated properties reflect design intent: syntax and tool acceptance alone do not guarantee meaningful proofs, broad coverage, or reliable bug detection.

Latest papers

32 papers3 papers in the last four weeks, down 25% on the four weeks before. 0.0% of all new papers.

Formal-Verification-Guided Bayesian Optimization for Non-Intrusive Last-Mile Coverage Closure
Oct 12, 2026Chengjia Liu, Priyadarsi Mishra, David Kebo Houngninou +3Bayesian Optimization Formal Hardware Verification
Department of Electrical and Computer Engineering, Texas A&M University, College Station, Texas, USA · Department of Computer Science and Engineering, Texas A&M University, College Station, Texas, USA
A Survey on LLM-Integrated Hardware Design Verification
Oct 6, 2026Hao Zheng, Jaime Rafael Imperial, Bardia Nadimi +1LLM Agent Verification Formal Hardware Verification
Bellini College of Cybersecurity, AI, and Computing, University of South Florida Tampa, FL, USA
BEHAVE: Functional Behavior Modeling Enables Self-Improving Agents for Hardware Design and Verification
Sep 28, 2026Yuheng Wu, Berk Gokmen, Sujeeth Jinesh +5Formal Hardware Verification Electronic Design Automation
Stanford University · Workato, Inc.
Automatic Harness Evolution for Hardware Design Verification: Can LLMs Consolidate Gains Across Discovered Harnesses?
Sep 24, 2026Kidus Seyoum, Ajay MitturFormal Hardware Verification Agent Harness Optimization
NVIDIA
EquivSVA: A Formally Verified Dataset of Behavioral Assertions Across Equivalent RTL Implementations
Sep 22, 2026FNU AditiFormal Hardware Verification SystemVerilog Assertion Generation
Trust, but Validate the Instrument: Auditing AI-Generated RTL Verification Plans on Authored Security-Regression Proxies
Sep 17, 2026Hang Xiao, Chuhong Xu, Kainan Zhou +2Formal Hardware Verification LLM Auditing
Fortinet, Inc. Sunnyvale, CA, USA · Sony Corporate of America San Jose, CA, USA · Google LLC Mountain View, CA, USA
Robustness of LLM-Generated SystemVerilog Assertions to Semantics-Preserving RTL Transformations
Sep 4, 2026FNU AditiSystemVerilog Assertion Generation Language Model Robustness
Beyond Flat Netlist: Hierarchical Graph Representation Learning for Scalable Analysis of Sequential Circuits
Aug 28, 2026Jingyi Zhou, Zhengyuan Shi, Jiaying Zhu +2Bounded Model Checking Representation Learning
The Chinese University of Hong Kong, Hong Kong, China · Tsinghua University, Beijing, China
NoTB: Oracle-Free Triage of LLM-Generated RTL via Cross-Model Formal Consensus
Aug 22, 2026Elisavet Lydia Alvanaki, Je Yang, Biruk Seyoum +1LLM Reliability LLM-Based Program Synthesis
Dept. of Computer Science Columbia University New York, USA
AI with Authority, from Application to Silicon
Aug 21, 2026Jason HickeyVerified Code Generation Formal Verification
Karyk
Coverage-Driven RTL Assertion Generation with Formal Exploration and Neuro-Symbolic Refinement
Aug 19, 2026Zhiyuan Yan, Ziyue Zheng, Hongce ZhangFormal Hardware Verification Program Synthesis
The Hong Kong University of Science and Technology (Guangzhou) · The Hong Kong University of Science and Technology
NeuroAbs: A Neuro-Symbolic RTL Abstraction Framework for Property Checking Acceleration
Aug 18, 2026Zhiyuan Yan, Xiaofeng Zhou, Ziyue Zheng +5Formal Hardware Verification Neuro-Symbolic Reasoning
The Hong Kong University of Science and Technology (Guangzhou) · The Hong Kong University of Science and Technology
Open-Source LLM-Driven Formal Verification: A Multi-Agent Pipeline for RTL Repair
Jul 30, 2026Ha Trung TranFormal Hardware Verification Automated Program Repair
Independent Researcher · Seattle, WA, USA
Formally Verified Synthesizable Floating-Point Data Types in ARCH HDL
Jul 26, 2026Shuqing ZhaoFormal Hardware Verification Formal Verification
HierSVA: A Data Synthesis Pipeline, Dataset, and Benchmark for LLM-Driven Hierarchical Hardware Formal Verification
Jun 9, 2026Maohua Nie, Jiang Zhu, Jingqun Zhang +5Formal Hardware Verification LLM Evaluation
University of Washington · Independent Researcher
AssertLLM2: A Comprehensive LLM Benchmark for Assertion Generation from Design Specifications
May 26, 2026Yuchao Wu, Wenji Fang, Jing Wang +3Formal Hardware Verification LLM Evaluation
Hong Kong University of Science and Technology (HKUST)
SpecAlign: A Semantic Alignment Framework for SystemVerilog Assertion Generation
May 24, 2026Jaime Rafael Imperial, Hao ZhengFormal Hardware Verification SystemVerilog Assertion Generation
Bellini College of Cybersecurity, AI, and Computing University of South Florida Tampa, USA
Reward-Weighted On-Policy Distillation with an Open Property-Equivalence Verifier for NL-to-SVA Generation
May 13, 2026Qingyun Zou, Yingze Li, Tianen Liu +2Formal Hardware Verification Formal Verification
National University of Singapore
Formally Verifying Analog Neural Networks Under Process Variations Using Polynomial Zonotopes
May 11, 2026Yasmine Abu-Haeyeh, Tobias Ladner, Matthias Althoff +1Formal Hardware Verification Neural Network Verification
Goethe University Frankfurt, Germany · Technical University of Munich, Germany
Arcane: An Assertion Reduction Framework through Semantic Clustering and MCTS-Guided Rule Exploring
May 11, 2026Hongqin Lyu, Yonghao Wang, Zhiteng Chao +2Formal Hardware Verification Formal Verification
State Key Lab of Processors, Institute of Computing Technology, CAS, Beijing, China · University of Chinese Academy of Sciences, Beijing, China
CktFormalizer: Autoformalization of Natural Language into Circuit Representations
May 8, 2026Jing Xiong, Qi Han, Chenchen Ding +5Formal Hardware Verification Electronic Design Automation
The University of Hong Kong
Knowledge Graphs, the Missing Link in Agentic AI-based Formal Verification
May 7, 2026Vaisakh Naduvodi Viswambharan, Keerthan Kopparam Radhakrishna, Deepak Narayan Gadde +1KG Construction Formal Hardware Verification
Infineon Technologies Dresden AG & Co. KG, Germany · Infineon Technologies Semiconductor India Private Limited, India
Autoformalizing Memory Specifications with Agents
Apr 30, 2026Jan Ole Ernst, Dmitri Michelangelo Saberi, Derek Christ +6Formal Hardware Verification Autoformalization
Normal Computing · Fraunhofer Institute for Experimental Software Engineering (IESE), Kaiserslautern, Germany · University of Würzburg, Germany
A-IC3: Learning-Guided Adaptive Inductive Generalization for Hardware Model Checking
Apr 23, 2026Xiaofeng Zhou, Guangyu Hu, Hongce Zhang +1Formal Hardware Verification Learning-Augmented Algorithms
The Hong Kong University of Science and Technology · The Hong Kong University of Science and Technology (Guangzhou)
ChatSVA: Bridging SVA Generation for Hardware Verification via Task-Specific LLMs
Apr 3, 2026Lik Tung Fu, Jie Zhou, Shaokai Ren +6SystemVerilog Assertion Generation Formal Hardware Verification
National ASIC Center, School of Integrated Circuits, Southeast University, China · National Center of Technology Innovation for Electronic Design Automation, China · Department of Computer Science, City University of Hong Kong, Hong Kong, China
QiMeng-CodeV-SVA: Training Specialized LLMs for Hardware Assertion Generation via RTL-Grounded Bidirectional Data Synthesis
Mar 15, 2026Yutong Wu, Chenrui Cao, Pengwei Jin +6SystemVerilog Assertion Generation Formal Hardware Verification
SKL of Processors, Institute of Computing Technology, CAS Beijing, China · University of Chinese Academy of Sciences Beijing, China · University of Science and Technology of China Hefei, Anhui, China +1
FVRuleLearner: Operator-Level Reasoning Tree (Op-Tree)-Based Rules Learning for Formal Verification
Mar 6, 2026Lily Jiaxin Wan, Chia-Tung Ho, Yunsheng Bai +4Structured Reasoning in Language Models SystemVerilog Assertion Generation
University of Illinois Urbana-Champaign · NVIDIA · University of Maryland, College Park
Saarthi for AGI: Towards Domain-Specific General Intelligence for Formal Verification
Mar 3, 2026Aman Kumar, Deepak Narayan Gadde, Luu Danh Minh +3SystemVerilog Assertion Generation LLM Agent Verification
Infineon Technologies India Private Limited, India · Infineon Technologies Dresden AG & Co. KG, Germany · Infineon Technologies Vietnam Company Ltd., Vietnam
Agentic AI-based Coverage Closure for Formal Verification
Mar 3, 2026Sivaram Pothireddypalli, Ashish Raman, Deepak Narayan Gadde +1Formal Hardware Verification Formal Verification
Infineon Technologies India Private Limited, India · Dr. B R Ambedkar National Institute of Technology Jalandhar, India · Infineon Technologies Dresden AG & Co. KG, Germany
ATLAS: AI-Assisted Threat-to-Assertion Learning for System-on-Chip Security Verification
Mar 1, 2026Ishraq Tashdid, Kimia Tasnia, Alexander Garcia +2Cybersecurity Formal Hardware Verification
Department of Electrical and Computer Engineering, University of Central Florida · Intel Corporation

Oct 12, 2026J/K move · Enter open · S save

Formal-Verification-Guided Bayesian Optimization for Non-Intrusive Last-Mile Coverage Closure

Chengjia Liu, Priyadarsi Mishra, David Kebo Houngninou, Michael Quinn+2

Department of Electrical and Computer Engineering, Texas A&M University, College Station, Texas, USA · Department of Computer Science and Engineering, Texas A&M University, College Station, Texas, USA

Bayesian Optimization Formal Hardware Verification

Open paper AskPDF arXiv

Last-mile functional coverage closure for modern chip designs remains costly because a mature UVM environment exposes many controls while direct hits on the remaining bins are sparse. We present a non-intrusive workflow that closes pre-defined bins in an existing, human-authored functional coverage model; it does not synthesize verification objectives from the design specification. The workflow first uses abstract-syntax-tree (AST) parsing and cone-of-influence (COI) tracing to map each residual target to existing testbench knobs. Under a matched 20-simulation budget, Bayesian optimization (BO) is compared with continued constrained-random verification (CRV) and random search over the same AST/COI-reduced space. Formal reachability then removes only targets supported by complete unreachability proofs, after which retained targets are grouped by formal difficulty and processed by group-specific BO under a second matched 20-simulation budget. Cleanup and grouping never add numerator bins; only simulator coverage artifacts do. On OpenTitan AES, first-pass reduced-space BO reaches 241/271 bins; formal cleanup removes two denominator bins; the integrated post-cleanup stage - difficulty grouping, policy routing, and group-specific BO - adds 20 simulator-confirmed hits, yielding 261/271 raw coverage (96.31%) and 261/269 effective coverage (97.03%). On Entropy Source, first-pass reduced-space BO reaches 2117/2277 bins; formal cleanup removes ten denominator bins; the integrated post-cleanup stage - difficulty grouping, policy routing, and group-specific BO - adds 93 simulator-confirmed hits, yielding 2210/2277 raw coverage (97.06%) and 2210/2267 effective coverage (97.49%). These results characterize the integrated diagnosis-and-search workflow; the present evaluation does not isolate the causal contributions of difficulty classification, policy routing, and post-cleanup BO.