PaperlayerView exact revision on arXiv

Source-linked AI summary

Automated Multi-Line Bug Repair Using Model Checker Aided LLMs: A Case Study on RISC-V Processors

Debleena Das, Chandan Kumar Jha, Muhammad Hassan, Rolf Drechsler, Ansuman Banerjee, Subhra K. Das, Amlan Chakrabarti

arXiv:2610.32597v1cs.ARcs.SE

TL;DR

RAG, Chain-Of-Thought (COT), and agentic frameworks, streamline verification-artifact creation but do not directly address buggy RTL repair. The method uses failing assertions to inform LLM-generated RTL patches and formally checks candidate repairs with a model checker. Up to 98% of single-line RTL bugs and 93% of multi-line bugs were fixed in BRISC-V mutation-testing experiments.

  • Problem

    RAG, Chain-Of-Thought (COT), and agentic frameworks, streamline verification-artifact creation but do not directly address buggy RTL repair.

    Source: §I · p. 1

  • Method

    The method uses failing assertions to inform LLM-generated RTL patches and formally checks candidate repairs with a model checker.

    Source: §I · pp. 1–2

  • Results

    Up to 98% of single-line RTL bugs and 93% of multi-line bugs were fixed in BRISC-V mutation-testing experiments.

    Source: §I · p. 2

  • Takeaways & Limitations

    The BRISC-V experiments demonstrate repair of both single-line and multi-line RTL bugs with assertions and a model checker in the loop.

    Source: §I · p. 2, §V · p. 6

Abstract

from arXiv · show

Functional verification of Register-Transfer Level(RTL) designs has become a critical bottleneck in modern semiconductor development, often consuming the majority of project resources. Debugging, in particular, remains an especially time-consuming task, requiring careful analysis of simulation traces or counterexamples. Recent work has explored applying Large Language Models (LLMs) to RTL debug and repair with great promise. However, the existing approaches typically are for single-line bugs, operate in open-loop, rely heavily on prompts or retrieval, lack scalability, and often produce incorrect fixes. In this paper, we propose a novel automated RTL bug repair methodology that combines LLMs, assertions, and a model checker to provide scalable, trustworthy semantic grounding and formal guarantees. Concretely, the methodology leverages failing assertions to guide the LLM in generating patches for multi-line bugs. Each candidate patch is formally verified using a model checker (JasperGold), ensuring only valid repairs are accepted. We evaluate the efficacy and scalability of our methodology on the BRISC-V RISC-V core using mutation testing, introducing several mutation types, and demonstrate that our methodology can repair up to 98% of single-line RTL bugs and 93% of the multi-line bugs. To the best of our knowledge, this is the first work to show automated, LLM-assisted RTL multi-line bug repair results on a complex RISC-V processor design in a scalable manner.

I. INTRODUCTION

RTL verification is a major resource bottleneck, and debugging requires time-consuming analysis of traces or counterexamples. The paper combines LLMs, assertions, and model checking to repair single- and multi-line RTL bugs, addressing limitations in prior repair approaches.

I. INTRODUCTION

  • Prior LLM-based RTL repair methods focus on single-line bugs, often operate open-loop, and can produce plausible but incorrect fixes.Earlier work also includes assertion generation and retrieval-based repair, but does not directly address RTL repair in some cases.Source: §I · p. 1
  • The proposed approach uses assertions and a model checker in the repair loop to ground LLM patches and provide formal guarantees.The model checker serves as an objective oracle for evaluating candidate fixes.Source: §I · pp. 1–2
  • Up to 98% of single-line RTL bugs and 93% of multi-line bugs were fixed, with patches certified by a model checker.Experiments used mutation testing on BRISC-V and 10 mutation classes.Source: §I · p. 2
  • The evaluation covers 10 mutation classes on BRISC-V, including a new if-else indentation mutation.The experiments compare an initial code-only LLM stage with a stage that also supplies failing assertions.Source: §I · p. 2
  • The method targets bugs that span multiple lines as well as single-line bugs, including bugs anywhere in procedural blocks.The authors report that assertions help the fixing task in their comparative experiments.Source: §I · p. 2

II. MOTIVATING EXAMPLE

A motivating BRISC-V example shows that an LLM given buggy RTL alone can return an incorrect patch, even for a simple single-line mutation. The paper uses assertions and model checking in the loop to address this open-loop limitation.

