RTL-Repair: Fast Symbolic Repair of Hardware Design Code

Kevin Laeufer, Brandon Fajardo, Abhik Ahuja, Vighnesh Iyer, Borivoje Nikolic and Koushik Sen

Automatically fixing bugs in chip designs was shown to be possible two years earlier by a tool that mutated the code and re-ran the tests, which worked but took up to fourteen hours and produced a wrong answer as often as a right one; this paper (Berkeley) replaces the search with a constraint problem — encode every change a template could make as a switch, assert the failing waveform, and ask a solver which switches to flip — turning hours into a median of 0.7 seconds while producing more correct repairs and far fewer wrong ones.

The argument in one glance

Problem

You get a failing waveform and no way to step through it

Digital circuits are written at the register transfer level, describing how registers update each clock cycle, and most logic bugs show up there. However the design is tested — by eye, by a self-checking testbench, or by a formal tool — the designer ends up holding the same artefact: a trace of signal values over time that ends in a violation. The software habit of stepping through execution does not help, because there is no execution to step through. Everything computes concurrently every cycle, which is why hardware languages describe designs as parallel processes.
What people did

Mutate the code until the tests pass

Automated program repair has a standard recipe: given source code and a failing test, generate candidate edits and keep any that make the test pass. Recent work showed this transfers to hardware descriptions, using a genetic algorithm to mutate the design and score candidates against the expected waveform. That was a real result — it established that the problem is tractable at all — and it defined the templates for what kinds of edit are worth trying.
Why it fell short

Search is slow, and passing the test is not the same as being right

Generating and validating candidates means paying for a simulation run per candidate, and the measurements here put the median correct repair at two and a half minutes and the worst at over fourteen hours. Worse than the wait is the hit rate: across the same benchmarks, that approach produces 11 wrong repairs against 10 correct ones, where a wrong repair is one that satisfies the testbench while breaking something the testbench never looked at. Nobody waits fourteen hours for a coin flip.
This paper's idea

Stop searching and let a solver work it out

This paper (UC Berkeley — Laeufer, Fajardo, Ahuja, Iyer, Nikolic and Sen) keeps the templates and throws away the search. Rather than a template producing one concrete candidate edit, it inserts every edit that template could make at once, each behind a switch variable, and hands the whole thing to a solver together with the failing trace as a constraint. The solver decides which switches to flip and what constants to use, in one query that locates and fixes the bug simultaneously. Add a rule that the fewest switches wins, and the median repair takes 0.7 seconds.

Why this problem is worth solving

The difficulty is specific to the domain and worth stating precisely, because it shapes what a repair tool can assume.

In software, a programmer reasons about a program in execution order, and even though threads break that abstraction, the sequential model is the default. Hardware has no sequential program at all. A register transfer level description says what every register and memory holds after the next clock edge, and all of those updates are computed CONCURRENTLY. The languages reflect this directly, modelling a design as a set of parallel processes, or allowing a signal to be referenced before the line that assigns it. So step-through debugging has nothing to step through. What a designer actually receives, whatever the checking method, is a WAVEFORM — a table of every signal value at every cycle, ending at a violation — and the job is to work backwards from that to a line of code

The way the failing test is used is what separates the two approaches.

The established recipe is GENERATE AND VALIDATE: produce a candidate edit, simulate the design, see if the test passes, repeat. Each candidate costs a simulation, so the cost is the size of the search. The alternative starts from the observation that a circuit can be converted into a TRANSITION SYSTEM — mathematical expressions saying what each register holds next, in terms of what it holds now and its inputs — which is exactly the form used for bounded model checking, where a solver is asked to find inputs that violate a property. This paper turns that around. Instead of asking the solver for inputs, it fixes the inputs and outputs to the values in the failing trace, adds variables representing which edits to apply and what constants they use, and asks the solver to satisfy the trace. Locating the fault and fixing it stop being separate steps

What people did before, and where it broke

Read the waveform and fix it yourself. This is what designers do, using knowledge of the design to trace a violation back to its cause.
But the tools do not help much. Techniques carried over from software debugging assume an execution order that hardware does not have.
Prove the design correct with formal methods. Bounded model checking will find inputs that violate an assertion, which is genuinely powerful.
But it tells you the design is wrong, not what to change. You still end up holding a failing trace and a question about which line produced it.
Generate candidate edits and validate them against the testbench. Recent work showed this works on hardware descriptions for the first time, with templates describing what kinds of edit to try.
But every candidate costs a simulation. Median two and a half minutes for a correct repair, worst case over fourteen hours, with a sixteen-hour timeout reached on a third of benchmarks.
Accept whatever makes the test pass. If the testbench is satisfied, the bug is presumably fixed.
But that is exactly how you get a wrong repair. The same approach yields 11 wrong repairs against 10 correct ones, each passing its test while breaking behaviour the test never exercised.
The gap. The templates describing what kinds of edit help were a real contribution and worth keeping. Enumerating edits one at a time and paying a simulation to score each was not.

