Using LLMs to Facilitate Formal Verification of RTL

• URL: http://arxiv.org/abs/2309.09437v2
• Date: Thu, 28 Sep 2023 15:27:39 GMT
• Title: Using LLMs to Facilitate Formal Verification of RTL
• Abstract summary: We show that GPT4 can generate correct SVA even for flawed RTL, without mirroring design errors. We extend the open-source AutoSVA framework by integrating our improved GPT4-based flow to generate safety properties.
• Score: 7.45362896000302
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Formal property verification (FPV) has existed for decades and has been shown to be effective at finding intricate RTL bugs. However, formal properties, such as those written as SystemVerilog Assertions (SVA), are time-consuming and error-prone to write, even for experienced users. Prior work has attempted to lighten this burden by raising the abstraction level so that SVA is generated from high-level specifications. However, this does not eliminate the manual effort of reasoning and writing about the detailed hardware behavior. Motivated by the increased need for FPV in the era of heterogeneous hardware and the advances in large language models (LLMs), we set out to explore whether LLMs can capture RTL behavior and generate correct SVA properties. First, we design an FPV-based evaluation framework that measures the correctness and completeness of SVA. Then, we evaluate GPT4 iteratively to craft the set of syntax and semantic rules needed to prompt it toward creating better SVA. We extend the open-source AutoSVA framework by integrating our improved GPT4-based flow to generate safety properties, in addition to facilitating their existing flow for liveness properties. Lastly, our use cases evaluate (1) the FPV coverage of GPT4-generated SVA on complex open-source RTL and (2) using generated SVA to prompt GPT4 to create RTL from scratch. Through these experiments, we find that GPT4 can generate correct SVA even for flawed RTL, without mirroring design errors. Particularly, it generated SVA that exposed a bug in the RISC-V CVA6 core that eluded the prior work's evaluation.

Related papers

• From Language to Logic: Bridging LLMs & Formal Representations for RTL Assertion Generation [0.0]
  SystemVerilog Assertions (SVA) are essential for formal verification of digital hardware.<n>Recent studies have explored using large language models (LLMs) to automate SVA generation.<n>This paper presents ProofLoop, a tool-augmented ReAct agent that generates SVA from natural-language specifications.
  arXiv  Detail & Related papers  (2026-04-25T01:46:33Z)
• QiMeng-CodeV-SVA: Training Specialized LLMs for Hardware Assertion Generation via RTL-Grounded Bidirectional Data Synthesis [41.09864485551356]
  We propose a data synthesis framework to tackle two challenges: the scarcity of high-quality real-world SVA corpora and the lack of reliable methods to determine NL-SVA semantic equivalence.<n>We train CodeV-SVA, a series of SVA generation models. Notably, CodeV-SVA achieves 75.8% on NL2SVA-Human and 84.0% on NL2SVA-Machine in Func.@1.
  arXiv  Detail & Related papers  (2026-03-15T06:25:09Z)
• Rethinking VLMs for Image Forgery Detection and Localization [55.32700985102152]
  We study how to fully leverage vision-language models (VLMs) to assist the image forgery detection and localization (IFDL) task.<n>Building on these findings, we propose a new IFDL pipeline named IFDL-VLM.<n>The experimental results show that we consistently achieve new state-of-the-art performance in detection, localization, and interpretability.
  arXiv  Detail & Related papers  (2026-03-13T12:21:31Z)
• OPV: Outcome-based Process Verifier for Efficient Long Chain-of-Thought Verification [91.15649744496834]
  We propose the Outcome-based Process Verifier (OPV), which verifies the rationale process of summarized outcomes from long chains of thought.<n>OPV achieves new state-of-the-art results on our held-out OPV-Bench, outperforming much larger open-source models such as Qwen3-Max-Preview with an F1 score of 83.1 compared to 76.3.
  arXiv  Detail & Related papers  (2025-12-11T15:47:38Z)
• VaPR -- Vision-language Preference alignment for Reasoning [43.4847999322297]
  We introduce a hard-negative response generation framework based on LLM-guided response editing.<n>VaPR produces rejected responses with targeted errors, maintaining stylistic and length similarity to the accepted ones.<n>We show that VaPR generalizes to open-source LLMs as editors, with models trained on VaPR-OS achieving 99% of the performance of models trained on name.
  arXiv  Detail & Related papers  (2025-10-02T06:10:43Z)
