Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Insights from Rights and Wrongs: A Large Language Model for Solving Assertion Failures in RTL Design

Jie Zhou, Youshu Ji, Ning Wang, Yuchen Hu, Xinyao Jiao, Bingkun Yao, Xinwei Fang, Shuai Zhao, Nan Guan, Zhe Jiang

TL;DR

The paper tackles automatic solving of assertion failures in RTL design by introducing AssertSolver, an open-source LLM fine-tuned for SVAs. It combines continual Verilog pretraining on the Verilog-PT corpus, supervised fine-tuning on SVA-Bug/Verilog-Bug data, and learning from challenging error cases via Direct Preference Optimisation to improve repair accuracy and reasoning. A new open benchmark, SVA-Eval, enables comprehensive evaluation against SOTA models, with AssertSolver achieving a bug-fixing pass@1 of 88.54% and strong pass@5 performance, significantly outperforming baselines such as o1-preview. The approach, data-augmentation pipeline, and open benchmarks provide a reproducible, domain-specific framework with practical impact for RTL verification and hardware design debugging.

Abstract

SystemVerilog Assertions (SVAs) are essential for verifying Register Transfer Level (RTL) designs, as they can be embedded into key functional paths to detect unintended behaviours. During simulation, assertion failures occur when the design's behaviour deviates from expectations. Solving these failures, i.e., identifying and fixing the issues causing the deviation, requires analysing complex logical and timing relationships between multiple signals. This process heavily relies on human expertise, and there is currently no automatic tool available to assist with it. Here, we present AssertSolver, an open-source Large Language Model (LLM) specifically designed for solving assertion failures. By leveraging synthetic training data and learning from error responses to challenging cases, AssertSolver achieves a bug-fixing pass@1 metric of 88.54% on our testbench, significantly outperforming OpenAI's o1-preview by up to 11.97%. We release our model and testbench for public access to encourage further research: https://github.com/SEU-ACAL/reproduce-AssertSolver-DAC-25.

Insights from Rights and Wrongs: A Large Language Model for Solving Assertion Failures in RTL Design

TL;DR

The paper tackles automatic solving of assertion failures in RTL design by introducing AssertSolver, an open-source LLM fine-tuned for SVAs. It combines continual Verilog pretraining on the Verilog-PT corpus, supervised fine-tuning on SVA-Bug/Verilog-Bug data, and learning from challenging error cases via Direct Preference Optimisation to improve repair accuracy and reasoning. A new open benchmark, SVA-Eval, enables comprehensive evaluation against SOTA models, with AssertSolver achieving a bug-fixing pass@1 of 88.54% and strong pass@5 performance, significantly outperforming baselines such as o1-preview. The approach, data-augmentation pipeline, and open benchmarks provide a reproducible, domain-specific framework with practical impact for RTL verification and hardware design debugging.

Abstract

SystemVerilog Assertions (SVAs) are essential for verifying Register Transfer Level (RTL) designs, as they can be embedded into key functional paths to detect unintended behaviours. During simulation, assertion failures occur when the design's behaviour deviates from expectations. Solving these failures, i.e., identifying and fixing the issues causing the deviation, requires analysing complex logical and timing relationships between multiple signals. This process heavily relies on human expertise, and there is currently no automatic tool available to assist with it. Here, we present AssertSolver, an open-source Large Language Model (LLM) specifically designed for solving assertion failures. By leveraging synthetic training data and learning from error responses to challenging cases, AssertSolver achieves a bug-fixing pass@1 metric of 88.54% on our testbench, significantly outperforming OpenAI's o1-preview by up to 11.97%. We release our model and testbench for public access to encourage further research: https://github.com/SEU-ACAL/reproduce-AssertSolver-DAC-25.

Paper Structure

This paper contains 13 sections, 4 equations, 5 figures, 4 tables.

Table of Contents

  1. Introduction
  2. Data Augmentation
  3. training strategy
  4. Pretraining
  5. Supervised Fine-Tuning (SFT)
  6. Learning from Error Responses to Challenging Cases
  7. Evaluation
  8. Research Questions
  9. Dataset Property
  10. New Open-Source Benchmark and SOTA Counterparts
  11. Evaluation Metrics
  12. Implementation Details
  13. Results and Analysis

Figures (5)

  • Figure 1: The process of solving assertion failures in RTL verification. Engineers analyse the design specification and code signals to identify the root causes of assertion failures and implement fixes.
  • Figure 2: AssertSolver overview: (I) shows the process for augmenting the training data. (II) describes the training strategy, consisting of pretraining (PT), Supervised Fine-Tuning (SFT), and Direct Preference Optimisation (DPO) which is used to guide learning from error responses to challenging cases. In the inference phase (III), AssertSolver locates and fixes the bug based on the specification (Spec), buggy SystemVerilog (SV) code, and logs, while also providing bug location (Bug Loc.) and an explanation (CoT).
  • Figure 3: Histogram of correct answers across 20 responses. (x-axis: c (number of correct solutions in 20 responses))
  • Figure 4: Comprehensive comparison with closed-source LLMs.
  • Figure 5: The performance of STF Model and AssertSolver in various bugs types and code length intervals.