Paper deep dive
Clover: A Neural-Symbolic Agentic Harness with Stochastic Tree-of-Thoughts for Verified RTL Repair
Zizhang Luo, Yansong Xu, Runlin Guo, Fan Cui, Kexing Zhou, Mile Xia, Hongyuan Hou, Yuhao Luo, Yun Liang
Intelligence
Status: succeeded | Model: Gemma-4-26B-A4B | Prompt: intel-v1 | Confidence: 97%
Last extracted: 4/27/2026, 6:24:25 AM
Summary
Clover is a neural-symbolic agentic harness designed for automated Register-Transfer-Level (RTL) program repair. It addresses the limitations of traditional APR (limited coverage) and LLM-based methods (context corruption and randomness) by orchestrating a structured search over code manipulations. The framework utilizes a main agent that manages specialized sub-agents (Context Agent and Lint-fix Agent) and integrates SMT-based symbolic solvers for low-level repairs. A core innovation is the 'Stochastic Tree-of-Thoughts' mechanism, a test-time scaling strategy that allows the agent to explore a tree of hypotheses, balancing exploration and exploitation to ensure reliable and verified hardware design patches.
Entities (8)
Relation Signals (5)
Main Agent → delegatesto → Context Agent
confidence 100% · Two sub-agents operate under the main agent’s control: a context agent and a lint-fix agent.
Clover → evaluatedon → RTL-repair
confidence 100% · Evaluated on the RTL-repair benchmark, Clover fixes 96.8% of bugs
Main Agent → invokes → SMT Solver
confidence 100% · The chosen template is then formulated as an SMT problem... The agent then synthesizes the final source-level patch
Clover → orchestrates → Main Agent
confidence 100% · The framework orchestrates RTL APR as a structured search over code manipulations... performed by the main agent.
Clover → uses → Stochastic Tree-of-Thoughts
confidence 100% · At its core, Clover introduces stochastic tree-of-thoughts, a test-time scaling mechanism
Cypher Suggestions (0)
No Cypher suggestions yet.
Abstract
Abstract:RTL program repair remains a critical bottleneck in hardware design and verification. Traditional automatic program repair (APR) methods rely on predefined templates and synthesis, limiting their bug coverage. Large language models (LLMs) and coding agents based on them offer flexibility but suffer from randomness and context corruption when handling long RTL code and waveforms. We present Clover, a neural-symbolic agentic harness that orchestrates RTL repair as a structured search over code manipulations to explore a validated solution for the bug. Recognizing that different repair operations favor distinct strategies, Clover dynamically dispatches tasks to specialized LLM agents or symbolic solvers. At its core, Clover introduces stochastic tree-of-thoughts, a test-time scaling mechanism that manages the main agent's context as a search tree, balancing exploration and exploitation for reliable outcomes. An RTL-specific toolbox further empowers agents to interact with the debugging environment. Evaluated on the RTL-repair benchmark, Clover fixes 96.8% of bugs within a fixed time limit, covering 94% and 63% more bugs than both pure traditional and LLM-based baselines, respectively, while achieving an average pass@1 rate of 87.5%, demonstrating high reliability and effectiveness.
Tags
Links
- Source: https://arxiv.org/abs/2604.17288v1
- Canonical: https://arxiv.org/abs/2604.17288v1
Trouble viewing inline? Open PDF directly →
Full Text
47,249 characters extracted from source content.
Expand or collapse full text
Clover: A Neural-Symbolic Agentic Harness with Stochastic Tree-of-Thoughts for Verified RTL Repair Zizhang Luo semiwaker@pku.edu.cn Peking University Beijing, China Yansong Xu yansongxu.mail@gmail.com Peking University Beijing, China Runlin Guo linyu22373@gmail.com Peking University Beijing, China Fan Cui pku_cf@stu.pku.edu.cn Peking University Beijing, China Kexing Zhou zhoukexing@pku.edu.cn Peking University Beijing, China Mile Xia milexia@stu.pku.edu.cn Peking University Beijing, China Hongyuan Hou houhy@stu.pku.edu.cn Peking University Beijing, China Yuhao Luo luoyuhao584@gmail.com Peking University Beijing, China Yun Liang ericlyun@pku.edu.cn Peking University Beijing, China Abstract RTL program repair remains a critical bottleneck in hardware design and verification. Traditional automatic program repair (APR) methods rely on predefined templates and synthesis, limiting their bug coverage. Large language models (LLMs) and coding agents based on them offer flexibility but suffer from randomness and context corruption when handling long RTL code and waveforms. We present Clover, a neural-symbolic agentic harness that orchestrates RTL repair as a structured search over code manipulations to explore a validated solution for the bug. Recognizing that different repair operations favor distinct strategies, Clover dynamically dispatches tasks to specialized LLM agents or symbolic solvers. At its core, Clover intro- duces stochastic tree-of-thoughts, a test-time scaling mecha- nism that manages the main agent’s context as a search tree, balancing exploration and exploitation for reliable outcomes. An RTL-specific toolbox further empowers agents to interact with the debugging environment. Evaluated on the RTL-repair benchmark, Clover fixes 96.8% of bugs within a fixed time limit, covering 94% and 63% more bugs than both pure traditional and LLM-based base- lines, respectively, while achieving an average pass@1 rate of 87.5%, demonstrating high reliability and effectiveness. 1 Introduction Register-transfer-level (RTL) debugging is an indispensable task for hardware design and verification [20]. In a typical manual debug workflow, engineers first craft testbenches to expose bugs, simulate the design to reproduce them [2], analyze waveforms or assertions to pinpoint the root cause LLM -friendly Symbolic -friendly Not for APR Difficulty Design Intention RTL Net-list Waveform Programmer Synthesizer Simulator H-Spec L-Spec per spec literals bool-expr cycle shift coding style add signal dependency adjust submodule algorithm word-expr control flow syntax LLM Symbolic handshake Figure 1: Spectrum of Program Repair Operations [18,19,29], and finally patch the code. For complex systems, this trial-and-error cycle may require many iterations of simulation and manual inspection, making RTL debugging both time-consuming and expensive. Automatic Program Repair (APR)[8, 23] has been proven effective in streamlining debugging for both software and hardware. There are two major ways for RTL-APR. Tradi- tional techniques[5,11,25] typically combine program syn- thesis with symbolic execution to search in a predefined solution space, like AST manipulations. Recently emerged LLM-based methods[4,6–9,16,17,23,26,28] rely on learned statistics of RTL designs and natural language to directly generate patches in token space. As shown in Figure 1, we observed a spectrum of pro- gram repair operations that aligns with different classes of repair techniques, and a fix may be composed of multiple operations, namely multi-step heterogeneity. From top to bottom is the level of abstractions, descending from high- level design intent to low-level implementation detail, while 1 arXiv:2604.17288v1 [cs.AR] 19 Apr 2026 Zizhang Luo, Yansong Xu, Runlin Guo, Fan Cui, Kexing Zhou, Mile Xia, Hongyuan Hou, Yuhao Luo, and Yun Liang the horizontal axis indicates the increasing difficulty of iden- tifying a correct repair operation. The natural design flow proceeds from top to bottom: programmers first capture de- sign intent in RTL, which is subsequently synthesized into netlists and simulated to produce waveforms. High-level operations rooted in design intent or RTL source code are inherently more amenable to LLM-based reasoning, whereas low-level operations involving netlists and dense waveforms are better suited to symbolic methods. Certain defects reside at the extreme high end of the spectrum, e.g., algorithmic errors, and fall beyond the scope of existing APR techniques. No fully automatic method can currently address them with reliable efficiency. This observation raises a central challenge: there is no silver bullet, no universal solution in RTL APR. Spec- ifications, interestingly, are only provided at the two ex- tremes of the abstraction hierarchy, and any given APR tech- nique works with one of them. A low-level specification precisely defines waveform segments via assertions or ref- erence model comparison, while a high-level specification expresses design intent in natural language. Symbolic meth- ods construct a search space from lower-level primi- tives, e.g., fix a Boolean expression by constructing a sum- of-product expression encoding all possible combinations as an SMT formulation[11]. As the abstraction level rises, the search space expands exponentially and quickly becomes intractable, forcing these methods to degrade into less formal search engines guided by hand-crafted heuristics[5]. On the other hand, LLM-based methods draw on higher-level information, such as the natural language specification and RTL source code. Their understanding of design intention and experience learned from prior designs enables them to rapidly resolve issues like coding style violations (e.g., mixing blocking and non-blocking assignments) or syntax errors. Yet low-level information, particularly dense waveform traces, quickly saturates their limited context windows, inducing distraction and promoting hallucination. Most critically, a practical fix often demands a coordinated sequence of diversified repair operations, compounding the overall complexity. Recent developments in LLM agents offer a unique op- portunity to orchestrate LLM-based and symbolic APR ap- proaches within a unified framework, capitalizing on the complementary strengths of both. The LLM agent paradigm enables an LLM to interact with an environment and it- eratively refine its output. Harness engineering[14] has emerged as a systematic approach to constructing scaffold systems that equip agents for domain-specific tasks, inte- grating context engineering[15], guiding prompts, domain- specific skills, and a curated toolbox. In the context of RTL APR, harness engineering addresses how an LLM can effec- tively ingest complex RTL code and waveform data, invoke intricate linters and simulators, and distill overwhelming tool output without corrupting the context. Moreover, a har- ness mitigates a critical concern in hardware verification: the inherent stochasticity of LLM outputs. The statistical nature and sampling-driven generation of LLMs yield unpredictable results, a challenge that can be tempered by validating out- puts within the harness or by employing test-time scaling strategies[12, 13, 21, 27, 30]. In this paper, we introduce Clover, a neural-symbolic agentic harness for verified RTL repair. The framework or- chestrates RTL APR as a structured search over code ma- nipulations to explore a validated solution for the bug, per- formed by the main agent. Recognizing that distinct repair operations demand distinct techniques, the main agent dy- namically delegates specialized subtasks to dedicated sub- agents or to symbolic solvers. We integrate and extend the SMT-based symbolic repair techniques from [11], augment- ing them with additional templates. The symbolic methods can precisely target their corresponding repair operations, thereby shielding the agent from low-level detail. As a com- ponent of the harness, we also introduce an RTL-specific toolbox that streamlines LLM–environment interaction. Fur- thermore, we propose a Stochastic Tree-of-Thoughts test- time-scaling strategy to govern the main agent. This mecha- nism records and samples dialogue states, allowing the agent to backtrack and explore alternative solution paths. Depart- ing from the original Tree-of-Thoughts framework[27], we incorporate a heuristic distribution for expansion selection to balance exploration and exploitation, achieving faster and more reliable repair. Our major contributions are: •Clover harness: We propose an agentic harness to automate RTL program repair with LLM-agents and symbolic approaches. A toolbox is designed to adapt the agent to RTL debugging. • Stochastic Tree of Thoughts test-time-scaling: We propose a searching agentic workflow with a sto- chastic tree-of-thoughts sampling method, turning the LLM’s randomness into reliable search and con- sistently producing valid fixes. •Neural-symbolic Integration: We orchestrate mul- tiple task-specific LLM agent workflows together with SMT-based symbolic repairing to deal with di- versified program repair operations. Evaluated on the RTL-Repair benchmarks [11], experi- ments show that our approach can fix 96.8% of bugs in the RTL-repair dataset within a given time limit, which covers 94% and 63% more bugs than traditional methods and other LLM-based approaches, while achieving an 87.5% pass@1 rate on average, showing a high reliability. 2 Clover: A Neural-Symbolic Agentic Harness with Stochastic Tree-of-Thoughts for Verified RTL Repair Table 1: Comparison between different APR methods Name Fault Localization Patch Generation Fix Capability CirFix[5]nosynthesislimited RTL-Repair[11]nosolvinglimited Strider[25]tracingsynthesislimited [22]statisticsnono Location-is-Key [26] experience experience translation weak RTLFixer[17] analysis experience experience translation trial-and-error weak UVLLM[9] analysis tracing experience experience translation medium Clover (this work) analysis experience experience trial-and-error solving strong 2 Background and Motivation 2.1 RTL Debugging RTL debugging aims to restore correct functionality with minimal code modifications and typically proceeds in three stages: bug discovery, fault localization, and patch generation. Bug discovery identifies a test case that exposes the fault, either through simulation[2] or verification methods[18,19]. Fault localization then narrows the suspect code region[22, 25,26], and patch generation resolves the fault while mini- mizing edits[5, 9, 11, 25]. This paper targets APR, which assumes bugs are known and focuses on the latter two stages. We define correctness by comparing waveforms during simulation, a method that is both comprehensive for LLMs and standard in RTL debug- ging. A setting with minimal human guidance is assumed, as in traditional methods: no design specification in natural language and the LLM observes only the source code and the I/O waveforms of the top module. 2.2 Program Repair Program repair aims to modify a program within a bounded editorial distance such that it passes a given test. Figure 1 summarizes a representative spectrum of common repair operations. Per spec refers to aligning code behavior with a natural language specification. Coding style restructures RTL code to conform to standard conventions (e.g., restrict- ing sensitivity lists toposedge clock). Add signal depen- dency introduces a new dependency to an existing signal. Adjust submodule instantiates or removes submodules. Al- gorithm addresses algorithmic flaws that may require sub- stantial changes to the logic. Syntax corrects RTL syntax errors. Handshake resolves issues on handshaking interfaces. Control flow fixes control constructs such asif-elseor generate for. Cycle shift adjusts signal timing across cy- cles by inserting or removing pipeline registers. Word-expr and bool-expr reshape word-level or bit-level expressions without adding new dependencies. Literals supplies a new constant value for a static signal. 2.3 SMT-based Symbolic Repair RTL-repair [11] introduces a symbolic repair approach that formulates a subset of repair operations as an SMT problem. The hardware design is synthesized into a transition model under bounded model checking, with waveform specifica- tions expressed as assertions on inputs and outputs; repair operations are then encoded as free variables. Due to the inherent complexity, the method relies on predefined tem- plates that target specific repair types. Three templates are proposed: replace literal, add guard, and conditional overwrite, which correspond respectively to the literals, bool-expr, and (partially) word-expr repair categories shown in Figure 1. 2.4 Motivation We summarize existing approaches for fault localization and patch generation, along with their fix capability, in Table 1. Regarding fault localization, [5] and [11] bypass this step entirely. [25] and [9] trace mismatched signals, a technique that, while powerful, is often impractical due to its reliance on internal signal waveforms. [22] adopts spectrum-based fault localization borrowed from software debugging. LLM- based methods, in contrast, leverage learned patterns to infer fault locations, and some [9,17] incorporate static checks from linters [1, 2] for additional guidance. Fix capability is intrinsically tied to the underlying patch generation strategy. We define capability as the probability of producing a valid repair within prescribed time and resource constraints. [5] and [25] employ program synthesis, while [11] reduces the task to SMT solving. In both cases, the fix capability is confined to a set of predefined templates. LLM- based methods eliminate such template restrictions, yet they struggle with low-level hardware details due to limited con- text windows and high computational cost under frequent invocation. Many of these approaches translate specifica- tions to code directly, a paradigm ill-suited for large designs where sufficiently detailed specifications are rarely available. Some efforts [26] explore fine-tuning to improve outcomes. Notably, [9] strengthens its performance by incorporating the signal-tracing strategy of [25]. 3 Zizhang Luo, Yansong Xu, Runlin Guo, Fan Cui, Kexing Zhou, Mile Xia, Hongyuan Hou, Yuhao Luo, and Yun Liang (a) Main agent validation loop patch loop proactive / out-of-patience make hypothesis view code patch view trace get context fix lint update context query call SMT solver (b) Context agent get task view code query def query ref summarize file systemlanguage serversimulatorvcd viewer hypo 1 hypo 2 hypo 3 hypo 4 hypo 5 (d) Hypothesis Tree (c) SMT-based repair Template Selection SMT formulation Patch Writeback literals guards conditions cycles Figure 2: Overview of the Clover Framework Addressing the challenge of multi-step heterogeneity, neither purely symbolic nor purely LLM-based approaches can handle the full spectrum of APR operations alone. A natural resolution is to combine them into a neural-symbolic framework. Given the rigidity of symbolic methods, which either enforce exact compliance with the specification or fail completely, LLMs are best positioned as high-level orches- trators. They can first resolve problems at a more abstract granularity and then delegate the final, low-level adjustments to symbolic techniques. Such a system can be constructed as a harness for the RTL APR agent, exposing symbolic tools and RTL-specific utilities as an environment. By applying test-time scaling to mitigate LLM stochasticity, this design enables reliable, verifiable repair. 3 Overview Figure 2 illustrates the core components of the Clover frame- work. Figure 2(a) depicts the workflow of the main agent, which orchestrates all sub-agents and manages symbolic repair. Two sub-agents operate under the main agent’s con- trol: a context agent and a lint-fix agent. These sub-agents are designed with narrow, task-specific responsibilities to reduce the cognitive load on the main agent and maintain a clean LLM context. The context agent, shown in Figure 2(b), extracts critical code fragments from the extensive RTL code- base. The lint-fix agent follows a similar workflow but targets errors and warnings reported by linters. A detailed discus- sion of these agents as a harness appears in section 4. The SMT-based symbolic repair technique functions as a tool invoked by the main agent when a predefined repair template is deemed applicable. This approach is inspired by RTL-repair [11] and extended with an additional template, adapted for integration with the LLM agent, as outlined in Figure 2(c) and elaborated in section 5. To further enhance reliability, we introduce the Stochastic Tree-of-Thoughts test-time scaling method, which enables the main agent to search over a tree of hypotheses, as shown in Figure 2(d) and detailed in section 6. 4 Multi-Agent Harness 4.1 The main agent As illustrated in Figure 2(a), the main agent orchestrates the overall APR process. Its workflow is structured as a three- level nested loop: an outer loop for hypothesis generation, a middle validation loop for hypothesis verification, and an innermost patch loop for concrete patch formation. The hypothesis-making loop emulates the trial-and-error reasoning of a human programmer. When confronted with a bug, a programmer typically posits a hypothesis regarding the root cause based on observable symptoms, then validates it by applying and testing a patch. Through this iterative cycle, the programmer refines their understanding and may formulate a new hypothesis if the current one proves incor- rect. In our workflow, the agent either proactively proposes a new hypothesis or triggers an out-of-patience mechanism after exceeding a predefined operation budget. This simple mechanism curtails resource expenditure on any single hy- pothesis, encouraging broader exploration of the solution space. The validation loop begins by retrieving relevant code con- text from the context agent. Depending on whether linter errors or warnings are present, the main agent either invokes the lint-fix agent or proceeds directly to the patch loop to synthesize a patch. Once a patch is generated, it is registered with the context agent and submitted to the simulator for verification. In summary, this loop primarily delegates sub- tasks and applies exactly one patch per iteration. Patches are applied cumulatively to enable multi-step repair, such as using LLMs to introduce new signal dependencies before refining a Boolean expression via the SMT solver. 4 Clover: A Neural-Symbolic Agentic Harness with Stochastic Tree-of-Thoughts for Verified RTL Repair The patch loop gathers the necessary information to con- struct a concrete patch. In each iteration, the LLM may per- form one action: it can inspect code snippets or trace files, or query the context agent for additional details. This process continues until the LLM either determines that a direct patch can be emitted or concludes that invoking the SMT solver with a specific repair template is appropriate. 4.2 Multi-agent Interaction The main agent delegates specific subtasks to subordinate agents, thereby maintaining a focused context, accessing specialized tool sets, and executing task-specific workflows. The orchestration involves two sub-agents: a context agent and a lint-fix agent. The context agent is responsible for gathering critical code fragments needed to validate a hypothesis. For each hypothesis proposed by the main agent, a context agent instance is created, maintaining a continuous LLM dialogue across multiple patches in the validation loop. As shown in Figure 2(b), each invocation of the context agent begins with a task from the main agent, performs a series of navigation actions within the RTL codebase, and returns a summarized response. A task may consist of receiving a newly applied patch or answering an explicit query from the main agent. Equipped with a language server, the context agent traces signal dependencies and module hierarchies using query def to locate symbol definitions and query ref to identify all reference sites. The lint-fix agent addresses errors and warnings from the linter, or determines that a given warning should be suppressed. Its workflow is straightforward: gather relevant context and then decide on an appropriate fix or ignore ac- tion. We separate this agent from the main agent because lint resolution, while trivial for LLMs, is ubiquitous during RTL APR. Upon receiving a lint message, the main agent spawns a new lint-fix agent to obtain a patch, thereby insulating the main dialogue from low-level linting details and preserving a clean context. 4.3 RTL-specific Tool Usage As depicted in Figure 2(a) and (b), the agents are provisioned with an RTL-specific toolbox. Basic file reading and editing are performed via the file system. For signal traces (e.g., VCD files), we provide a VCD viewer that returns textual signal traces over a specified time window, with deviations from the golden reference explicitly highlighted and optimizations such as suppressing wide-bit signals. We further simplify environment interaction by allowing the agent to invoke the RTL simulator and retrieve feedback with minimal friction. Additionally, we integrate the slang-server [10] as an RTL language server. Language servers serve as the backend for yzcomb zcombreg xcomb yxcomb zcomb reg y xcomb free variable clk x y z x y z (a) Cycle Shifting (b) SMT formulation Figure 3: Cycle Shifting and Its SMT formulation IDEs such as VS Code, enabling code navigation and linting through parsed program representations. For linting, we primarily rely on Verilator [2], supplemented by a custom linter that flags constructs that are legal under the Verilog specification yet error-prone in practice (e.g., multiply driven signals or partially driven wires). 5 SMT-based Symbolic Repair Our repair module extends RTL-Repair [11] with additional repair templates and integrates them within the LLM agent framework. The process is illustrated in Figure 2(c). Rather than applying all templates in a fixed sequence, the main agent selects a single repair template that best aligns with the inferred bug mechanism. The chosen template is then formulated as an SMT problem: the RTL code is translated into a bounded model checking instance, and repair options are encoded as free variables. After the SMT solver produces a solution, we convert the symbolic outcome into structured repair actions instead of directly modifying the source code. The agent then synthesizes the final source-level patch, en- suring minimal disruption and respect for the original coding style. 5.1 Cycle Shift Templates To address temporal RTL bugs, we introduce an additional template that explicitly models cross-cycle behavior. As shown in Figure 3(a), a signal y can be either a wire or the output of a register, determining whether y changes concurrently with x or is delayed by one cycle. To capture this cycle-shifting behavior in SMT, we introduce a free variable휙that serves as the selection signal for a multiplexer, as depicted in Fig- ure 3(b). The SMT solver then assigns a constant value to휙 such that the output satisfies the bounded model checking assertions. Indiscriminately inserting such multiplexers on all signals is hazardous, as it can introduce combinational loops. In a purely symbolic approach, this template would be infeasible 5 Zizhang Luo, Yansong Xu, Runlin Guo, Fan Cui, Kexing Zhou, Mile Xia, Hongyuan Hou, Yuhao Luo, and Yun Liang because the solver cannot determine the appropriate signals to modify. With the assistance of the main agent, however, the template can be selectively applied to a targeted set of signals identified by the agent. 5.2 Agentic Template Selection and Repair A key enhancement afforded by the agent framework is that template-based repair ceases to be an isolated backend pass and instead becomes a context-aware decision guided by the debugging process. Whereas the original RTL-Repair work- flow attempts its three templates sequentially until one yields a satisfying repair, our approach delegates template selec- tion to the main agent, providing it with detailed instructions regarding the effect and applicability of each template. After SMT solving, Clover further diverges from prior flows in how the repair is materialized. The backend returns a structured repair result rather than directly emitting a patch. This result identifies the selected template and normalizes the synthesized repair into explicit source-level actions, e.g., ex- pression rewrites, guarded insertions, or temporal-structure modifications. The patch-generation agent then interprets these actions under template-specific constraints and emits the final patch while preserving the original control-flow structure, statement ordering, and coding style. For instance, when rewriting the conditions of a signal, the agent may locate a suitableif-elsebranch to apply the modification, avoiding the introduction of an explicit multiplexer tree. Furthermore, compared with the original RTL-Repair im- plementation, Clover extends this agent-mediated template repair flow to System Verilog designs, thereby broadening the applicability of the symbolic repair strategy to a wider range of modern RTL codebases. 6 Stochastic Tree-of-Thoughts 6.1 Hypothesis Tree As shown in Figure 2(d), the hypotheses proposed by the main agent are organized into a tree structure, which sub- stantially enhances the capacity to explore diverse solutions to a given bug. This mechanism is realized by applying our Stochastic Tree-of-Thoughts test-time scaling algorithm to the main agent. Test-time scaling [30] refers to the allocation of additional computational resources during LLM inference to improve output quality. Tree-of-thoughts, a specific test- time scaling technique, structures LLM inferences as a search tree. Within this hypothesis tree, each node can branch into multiple child nodes, corresponding to new hypotheses for- mulated based on observations gathered while validating the parent hypothesis. The original tree-of-thoughts algorithm employs depth-first or breadth-first search combined with beam search, and relies on the LLM itself to evaluate each node, leading to blind exploration over a near-infinite space. In contrast, our approach introduces an auxiliary sampling procedure to dynamically balance the trade-off between ex- ploration and exploitation within the tree, guided by a heuris- tic function that evaluates the promise of each node. 6.2 Heuristic Function and Algorithm Instead of asking LLM to evaluate a node, we provide a heuristic value function for stable outcomes. However, it is hard to precisely determine how far a given node is from the goal, since the location of the target region is unknown. We define a heuristic function푓(푐,ℎ), where푐is the code status andℎis the LLM dialogue history. It estimates the likelihood that the search can succeed from a node(푐,ℎ)based on prior knowledge, as shown by Equation 1. The meaning of symbols is defined in Table 2. This function encourages passing more test benches푡푏 푝 (푐)and getting more information푁 푄 (ℎ) from the design, while avoiding compilation errors푁 퐶퐸 (ℎ), excessive patches푁 푝 (ℎ), and token usage푁 푡표푘 (ℎ). The base value푏adjusts the probability to balance between exploiting good nodes and exploring temporarily worse nodes. These features can be gathered during the validation loop in the main agent. The coefficients휆balance the strength of each factor. As a test-time scaling approach, the coefficients can be changed without the cost of retraining. Furthermore, we choose the state to expand stochastically to balance exploration and exploitation. In each search step, the probability of choosing a state푠= (푐,ℎ)to expand is defined in Equation 2. The algorithm is simple: in each step, a node is sampled from the distribution, then its code status and dialogue history are restored for the main agent. The main agent runs until it proposes a new hypothesis, which is added to the nodes for the next sampling step. 푓(푐,ℎ)= 휆 1 · 푡푏 푝 (푐) 푁 푡푏 + 휆 2 · 푁 푄 (ℎ)− 휆 3 · 푁 퐶퐸 (ℎ) − 휆 4 · 푁 푡표푘 (ℎ)− 휆 5 · 푁 푃 (ℎ)+푏(1) 푃푟[푠=(푐,ℎ)]= 푒 푓(푐,ℎ) Í 푖 푒 푓(푐 푖 ,ℎ 푖 ) (2) 7 Experiments 7.1 Experiment Setup We evaluate using the RTL-repair[11] dataset, which con- tains a variety of buggy RTL designs, widely used in prior works[5,11]. The roots of bugs varied from structural to al- gorithmic. Our results are compared against three baselines. For traditional APR, RTL-repair[11] is the state-of-the-art, which transforms program repair into SMT problems. For LLM-based APR designed for RTL, MEIC[24] and UVLLM[9] are recent works that are open-sourced. In our evaluation, 6 Clover: A Neural-Symbolic Agentic Harness with Stochastic Tree-of-Thoughts for Verified RTL Repair 1234567891011121314151617181920212223242526272829303132 Benchmarks [11] [24] [9] Clover 16 10 19 31 P 0.0 0.2 0.4 0.6 0.8 1.0 pass@1 Benchmarks: 1. decoder_w1 2. decoder_w2 3. counter_k1 4. counter_w1 5.counter_w2 6. flop_w1 7. flop_w2 8. fsm_w1 9. fsm_w2 10.fsm_s1 11.fsm_s2 12.shift_w1 13.shift_w2 14.shift_k1 15.mux_k1 16.mux_w1 17.mux_w2 18.sha3_r1 19.sha3_w1 20.sha3_w2 21.sha3_s1 22.pairing_w1 23.pairing_w2 24.pairing_k1 25.reed_b1 26.reed_o1 27.sdram_w1 28.sdram_w2 29.sdram_k2 30.i2c_w1 31.i2c_w2 32.i2c_k1 Figure 4: Evaluation on Bug Repairing Ability for RTL-repair[11], MEIC[24], UVLLM[9] and Clover. The first 17 benchmarks are easy cases with only one module and one file, and the rest are much more complex. The color implies the pass@1 rate of each case. P: total passed tests. Table 2: Symbols in the heuristic functions NameMeaning 푡푏 푝 (푐)Number of passed testbenches 푁 푡푏 Number of testbenches 푁 푄 (ℎ)Number of queries 푁 퐶퐸 (ℎ)Number of unsolved compile errors 푁 푡표푘 (ℎ)Number of used tokens 푁 푃 (ℎ)Number of patches 푏Base value 휆 푖 Coefficients a case is passed if the waveform matches the golden refer- ence, the same as prior works. Bug discovery or testbench generation is a different research domain. We evaluate our approach with API calls from the Seed2- code model. Only the source code is modifiable to avoid the agent removing the tests. We use Verilator[2] to lint and simulate the designs, and build additional linting on top of Yosys [3] processed net list. The patched code is verified by simulation to ensure correctness on the given testbenches. To estimate the reliability, we use the pass@k metric, which means the probability that the bug is fixed within k independent retries within the given time and re- source limit. We sample pass@k with 10 retries, each with a 30-minute timeout and 2M total token limit. Because to- ken usage can only be checked after the LLM finishes in- ference, the actual time and token usage may be slightly more than the limit. The baselines do not support such a limit, so we adjust the number of rounds and retries for a similar time usage. The coefficients in Equation 1 are 휆 1 = 50,휆 2 = 1,휆 3 = 5,휆 4 = 0.0005,휆 5 = 3,푏= 10. 7.2 Bug Repair Results We first evaluate the ability to reliably fix a bug within the retry, time, and resource limit. As shown in Figure 4, our approach can fix 31 of the bugs, while RTL-repair, MEIC, and UVLLM can only fix 16, 12, and 20 of them, respectively. The first 17 benchmarks are easy cases with only one mod- ule and one file, and the LLM can fix them easily. However, some of the designs have some differences from commonly used textbook designs, e.g., the 3-to-8 decoder has an enable signal that is not useful. This causes the agent to be confused at first, but it can be recovered after validating the agent’s understanding by trial-and-error. The latter 15 benchmarks are much more complex. Their root cause is hidden deep inside the module tree and file structure. Some faults can be found by linters. sha3_r1, pair- ing_k1, and reed_b1 have incorrect width on signals or ex- pressions, which can trigger warnings in Verilator. sha3_w1 has a wire partially undriven, and pairing_w2 mistakenly exchanges the input and output of a module. Though legal in Verilog, these error-prone cases can be detected by our additional linter. Others can benefit from the information collected by interaction: The dead loop in pairing_w1 is an algorithmic error that changes the direction of a loop variable, which is suspicious and can be identified. sha3_w2 miswrites a condition into 0 and changes a wire into a reg- ister. sha3_s1 drops an update condition when the buffer is full. These two cases are rather difficult as they combine multiple repair operations. Our approach still managed to search for a solution. We fail to fix the i2c_k1 case. i2c benchmarks require simulating in-cycle latency and z-value, which is a different category of RTL design, and our tools do not support it well. For RTL-repair, many bugs fall out of its predefined tem- plates. For example, its fix range cannot cover the bug of decoder_w2, fsm_w1, counter_w1, and shift_k1 bench- marks has some wrong "if-else" or "case" structures or wrong sensitivity lists in an "always" block. Though RTL-repair 7 Zizhang Luo, Yansong Xu, Runlin Guo, Fan Cui, Kexing Zhou, Mile Xia, Hongyuan Hou, Yuhao Luo, and Yun Liang Setting 70% 75% 80% 85% pass@1 Setting 0 100 200 avg time(s) Setting 0 100 200 300 avg tokens(k) no ToTno SMTfull Figure 5: Ablation study on different settings on the complex benchmarks (#18-#32 in Figure 4). The average time and tokens exclude failed trials. passes the i2c_k1 case, we found that it manually instructed the repairer to fix the one file where the bug is located to reduce the scale of the SMT problem, which is forbidden in our minimal human guidance setting. MEIC ranks RTL codes with a scorer agent, which further increases the insta- bility. UVLLM localizes fault by Verilator linting and Strider signal tracing, and samples multiple LLM outputs from the same input. This strategy works well in smaller cases, but only linting works in more complex multi-file cases. Besides, UVLLM requires a problem description text as input, but our setting assumes no specification. If a specification is pro- vided, then it can pass the simple cases of counter, but has no improvement in other cases. For the counter cases, signal tracing fails to trace through combinational logics, and patch by experience also fails because the design is uncommon: the "overflow" signal is not related to the "enable" signal. Without specification, the LLM is often hallucinated to over- write the design. Our approach prevents such a hazard by verifying the hypotheses and reviewing the feedback. We found that the original testbench in RTL-repair for the "bug" of reed_o1 has no effect. We keep it unchanged for a fair comparison with RTL-repair. In conclusion, our approach can reliably fix the bugs within the time limit, passing 63% and 94% more bugs than LLM- based[9,24] and traditional methods[11], respectively. RTL- repair has limited fix capability, while MEIC and UVLLM do not address the characteristics of LLM for a reliable outcome. We achieved 87.5% pass@1 rate, showing high reliability. Our average time usage is 413.8 seconds (241.8 if failed cases are excluded), and our average token usage is 294.8k. 7.3 Ablation Study We evaluate the effectiveness of our SMT-based repair mod- ule and the Stochastic Tree-of-Thoughts method. As shown in Figure 5, we compare three configurations: no ToT disables Stochastic Tree-of-Thoughts on the main agent, which then iteratively proposes new hypotheses based solely on the im- mediately preceding one; no SMT prevents the main agent from invoking SMT-based repair, reducing it to a pure LLM Table 3: Evaluation on the Synthetic Benchmarks. BenchmarkErrorResultPass@1 synth_s1Incorrect binary operator✓80% synth_s2Duplicated item in expression✓100% synth_s3Negate if condition✓100% synth_s4Additional minus one✓100% synth_s5Missing item in expression✓100% synth_s6Incorrect reduce operator✓80% synth_s7Delayed by one cycle✓100% synth_s8Advanced by one cycle✓100% agent; and full enables all proposed techniques. Evaluation is conducted on the more challenging benchmarks (#18-#32 in Figure 4), as the baseline capabilities of LLMs readily solve the simpler cases, rendering comparisons uninformative. We report pass@1 rate, average execution time, and average token usage. Failed trials are excluded from the time and to- ken averages because successful runs consume substantially fewer resources than the imposed limits (successful trials average 241 seconds, compared to a 1800-second timeout). As shown in Figure 5, the no ToT, no SMT, and full configu- rations exhibit a consistent increasing trend across all three metrics. no ToT yields the lowest pass@1 rate, underscoring the importance of exploring diverse root-cause hypotheses for complex bugs, as a strictly linear hypothesis chain fre- quently terminates in dead ends. Although expanding the hypothesis tree incurs additional time and token costs, the overhead remains within acceptable bounds. The no SMT configuration also trails full in pass@1 rate, indicating that SMT-based repair contributes to stabilization in specific cases. full consumes more time and tokens due to the overhead of template selection and post-solving patch synthesis by the main agent. The improvement in pass@1 is modest, pri- marily because the selected benchmarks are not sufficiently difficult and the baseline pass rate already exceeds 75%. In summary, the integration of neural-symbolic techniques with Stochastic Tree-of-Thoughts enhances bug-fixing capa- bility at a modest increase in time and token consumption. 7.4 Synthetic Benchmarks Results The RTL-repair benchmarks consist of common hardware modules, which may have open-source implementations and thus could appear in an LLM’s training data. To test general- ization, we design a synthetic benchmark with purely ran- dom logic that carries no semantic meaning or no practical usage. The synthetic module contains randomly wired sig- nals and operators, with simple internal states and logic. We insert a variety of bugs into this synthetic design. The errors 8 Clover: A Neural-Symbolic Agentic Harness with Stochastic Tree-of-Thoughts for Verified RTL Repair and results are shown in Table 3. This ensures these bench- marks did not appear in training data. SMT-based repair is disabled for this experiment. The results show that, even without meaningful semantics, the LLM-based approach can still fix the RTL bugs by analyzing error symptoms, guess- ing likely problematic locations, and deducing the correct code from waveform comparison, demonstrating that our approach can fix bugs in completely new designs. synth_s1 and synth_s6 require the agent to guess the cor- rect operator with very little context—essentially a program synthesis task—resulting in low success rates. synth_s2, synth_s3, synth_s4, and synth_s5 contain combinational logic errors that could be inferred from the waveform trace, showing the agent’s capability for simple logical reasoning. synth_s5 is harder as it requires introducing new depen- dencies and needs more guesses. synth_s7 and synth_s8 need to remove or add a register instance. Thanks to the ADI waveform dumping functionality, the agent could observe in the trace when a signal is delayed or advanced by one cycle, enabling it to repair these two types of bugs. 8 Conclusion RTL APR faces the multi-step heterogeneity challenge, and neither symbolic nor LLM-based APR methods alone can cover all repair operations. We propose Clover, a neural- symbolic agentic harness with stochastic Tree-of-thoughts. By exploring a hypothesis tree while applying both SMT- and LLM-based repairing, Clover reliably fixes 96.8% of bugs and achieves an 87.5% pass@1 rate on average in the RTL-repair benchmarks. References [1] [n. d.]. Icarus Verilog. https://steveicarus.github.io/iverilog/ [2] 2025. Verilator. https://w.veripool.org/verilator [3] 2025. Yosys Open Synthesis Suite. https://yosyshq.net/yosys/ [4] Baleegh Ahmad, Shailja Thakur, Benjamin Tan, Ramesh Karri, and Hammond Pearce. 2024. On Hardware Security Bug Code Fixes by Prompting Large Language Models. IEEE Transactions on Information Forensics and Security 19 (2024), 4043–4057. doi:10.1109/TIFS.2024. 3374558 [5]Hammad Ahmad, Yu Huang, and Westley Weimer. 2022. CirFix: auto- matically repairing defects in hardware design code. In Proceedings of the 27th ACM International Conference on Architectural Support for Programming Languages and Operating Systems. ACM, Lausanne Switzerland, 990–1003. doi:10.1145/3503222.3507763 [6]Fan Cui, Chenyang Yin, Kexing Zhou, Youwei Xiao, and the oth- ers. 2024. OriGen: Enhancing RTL Code Generation with Code-to- Code Augmentation and Self-Reflection. In Proceedings of the 43rd IEEE/ACM International Conference on Computer-Aided Design, ICCAD 2024, Newark Liberty International Airport Marriott, NJ, USA, October 27-31, 2024, Jinjun Xiong and Robert Wille (Eds.). ACM, 99:1–99:9. [7] Abdelrahman Elnaggar. 2025. Investigating Automatic Bug Repair Using Large Language Models for Digital Hardware Design. Ph. D. Dissertation. University of Calgary. [8] Zhiyu Fan, Xiang Gao, Martin Mirchev, Abhik Roychoudhury, and Shin Hwei Tan. 2023. Automated Repair of Programs from Large Language Models. In 2023 IEEE/ACM 45th International Conference on Software Engineering (ICSE). 1469–1481. doi:10.1109/ICSE48619.2023. 00128 [9] Yuchen Hu, Junhao Ye, Ke Xu, Jialin Sun, Shiyue Zhang, Xinyao Jiao, Dingrong Pan, Jie Zhou, Ning Wang, Weiwei Shan, Xinwei Fang, Xi Wang, Nan Guan, and Zhe Jiang. 2024. UVLLM: An Automated Universal RTL Verification Framework using LLMs. doi:10.48550/ arXiv.2411.16238 [10] hudson trading. [n. d.]. slang-server. https://hudson-trading.github. io/slang-server/ [11] Kevin Laeufer, Brandon Fajardo, Abhik Ahuja, Vighnesh Iyer, Borivoje Nikolić, and Koushik Sen. 2024. RTL-Repair: Fast Symbolic Repair of Hardware Design Code. In Proceedings of the 29th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 3. ACM, La Jolla CA USA, 867–881. doi:10. 1145/3620666.3651346 [12]Dacheng Li, Shiyi Cao, Chengkun Cao, Xiuyu Li, Shangyin Tan, Kurt Keutzer, Jiarong Xing, Joseph E. Gonzalez, and Ion Stoica. 2025. S*: Test Time Scaling for Code Generation. arXiv:2502.14382 (2025). doi:10. 48550/arXiv.2502.14382 [13] Qingwen Lin, Boyan Xu, Guimin Hu, Zijian Li, Zhifeng Hao, Keli Zhang, and Ruichu Cai. 2025. CMCTS: A Constrained Monte Carlo Tree Search Framework for Mathematical Reasoning in Large Lan- guage Model. arXiv:2502.11169 (2025). doi:10.48550/arXiv.2502.11169 [14]Ryan Lopopolo. 2026. Harness engineering: leveraging Codex in an agent-first world. https://openai.com/index/harness-engineering/ [15]Lingrui Mei, Jiayu Yao, Yuyao Ge, Yiwei Wang, Baolong Bi, Yujun Cai, Jiazhi Liu, Mingyu Li, Zhong-Zhi Li, Duzhen Zhang, Chenlin Zhou, Jiayi Mao, Tianze Xia, Jiafeng Guo, and Shenghua Liu. 2025. A Survey of Context Engineering for Large Language Models. arXiv:2507.13334 (2025). doi:10.48550/arXiv.2507.13334 [16]Khushboo Qayyum, Muhammad Hassan, Sallar Ahmadi-Pour, Chan- dan Kumar Jha, and Rolf Drechsler. 2024. From Bugs to Fixes: HDL Bug Identification and Patching using LLMs and RAG. In 2024 IEEE LLM Aided Design Workshop (LAD). 1–5. doi:10.1109/LAD62341.2024. 10691874 9 Zizhang Luo, Yansong Xu, Runlin Guo, Fan Cui, Kexing Zhou, Mile Xia, Hongyuan Hou, Yuhao Luo, and Yun Liang [17]Yun-Da Tsai, Mingjie Liu, and Haoxing Ren. 2024. RTLFixer: Au- tomatically Fixing RTL Syntax Errors with Large Language Models. doi:10.48550/arXiv.2311.16543 [18] Shobha Vasudevan, Wenjie Joe Jiang, David Bieber, Rishabh Singh, C Richard Ho, Charles Sutton, et al.2021. Learning semantic represen- tations to verify hardware designs. Advances in Neural Information Processing Systems 34 (2021), 23491–23504. [19]Shobha Vasudevan, David Sheridan, Sanjay Patel, David Tcheng, Bill Tuohy, and Daniel Johnson. 2010. GoldMine: Automatic assertion gen- eration using data mining and static analysis. In 2010 Design, Automa- tion & Test in Europe Conference & Exhibition (DATE 2010). 626–629. doi:10.1109/DATE.2010.5457129 [20]Jayce Wagner. 2018. Intel Could Make Billions Off of Meltdown & Spectre. https://w.digitaltrends.com/computing/intel-could-make- billions-offmeltdown-spectre/3 [21]Xuezhi Wang, Jason Wei, Dale Schuurmans, Quoc Le, Ed Chi, Sha- ran Narang, Aakanksha Chowdhery, and Denny Zhou. 2023. Self- Consistency Improves Chain of Thought Reasoning in Language Mod- els. arXiv:2203.11171 (2023). doi:10.48550/arXiv.2203.11171 [22]Jiang Wu, Zhuo Zhang, Deheng Yang, Xiankai Meng, Jiayu He, Xi- aoguang Mao, and Yan Lei. 2022. Fault Localization for Hardware Design Code with Time-Aware Program Spectrum. In 2022 IEEE 40th International Conference on Computer Design (ICCD). 537–544. doi:10.1109/ICCD56317.2022.00085 [23]Chunqiu Steven Xia, Yuxiang Wei, and Lingming Zhang. 2023. Au- tomated Program Repair in the Era of Large Pre-trained Language Models. In 2023 IEEE/ACM 45th International Conference on Software Engineering (ICSE). 1482–1494. doi:10.1109/ICSE48619.2023.00129 [24]Ke Xu, Jialin Sun, Yuchen Hu, Xinwei Fang, Weiwei Shan, Xi Wang, and Zhe Jiang. 2024. MEIC: Re-thinking RTL Debug Automation using LLMs. In Proceedings of the 43rd IEEE/ACM International Conference on Computer-Aided Design. ACM. doi:10.1145/3676536.3676801 [25]Deheng Yang, Jiayu He, Xiaoguang Mao, Tun Li, Yan Lei, Xin Yi, and Jiang Wu. 2024. Strider: Signal Value Transition-Guided Defect Repair for HDL Programming Assignments. IEEE Transactions on Computer- Aided Design of Integrated Circuits and Systems 43, 5 (2024), 1594–1607. doi:10.1109/TCAD.2023.3341750 [26]Bingkun Yao, Ning Wang, Jie Zhou, Xi Wang, Hong Gao, Zhe Jiang, and Nan Guan. 2024. Location is Key: Leveraging Large Language Model for Functional Bug Localization in Verilog. doi:10.48550/arXiv. 2409.15186 [27]Shunyu Yao, Dian Yu, Jeffrey Zhao, Izhak Shafran, Tom Griffiths, Yuan Cao, and Karthik Narasimhan. 2023. Tree of Thoughts: Deliberate Problem Solving with Large Language Models. In Advances in Neural Information Processing Systems, A. Oh, T. Naumann, A. Globerson, K. Saenko, M. Hardt, and S. Levine (Eds.), Vol. 36. Curran Associates, Inc., 11809–11822. [28] Xufeng Yao, Haoyang Li, Tsz Ho Chan, Wenyi Xiao, Mingxuan Yuan, Yu Huang, Lei Chen, and Bei Yu. 2024. HDLdebugger: Streamlining HDL debugging with Large Language Models. doi:10.48550/arXiv. 2403.11671 [29] Keyi Zhang, Zain Asgar, and Mark Horowitz. 2022. Bringing source- level debugging frameworks to hardware generators. In DAC ’22: 59th ACM/IEEE Design Automation Conference, San Francisco, California, USA, July 10 - 14, 2022, Rob Oshana (Ed.). ACM, 1171–1176. doi:10. 1145/3489517.3530603 [30] Qiyuan Zhang, Fuyuan Lyu, Zexu Sun, Lei Wang, Weixu Zhang, Wenyue Hua, Haolun Wu, Zhihan Guo, Yufei Wang, Niklas Muen- nighoff, Irwin King, Xue Liu, and Chen Ma. 2025. A Survey on Test- Time Scaling in Large Language Models: What, How, Where, and How Well? arXiv:2503.24235 (2025). doi:10.48550/arXiv.2503.24235 10