How a repair becomes a constraint

From a failing waveform to a minimal source change, in one solver query

Mutate the design and re-simulate to score each candidate

Produce a concrete edit from a template, run the testbench, measure how close the output waveform is to the expected one, and let a genetic algorithm steer the search. This is the prior approach and the source of the repair templates that get reused here.
↓ →
Compile the design into a transition system new

Run the Verilog through an open-source synthesis tool to obtain, for each register, an expression giving its next value in terms of current values and inputs. This is the same representation bounded model checking uses, and it is what makes the design something a solver can reason about.
↓ →
Turn each template into a space of edits rather than one edit new

Instead of picking one condition to invert, insert the possibility of inverting every condition, each guarded by its own switch variable, with free variables standing in for any constants the edit needs. Turning all switches off recovers the original circuit exactly.
↓ →
Assert the failing trace and solve for the switches new

Unroll the instrumented system cycle by cycle as for model checking, but fix inputs and expected outputs to the values recorded in the failing test, and ask the solver for an assignment to the switches and constants that makes the circuit follow the trace. Fault location and repair fall out of the same query.
↓ →
Demand the smallest repair, not just any repair new

First ask whether any solution exists, then constrain the number of switches turned on and raise that bound until the solver succeeds. Fewer edits are both more likely to generalise beyond the one test and far easier for a person to check, which is what the tool is ultimately for.
↓ →
Unroll only a window around the first divergence new

Simulate concretely up to the cycle where the output first goes wrong, then start symbolic reasoning there, since a developer would assume the state a few cycles earlier is fine. Grow the window backwards or forwards depending on how the candidate repairs fail, and cap it before giving up.

Implemented with a Verilog frontend for the templates, an open-source synthesis tool for the transition system, and a repair engine in Rust driving an SMT solver; evaluated on the prior tool benchmarks plus real bugs mined from open-source hardware projects.

The idea

Keep the templates, delete the search. The prior work’s genuine contribution was working out what kinds of edit fix hardware bugs — replacing a constant, inverting or strengthening a condition, adding a missing assignment. This paper takes those categories and changes what a template does with them. Where the earlier tool picks one condition and inverts it, producing a single candidate to go and simulate, the template here inserts the option of inverting every condition in the design at once, each behind its own switch, plus free variables for whatever constants an edit needs. The resulting circuit is not a candidate repair but a description of an entire space of them, and turning all the switches off recovers the original design exactly. Then the failing waveform is asserted as a constraint and a solver is asked which switches to flip. Because the solver reasons over the whole space simultaneously, there is no separate fault-localisation step — where the bug is and what to do about it come out of the same query. Three templates suffice where the search-based tool needed more, and the effect on cost is not incremental: median 0.7 seconds against two and a half minutes, with the worst case falling from over fourteen hours to thirteen seconds. Replacing an enumeration over candidates with a single constraint that describes all of them at once is the same solve-do-not-search move covered elsewhere on this site where a tool stops trying possibilities in sequence and instead hands the whole space to something built to reason about spaces.

The danger is not failing the test, it is passing it wrongly. The motivating example is small enough to see through completely. A counter is missing its reset assignment, and the test resets the circuit and checks the count is zero. The solver returns two valid answers. One adds an assignment in the reset block, which is the real fix. The other adds that same assignment and a second one in the overflow block — and since the test never counts high enough to overflow, that extra statement is dead code as far as this test is concerned, while being a genuine new bug that any test of overflow behaviour would expose. Both answers satisfy the constraint completely. What separates them is size, so the tool asks for a solution with any number of edits, then binds the count and raises it until the solver succeeds, taking the smallest. The justification is two-sided and both halves matter: fewer edits are less likely to have quietly changed behaviour the test does not cover, and a smaller diff is one a human might actually verify, which is the whole point of a suggestion tool. In practice one or two edits suffice, with three as the maximum. Treating minimality as a proxy for generalisation, because the specification you have is only a sample of the behaviour you want, is the same beware-of-fitting-the-test discipline covered elsewhere on this site where the risk in an automatically derived answer is that it satisfies the evidence without capturing the intent.