• Hybrid-NL2SVA: Integrating RAG and Finetuning for LLM-based NL2SVA [18.491764850064616]
  SystemVerilog Assertions (SVAs) are critical for verifying the correctness of hardware designs.<n>Recent advances in large language models (LLMs) offer opportunities to automate this translation.<n>We propose a customized retrieval-augmented generation (RAG) framework and a synthetic fine-tuning dataset.
  arXiv  Detail & Related papers  (2025-06-12T17:52:06Z)
• LaF-GRPO: In-Situ Navigation Instruction Generation for the Visually Impaired via GRPO with LLM-as-Follower Reward [10.432056588923224]
  This study focuses on producing precise, in-situ, step-by-step navigation instructions that are practically usable by visually impaired (VI) users.<n>LLM-as-Follower GRPO generates rewards guiding the Vision-Language Model (VLM) post-training.<n>Experiments on NIG4VI show the effectiveness of LaF-GRPO by quantitative metrics.
  arXiv  Detail & Related papers  (2025-06-04T15:34:33Z)
• QiMeng-CodeV-R1: Reasoning-Enhanced Verilog Generation [51.393569044134445]
  Large language models (LLMs) trained via reinforcement learning with verifiable reward (RLVR) have achieved breakthroughs on tasks with explicit, automatable verification.<n> Extending RLVR to automatically generating hardware description languages (HDLs) like Verilog from natural-language (NL) specifications, however, poses three key challenges.<n>We introduce CodeV-R1, an RLVR framework for training Verilog generation LLMs.
  arXiv  Detail & Related papers  (2025-05-30T03:51:06Z)
• Vad-R1: Towards Video Anomaly Reasoning via Perception-to-Cognition Chain-of-Thought [58.321044666612174]
  Vad-R1 is an end-to-end MLLM-based framework for Video Anomaly Reasoning.<n>We design a Perception-to-Cognition Chain-of-Thought (P2C-CoT) that simulates the human process of recognizing anomalies.<n>We also propose an improved reinforcement learning algorithm AVA-GRPO, which explicitly incentivizes the anomaly reasoning capability of MLLMs.
  arXiv  Detail & Related papers  (2025-05-26T12:05:16Z)
• Optimizing Case-Based Reasoning System for Functional Test Script Generation with Large Language Models [18.24326624696047]
  We propose a case-based reasoning (CBR) system, which maintains and leverages a case bank of test intent descriptions and corresponding test scripts. To improve user experience further, we introduce Re4, an optimization method for the CBR system, comprising reranking-based retrieval finetuning and reinforced reuse finetuning.
  arXiv  Detail & Related papers  (2025-03-26T14:23:59Z)
• FlanEC: Exploring Flan-T5 for Post-ASR Error Correction [25.931773686829796]
  We present an encoder-decoder model leveraging Flan-T5 for post-Automatic Speech Recognition (ASR) Generative Speech Error Correction (GenSEC) We explore its application within the GenSEC framework to enhance ASR outputs by mapping n-best hypotheses into a single output sentence. Specifically, we investigate whether scaling the training data and incorporating diverse datasets can lead to significant improvements in post-ASR error correction.
  arXiv  Detail & Related papers  (2025-01-22T16:06:04Z)
• Automatic High-quality Verilog Assertion Generation through Subtask-Focused Fine-Tuned LLMs and Iterative Prompting [0.0]
  We present a large language model (LLM) -based flow to automatically generate high-quality SystemVerilog Assertions (SVA) We introduce a novel sub-task-focused fine-tuning approach, leading to a remarkable 7.3-fold increase in the number of functionally correct assertions. Experiments demonstrate a 26% increase in the number of assertions free from syntax errors using this approach.
  arXiv  Detail & Related papers  (2024-11-23T03:52:32Z)
• FVEval: Understanding Language Model Capabilities in Formal Verification of Digital Hardware [4.480157114854711]
  We present FVEval, the first comprehensive benchmark for characterizing large language models (LLMs) performance in tasks pertaining to formal verification (FV) The benchmark consists of three sub-tasks that measure LLM capabilities at different levels. We present both collections of expert-written verification collateral and methodologies to scalably generate synthetic examples aligned with FV.
  arXiv  Detail & Related papers  (2024-10-15T21:48:57Z)
• OVLW-DETR: Open-Vocabulary Light-Weighted Detection Transformer [63.141027246418]
  We propose Open-Vocabulary Light-Weighted Detection Transformer (OVLW-DETR), a deployment friendly open-vocabulary detector with strong performance and low latency. We provide an end-to-end training recipe that transferring knowledge from vision-language model (VLM) to object detector with simple alignment. Experimental results demonstrate that the proposed approach is superior over existing real-time open-vocabulary detectors on standard Zero-Shot LVIS benchmark.
  arXiv  Detail & Related papers  (2024-07-15T12:15:27Z)
