Source note
Clover: A Neural-Symbolic Agentic Harness with Stochastic Tree-of-Thoughts for Verified RTL Repair
Rtl RepairNeural Symbolic AgentsTree Of ThoughtsHardware VerificationCode Intelligence
Summary
Clover is an automated RTL repair system that combines LLM agents with SMT-based symbolic repair and a search procedure over repair hypotheses. It targets verified hardware bug fixing, where pure template-based repair misses many bugs and pure LLM repair is unreliable on long RTL code and waveform data.
Problem
- RTL program repair is slow and costly because engineers must inspect code, run simulations, read waveforms, and try patches across many iterations.
- Existing RTL repair methods split into two weak extremes: symbolic systems are precise but limited to a small set of repair templates, while LLM systems are flexible but can lose context, misread low-level traces, and produce inconsistent patches.
- Real RTL bugs often need several repair steps at different abstraction levels, so a single repair strategy does not cover the full space of fixes.
Approach
- Clover treats RTL repair as a structured search over code states. A main agent proposes bug hypotheses, applies one patch at a time, runs validation, and keeps successful edits so it can perform multi-step repair.
- The system routes work by task type: LLM sub-agents handle code understanding and lint fixing, while SMT-based symbolic repair handles low-level edits that fit repair templates.
- It adds an RTL-specific toolbox with simulator access, a VCD trace viewer, a language server for code navigation, Verilator, and a custom linter so agents can inspect designs and test candidate fixes.
- Its main search method is stochastic tree-of-thoughts: each hypothesis and dialogue state becomes a node in a search tree, and Clover samples which node to expand using a heuristic based on passed testbenches, number of queries, compile errors, token use, and patch count.
- Clover extends prior symbolic RTL repair with an added cycle-shift template for temporal bugs and lets the agent choose when to invoke each template, then converts solver output into source-level patch actions.
Results
- On the RTL-Repair benchmark, Clover fixes 96.8% of bugs within a fixed time limit.
- The paper claims this covers 94% more bugs than traditional baselines and 63% more bugs than LLM-based baselines.
- Clover reports an average pass@1 of 87.5%, which the authors use as evidence that the search procedure improves reliability, not only peak success rate.
- The excerpt names the benchmark as RTL-Repair and compares against both traditional symbolic/template methods and prior LLM-based RTL repair systems, but it does not give the full per-baseline table in the provided text.
- The paper also claims broader symbolic applicability by extending the repair flow to SystemVerilog and adding a cycle-shift repair template, though the excerpt does not include an isolated ablation number for those additions.