Copy how a person debugs, and it turns out to be a scalability technique. Unrolling a circuit once per test cycle is what makes this kind of analysis expensive, and some of these testbenches run to hundreds of thousands of steps. The observation that fixes it is behavioural rather than mathematical: a developer investigating a failure looks at signals around the cycle where the violation appeared, and works on the assumption that the state a few cycles earlier was still correct. So the tool simulates concretely up to the first divergence, then starts reasoning symbolically from that concrete state, initially considering no surrounding cycles at all. What makes it adaptive is how it grows the window, which depends on how the candidate repairs fail. If every candidate still fails at or before the original failure, something earlier in the state must be wrong, so the window extends backwards. If a candidate fixes the original failure and causes a later one, the window was missing future context, so it extends forwards to include it. One benchmark went from timing out after an hour to finishing in under ten seconds. The paper then formalises when this is safe as a metric over the gap between when internal state first diverges and when that becomes visible at the output. Turning an informal debugging heuristic into a bounded, adaptive search strategy is the same trust-the-locality-of-causes reasoning covered elsewhere on this site where a diagnosis starts near the symptom and expands only when the evidence says it must.

Fixing a counter that forgot to reset

Following the paper worked example from failing waveform to minimal patch

The example is a small counter circuit, the same one used by the prior tool; timings and results are from the full evaluation.

Step 1 of 5

The test fails and you get a table of signals

A counter is supposed to go to zero when reset, but its reset branch only clears the overflow flag and never touches the count. The failing test is expressed as a table with one row per cycle and one column per input and expected output, where an entry can be marked as unconstrained if the testbench does not care about it at that moment.

that table can come from recording a testbench, from writing it by hand, or from a formal tool that discovered the violation
this is the same input the prior search-based tool consumes, which is deliberate so the two are directly comparable

Why it works

A template inserts every edit it could make rather than one → the solver reasons over the whole space at once → so locating the fault and choosing the fix become a single query instead of two phases.
The failing trace is asserted as a constraint rather than replayed by simulation → cost is one solver call instead of one simulation per candidate → collapsing a median of two and a half minutes to 0.7 seconds.
Two different edits can satisfy the same test while differing on untested behaviour → minimising the number of edits prefers the one that changed less → which both generalises better and produces a diff a human can check.
Reasoning cost scales with how many cycles are unrolled → starting from the concrete state at the first divergence and expanding only as failures demand → taking one benchmark from an hour-long timeout to under ten seconds.
Templates operate on the source syntax tree rather than the compiled transition system → the chosen edits map directly back to lines of Verilog → so the output is a readable patch rather than a modified circuit.

What it costs (trade-offs and scope)

The design has to be synthesizable. The whole method rests on compiling to a transition system, so non-synthesizable code is out of scope, and 8 of 20 real bugs were excluded partly for this and partly for unsupported language features.
Right place is not the same as right fix. On real bugs, 9 of 12 produce repairs that pass the testbench, but only 2 fully match the ground truth while 4 change the correct expression in a way that overfits the test.
Minimality can be the wrong objective. One repair leaves a new assignment unguarded by reset, because adding the guard would cost one more edit and the testbench never demanded it.
The window has a hard cap. Beyond 32 cycles the tool gives up, and one documented case succeeds only with a particular solver because others pick a guard that fails just outside the window.
It still produces wrong repairs. Two of them, and while that is far better than eleven, the output remains a suggestion for a human rather than something to apply blindly.

The evaluation

The comparison runs on the benchmarks the prior tool introduced, plus a set of real bugs mined from commits to open-source hardware projects by other authors — a harder test, since those testbenches were written to demonstrate a bug rather than to evaluate a repair tool. The methodological contribution is a stricter notion of what counts as a correct repair: synthesise the repaired design down to a gate-level netlist and run the original testbench against that, which catches repairs that work in simulation but would silently misbehave in real hardware.

Property	Debug the waveform by hand	Generate and validate candidates	Solve for the repair symbolically
Time to a suggestion
Correct repairs on the benchmarks
How the fault is located
Guard against overfitting
Scaling to long testbenches

On the shared benchmarks the symbolic approach produces 16 correct repairs and 2 wrong ones against 10 correct and 11 wrong for the search-based tool, at a median of 0.70 seconds against 2.53 minutes. On 12 real bugs from open-source projects it produces repairs passing the testbench for 9, of which 2 fully match the ground truth, 1 partially, 4 change the right expression but overfit, and 3 differ substantially. Under gate-level checking, only two of the prior tool multi-edit repairs survive as correct.Underlined values explain themselves when clicked.

Where this stops working

What to keep in mind