• RLAIF-V: Open-Source AI Feedback Leads to Super GPT-4V Trustworthiness [102.06442250444618]
  We introduce RLAIF-V, a novel framework that aligns MLLMs in a fully open-source paradigm. RLAIF-V maximally explores open-source MLLMs from two perspectives, including high-quality feedback data generation. Experiments on six benchmarks in both automatic and human evaluation show that RLAIF-V substantially enhances the trustworthiness of models.
  arXiv  Detail & Related papers  (2024-05-27T14:37:01Z)
• Can Feedback Enhance Semantic Grounding in Large Vision-Language Models? [61.899791071654654]
  We investigate whether Vision-Language Models (VLMs) can improve their semantic grounding by "receiving" feedback. We find that if prompted appropriately, VLMs can utilize feedback both in a single step and iteratively. We show grounding accuracy consistently improves using automated feedback across all models in all settings investigated.
  arXiv  Detail & Related papers  (2024-04-09T17:59:04Z)
• Test-Time Model Adaptation with Only Forward Passes [68.11784295706995]
  Test-time adaptation has proven effective in adapting a given trained model to unseen test samples with potential distribution shifts. We propose a test-time Forward-Optimization Adaptation (FOA) method. FOA runs on quantized 8-bit ViT, outperforms gradient-based TENT on full-precision 32-bit ViT, and achieves an up to 24-fold memory reduction on ImageNet-C.
  arXiv  Detail & Related papers  (2024-04-02T05:34:33Z)
• A Critical Evaluation of AI Feedback for Aligning Large Language Models [60.42291111149438]
  We show that simple supervised fine-tuning with GPT-4 as the teacher outperforms existing RLAIF pipelines. More generally, we find that the gains from RLAIF vary substantially across base model families, test-time evaluation protocols, and critic models.
  arXiv  Detail & Related papers  (2024-02-19T18:53:54Z)
• ChIRAAG: ChatGPT Informed Rapid and Automated Assertion Generation [10.503097140635374]
  ChIRAAG, based on OpenAI GPT4, generates System Verilog Assertion (SVA) from natural language specifications of a design. In experiments, only 27% of LLM-generated raw assertions had errors, which was rectified in few iterations. Our results show that LLMs can streamline and assist engineers in the assertion generation process, reshaping verification.
  arXiv  Detail & Related papers  (2024-01-31T12:41:27Z)
• Silkie: Preference Distillation for Large Visual Language Models [56.10697821410489]
  This paper explores preference distillation for large vision language models (LVLMs) We first build a vision-language feedback dataset utilizing AI annotation. We adopt GPT-4V to assess the generated outputs regarding helpfulness, visual faithfulness, and ethical considerations. The resulting model Silkie, achieves 6.9% and 9.5% relative improvement on the MME benchmark regarding the perception and cognition capabilities.
  arXiv  Detail & Related papers  (2023-12-17T09:44:27Z)
• GPT-4V-AD: Exploring Grounding Potential of VQA-oriented GPT-4V for Zero-shot Anomaly Detection [51.43589678946244]
  This paper explores the potential of VQA-oriented GPT-4V in the popular visual Anomaly Detection (AD) task. It is the first to conduct qualitative and quantitative evaluations on the popular MVTec AD and VisA datasets.
  arXiv  Detail & Related papers  (2023-11-05T10:01:18Z)
• LLM4DV: Using Large Language Models for Hardware Test Stimuli Generation [5.905138464855556]
  This paper presents a novel benchmarking framework for eliciting test stimuli from large language models (LLMs) We compare LLM4DV to traditional constrained-random testing (CRT), using three self-designed design-under-test (DUT) modules. Experiments demonstrate that LLM4DV excels in efficiently handling straightforward DUT scenarios, leveraging its ability to employ basic mathematical reasoning and pre-trained knowledge.
  arXiv  Detail & Related papers  (2023-10-06T19:02:04Z)
• AutoWeka4MCPS-AVATAR: Accelerating Automated Machine Learning Pipeline Composition and Optimisation [13.116806430326513]
  We propose a novel method to evaluate the validity of ML pipelines, without their execution, using a surrogate model (AVATAR) The AVATAR generates a knowledge base by automatically learning the capabilities and effects of ML algorithms on datasets' characteristics. Instead of executing the original ML pipeline to evaluate its validity, the AVATAR evaluates its surrogate model constructed by capabilities and effects of the ML pipeline components.
  arXiv  Detail & Related papers  (2020-11-21T14:05:49Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.