II. MOTIVATING EXAMPLE

  • The example in BRISC-V’s Cache Coherence Controller inverts an if condition in a finite-state-machine branch, violating the intended behavior.The module implements MESI and has seven snoop-operation states; its 56 assertions pass on the unmutated design.Source: §II · p. 2
  • A verbose code-only prompt failed to identify the correct patch and instead produced a hallucinated fix.The authors note that iterative prompting can be nondeterministic and may require an arbitrary number of iterations.Source: §II · p. 2
  • The example motivates using high-quality assertions and a model checker in the repair loop rather than relying only on LLM prompting.The paper presents the example to illustrate the lack of trustworthy grounding in open-loop methods.Source: §II · p. 2

III. LLM-ASSISTED AUTOMATED BUG REPAIR

The methodology accepts RTL and assertions, assumes the assertions pass on the unmutated design, and organizes repair into assertion checking followed by debugging.

A. Proposed Methodology

  • The approach targets localization and repair of specified bug types, whether they affect one line or multiple lines anywhere in the RTL.Its stated objective uses an RTL design R, assertion set P, and a set of bug types.Source: A. Proposed Methodology · p. 2
  • The workflow has an assertion-status-check phase followed by a debugging phase, with RTL code and assertions as inputs.The high-level workflow is described as two main phases.Source: A. Proposed Methodology · p. 2

1) Phase-1 Assertion Status Check:

The repair workflow first checks mutated RTL against assertions, then uses a two-stage LLM process and checks suggested patches with JasperGold. A BRISC-V case study shows how a failing assertion can help the LLM identify and repair an otherwise unlocalized bug.

1) Phase-1 Assertion Status Check:

  • Mutated code is checked against assertions in JasperGold, where violations can produce counterexamples.The initial design and assertions provide the basis for determining which assertions fail after mutation.Source: 1) Phase-1 Assertion Status Check · pp. 2–3

2) Phase-2: Debugging:

  • Stage 1 asks the LLM to repair buggy code without extra context; Stage 2 adds the failing assertions, and JasperGold checks whether all assertions pass.If assertions still fail after Stage 1, the failed assertions and the full code block are supplied for Stage 2 repair.Source: 2) Phase-2: Debugging · p. 3

B. Case Study: RISC-V Processor

  • In the BRISC-V Snooper case, a failing assertion gave the LLM context to identify and repair a bug without being told its location or mutation type.The example involved an inverted hit condition that broke expectations for r_invalidate and a state transition.Source: B. Case Study: RISC-V Processor · p. 3

IV. EXPERIMENTAL EVALUATION

The section presents the experimental setup, bug insertion process, and results for the proposed methodology.

  • The evaluation section covers experimental setup, bug insertion, and results for the proposed methodology.Source: §IV · p. 3

A. Experimental Setup

The experiments use BRISC-V, JasperGold, and GPT-5.5, with prompts that assign the LLM a role and request code repair or mutation generation.

A. Experimental Setup

  • The evaluation uses BRISC-V modules, JasperGold for formal verification, and GPT-5.5 as the LLM.Assertions used before and after mutation insertion are verified using JasperGold.Source: A. Experimental Setup · p. 3

1) Prompts:

  • The repair prompt assigns the LLM an expert SystemVerilog assertion-verification role and provides code context iteratively through the ChatGPT web interface.The authors note that the interaction could also be automated through API calls.Source: 1) Prompts · pp. 3–4
  • The mutation-generation prompt asks the LLM to produce only one mutation of a specified type in the original design.Source: 1) Prompts · p. 4

2) Assertions:

Assertions guide the repair workflow by exposing failures and providing formal coverage information, but their usefulness depends on assertion quality and coverage.

2) Assertions:

  • Formal coverage indicates how far the assertion suite spans code statements, states, transitions, and faults.Source: 2) Assertions · p. 4
  • Low assertion coverage may prevent failing assertions from helping localize bugs.Source: 2) Assertions · p. 4
  • The authors used manually generated assertions evaluated as high quality with JasperGold after reporting impractical results from two LLM-assisted assertion generators on OpenTitan modules.Source: 2) Assertions · p. 4

3) BRISC-V modules used:

The study evaluates six BRISC-V modules, mostly using always blocks of about 200–300 lines, and describes their cache and bus-control roles.

