Clover: A Neural-Symbolic Agentic Harness with Stochastic Tree-of-Thoughts for Verified RTL Repair¶

🕒 Published (v1): 2026-04-19 07:04 UTC · Source: Arxiv · link

Why this paper was selected

Neural-symbolic agentic harness with stochastic tree-of-thoughts for verified repair

Ask a follow-up

Open an assistant pre-loaded with this paper's context.

TL;DR¶

Clover is a neural-symbolic agentic harness that repairs Register-Transfer-Level (RTL) hardware code by orchestrating LLM agents and SMT-based symbolic solvers within a structured search framework. It introduces Stochastic Tree-of-Thoughts (SToT) as a test-time scaling mechanism that manages the main agent's context as a probabilistically-sampled hypothesis tree. On the RTL-repair benchmark, Clover fixes 96.8% of bugs within a fixed time budget, achieving 87.5% pass@1.

Problem¶

RTL program repair is heterogeneous: high-level bugs (coding style, algorithmic intent) suit LLMs, while low-level bugs (Boolean expressions, cycle-shift timing) suit symbolic methods. Neither alone covers the full spectrum. LLM-only approaches suffer from context window saturation on dense waveforms and stochastic unreliability; symbolic-only methods are restricted to predefined templates and scale poorly as abstraction rises. No prior system orchestrates both within a verified, reliable harness.

Method¶

Clover wraps a main agent in a three-level nested loop: (1) an outer hypothesis-making loop, (2) a validation loop that applies patches and checks against simulation, and (3) an inner patch loop where the LLM queries context or emits a patch. Two sub-agents are spawned on demand—a context agent (navigates RTL codebases via a language server with query_def/query_ref) and a lint-fix agent (handles linter errors without polluting the main context).

The SMT repair module extends RTL-Repair [11] with an additional cycle-shift template: a free variable \(\phi\) is inserted as a multiplexer selector to model whether a signal is combinational or registered, and the SMT solver assigns a constant to \(\phi\) satisfying bounded-model-checking assertions. Template selection is delegated to the LLM rather than applied sequentially; the solver returns structured repair actions, and the LLM synthesizes the final source patch.

Stochastic Tree-of-Thoughts (SToT) organizes hypotheses as a tree. Instead of DFS/BFS with LLM-evaluated node scoring, Clover uses a hand-crafted heuristic:

\[f(c, h) = \lambda_1 \cdot \frac{tb_p(c)}{N_{tb}} + \lambda_2 \cdot N_Q(h) - \lambda_3 \cdot N_{CE}(h) - \lambda_4 \cdot N_{tok}(h) - \lambda_5 \cdot N_P(h) + b\]

where \(tb_p(c)\) is passing testbenches, \(N_Q\) is informative queries, \(N_{CE}\) compilation errors, \(N_{tok}\) token usage, and \(N_P\) number of patches. Nodes are sampled proportionally to a softmax over \(f\):

\[\Pr[s=(c,h)] = \frac{e^{f(c,h)}}{\sum_i e^{f(c_i, h_i)}}\]

This converts LLM stochasticity into a directed search rather than blind exploration.

Key Contributions¶

Clover harness: a multi-agent scaffold for RTL APR with domain-specific toolbox (VCD viewer, Verilator linter, slang-server language server, RTL simulator)
Stochastic Tree-of-Thoughts: a test-time scaling strategy with heuristic-guided probabilistic node selection; no retraining needed to adjust \(\lambda\) coefficients
Neural-symbolic integration: LLM-driven template selection and patch materialization composing with SMT solvers; extended to SystemVerilog
Cycle-shift SMT template: new template modeling register-vs-wire temporal behavior as a free-variable multiplexer for SMT formulation

Results¶

Fixes 96.8% of bugs in the RTL-repair benchmark within a fixed time limit (31/32 benchmarks passed)
Covers 94% more bugs than the best traditional baseline (RTL-Repair [11], 16/32 passed)
Covers 63% more bugs than the best LLM-based baseline (UVLLM [9], 19/32 passed)
Achieves average pass@1 = 87.5%, indicating high per-run reliability
MEIC [24] passed 10/32; Clover passed 31/32

Limitations¶

Evaluation confined to a single benchmark dataset (RTL-repair [11]); generalization to other RTL corpora is unverified
Algorithmic-level bugs (top of the abstraction spectrum) are explicitly excluded—no fully automatic APR method handles these reliably
Heuristic \(\lambda\) coefficients are manually tuned; no principled method for setting them is provided
The cycle-shift template requires agent-guided signal targeting; purely symbolic application would be infeasible due to combinational loop risk
Computational cost of SToT (maintaining and restoring multiple LLM dialogue states) is not quantified relative to single-pass LLM approaches

Relevance to Harnesses / Meta-Harnesses¶

Clover is a direct instantiation of harness engineering as a first-class design methodology: the paper explicitly cites harness engineering [14] and context engineering [15] as its organizing principle, making it an unusually clean case study in what a domain-specific harness looks like in practice. The architecture—a main orchestrator spawning narrow sub-agents, a curated toolbox, and a test-time scaling loop that manages context state—maps directly onto the general harness template, applied to hardware verification. The SToT mechanism is notable for harness researchers because it shows how to absorb LLM stochasticity within the harness (via structured search with a symbolic heuristic) rather than pushing reliability onto the model itself. The clean separation between orchestrator context and sub-agent contexts (context agent, lint-fix agent) is a concrete example of cognitive load partitioning across a multi-agent harness.