The headline numbers come from benchmarks the competing tool created, and the authors handle that carefully — they note their machine ran the prior tool slower than its own paper reported, and raised its timeout from 12 to 16 hours so it could produce everything it had originally claimed, which is the right instinct. The real test is the second set, bugs mined from actual project history by other researchers, and there the picture is more sober. Of 20 available bugs only 12 are usable, the rest excluded for non-synthesizable code, unsupported language features or a missing ground truth. Of those 12, nine yield repairs that pass the testbench, but only two fully match what the developers actually did, one partially, and four modify the correct expression in a way that overfits — the tool is markedly better at finding the right place than the right fix, which the authors say plainly and illustrate with examples. The minimality objective is implicated in that: one documented repair leaves a new assignment unguarded by reset, because guarding it would have cost an extra edit and no test demanded it. Other limits are structural. The design must be synthesizable for any of this to work. The reasoning window is capped at 32 cycles, and one case succeeds only with a particular solver because others choose a guard whose failure lands outside that window. And two repairs are still simply wrong, so this remains a suggestion for a human to evaluate rather than a patch to apply.

Background

When the search was the problem, not the templates

This paper sits in the site’s correctness and hardware clusters and rhymes with several ideas covered elsewhere on this site. It is most directly a successor to the hardware repair page, whose contribution it keeps — the taxonomy of edits that fix circuit bugs — while replacing the mechanism that applied them, and the honest comparison it draws is a good model for how follow-on work should treat what it builds on. Its real-bug evaluation comes from the reconfigurable hardware debugging page, which assembled that corpus from project history, and the two together make a neat argument that bugs collected to study debugging are a harder test than benchmarks built to exercise repair tools. Its central move, giving a solver a compact description of an enormous space rather than walking that space one candidate at a time, is the same reason the e-graph superoptimisation and compiler generation pages abandon sequential rewriting. Its treatment of minimality as a defence against fitting the available evidence rather than the intended behaviour is the same caution the compiler testing and constraint inference pages raise. And its insistence that a repair be checked after synthesis, not merely in simulation, is the same verify-the-artefact-that-ships discipline the software sandboxing page applies to machine code.

If you remember only three things

1. Most logic bugs in a chip design surface as a failing waveform, and debugging one is awkward because hardware has no sequential execution to step through — every register update is computed concurrently, so the languages describe designs as parallel processes and software debugging habits do not transfer. Automated repair was recently shown to work here by mutating the design and re-running the testbench, which established the problem was tractable and produced a useful taxonomy of what kinds of edit fix circuit bugs. But paying a simulation per candidate makes it slow, with a median correct repair at two and a half minutes and a worst case over fourteen hours, and it yields 11 wrong repairs against 10 correct ones.
2. The fix is to keep the edit categories and discard the search. A template stops producing one concrete candidate and instead inserts every edit it could make at once, each behind a switch variable with free variables for any constants, so the instrumented design describes a whole space of repairs and turning all switches off recovers the original. Fixing the inputs and outputs to the failing trace and asking a solver which switches to flip then locates the fault and chooses the fix in a single query. Median repair time falls to 0.70 seconds and the worst case to 13.17 seconds, with 16 correct repairs against 2 wrong.
3. Two things keep it honest. Minimality, because a solver will happily return a repair that satisfies the test while adding dead code that is a genuine bug for any test that goes further — so the tool raises a bound on the number of edits until a solution appears, taking the smallest, which usually means one or two. And an adaptive window, which mimics how a developer assumes the state a few cycles before a failure is still good, starting symbolic reasoning at the first divergence and extending backwards or forwards depending on how candidates fail, taking one benchmark from an hour-long timeout to under ten seconds. On real bugs it is markedly better at finding the right place than the right fix.

Check yourself

Check your understanding

1. The prior tool established that automated repair works on hardware designs, using templates plus a genetic search. Predict what this paper keeps and what it replaces.
2. The solver finds a repair that makes the failing test pass. Predict why the tool does not simply return it.
3. Reasoning symbolically about a circuit costs more the more cycles you unroll, and some testbenches here run to hundreds of thousands of steps. Predict how the paper makes that tractable.
4. The evaluation adds a check the prior work did not perform: synthesising each repaired design to a gate-level netlist and running the original testbench against that. Predict what it is for.

Sources

Kevin Laeufer, Brandon Fajardo, Abhik Ahuja, Vighnesh Iyer, Borivoje Nikolic and Koushik Sen. “RTL-Repair: Fast Symbolic Repair of Hardware Design Code.” ASPLOS 2024, Volume 3, pages 867 to 881. University of California, Berkeley. DOI 10.1145/3620666.3651346.
Full text of the paper was used for this explainer, including the worked counter example in Section 3, the repair algorithm covering static analysis preprocessing, the three repair templates, the basic synthesizer and adaptive windowing in Section 4, the output and state divergence metric in Section 5, and the correctness comparison, gate-level simulation methodology, speed measurements and open-source bug study in Section 6.
The tool and a reproduction artifact were released publicly.