3) BRISC-V modules used:

  • The evaluation covers six BRISC-V modules and focuses on always blocks, with most selected blocks around 200–300 lines.The authors frame this as a setting where a designer can localize the bug to a small code region or always block without pinpointing the faulty line.Source: 3) BRISC-V modules used · p. 4
  • The L1 bus controller, coherence controller, and snooper coordinate bus access and cache behavior through state-based control.Their descriptions specify 14, 7, and 7 states, respectively.Source: 3) BRISC-V modules used · p. 4
  • The Lxcache controller, Lxbus interface, and cache controller manage L2 or L1 cache functions and communication flows.Their descriptions specify 9, 11, and 15 states, respectively; the Lxcache controller handles MESI-related bits, while the cache controller preserves MESI protocol correctness.Source: 3) BRISC-V modules used · p. 4

B. Bug Insertion

The evaluation inserts syntax-preserving, functionally incorrect mutations into RTL and tests ten mutation classes across BRISC-V modules. Mutations are designed to violate assertions and span sequential and combinational code.

B. Bug Insertion

  • Mutations are syntax-preserving but alter RTL functionality, causing one or more assertions to fail.Each inserted mutation affects a single line and is generated at a random location in a separate LLM session from repair.Source: B. Bug Insertion · p. 4
  • The experiment uses ten mutation classes spanning sequential and combinational code, including an additional class beyond those in prior work.The mutation set is summarized in Table I.Source: B. Bug Insertion · p. 4
  • Tables III–V organize results for cases with two, three, and four mutations, respectively, specifying the mutation types introduced in each case.Each table reports outcomes by repair stage.Source: Table III · p. 5, Table IV · p. 5, Table V · p. 5
  • Table VI covers eight mutation types introduced simultaneously, while Table II reports experiments across BRISC-V modules and identifies absent mutation types.The table legends distinguish repairs in Stage 1, Stage 2, or neither.Source: Table VI · p. 5, Table II · p. 5

C. Results and Findings

The assertion-guided, model-checker-aided workflow repairs up to 98% of the single-line cases and achieves 93% success on large-module multi-line experiments. Small-module combinations of multiple mutation types were repaired with 100% success.

C. Results and Findings

  • A Stage 1 patch for a mutated offset still failed assertions, while supplying the failing assertions in Stage 2 led to the correct offset and passing assertions.The example illustrates how assertion feedback can improve on an initial patch.Source: C. Results and Findings · p. 5
  • The single-line evaluation reports a 98% overall success rate, with only one bug left unrepaired after all stages.Stage 1 patched 28 of 59 cases and Stage 2 patched 29; Cache Controller examples used 4k–4.5k tokens, and JasperGold runtime ranged from 135 ms to 1273 ms.Source: C. Results and Findings · p. 6
  • The experiments reported 100% success in repairing multi-line bugs with different mutation types introduced simultaneously, including experiments using three or four mutation types.Ten different mutation combinations were introduced on one module; all bugs were repaired within Stage 2.Source: C. Results and Findings · p. 6
  • 93% of multi-line cases were repaired when eight mutation types were introduced simultaneously in modules exceeding 300 lines.Across the L1 bus interface and Snooper experiments, all but one mutation was corrected within two stages.Source: C. Results and Findings · p. 6
  • The authors conclude that model-checker guidance can support patching larger designs with multi-line bugs.The experiments include BRISC-V modules with multiple mutations across several classes.Source: C. Results and Findings · p. 6

V. CONCLUSION

The conclusion reports that the method repaired up to 98% of single-line bugs and 93% of multi-line bugs, with fixes formally verified. It also notes that further refinement may identify the few bugs left uncorrected.

V. CONCLUSION

  • Up to 98% of single-line RTL bugs and 93% of multi-line bugs were fixed, with the repairs formally verified.Source: §V · p. 6
  • The proposed two-step, closed-loop method uses assertions and model-checker output to build context for LLM-assisted repair.Source: §V · p. 6
  • The authors describe this as the first attempt at LLM-assisted automated RTL repair of both single-line and multi-line bugs with assertions and a model checker in the loop.Source: §V · p. 6
  • The methodology may be refined further to identify the few bugs it did not correct.Source: §V · p. 6

Related papers

Loading 2610.32597v1…