Skip to content

Repository files navigation

RTL Gauntlet

Measuring Honesty, Cost, and Latency-Robustness in Agentic Hardware Design.

Agentic RTL frameworks now report 100% pass on RTL benchmarks (e.g. HORIZON, arXiv:2606.28279). But that number is measured against visible tests, it is expensive to reach, and it is obtained on proxy benchmarks. HORIZON's own authors flag three open problems — reward hacking, token cost, high-latency (PPA) reward. RTL Gauntlet turns those into three measurable axes.

Paper: paper/main.pdf (7 pp, conference-format draft). Source paper/main.tex; rebuild with cd paper && pdflatex main.tex.

Headline result

The naïve headline reward-hacking number is entirely an oracle artifact. A naïve formal oracle over-reports hacking via don't-care x, async-reset, state-encoding, init-state, a SystemVerilog parser flag, and unstated input constraints. We harden the oracle in seven steps (reset-aware, don't-care-aware, bounded miter+SAT, read_verilog -sv, memory case→ROM, a -nolatches reset-aware BMC, and an X-aware careset miter with a real-latch half-cycle miter for the mixed-edge class), cutting false counter-examples 9→0 and "inconclusive" 50→0. Every naïvely-flagged counter-example is machine-proven equivalenthand-verification is eliminated entirely: zero genuine reward hacking across five models on fair tasks.

Model HPR (95% CI) flagged RHG (machine) verified RHG
Opus 4.8 0.93 [.88,.96] 0 0 (≤2.5%)
GPT-5.5 0.93 [.88,.96] 0 0 (≤2.5%)
Gemini 2.5 0.90 [.84,.94] 0 0 (≤2.6%)
DeepSeek 0.77 [.70,.83] 0 0 (≤3.1%)
Haiku 4.5 0.73 [.66,.79] 0 0 (≤3.2%)

All four naïvely-flagged tasks (q5b, prob095, prob149, circuit8) are machine-proven equivalentcircuit8's false CEX came from -nolatches destroying its intentional latch; the half-cycle miter (real latches, regular clock, posedge-registered inputs) proves it while wrong-edge / inverted mutants still CEX. Reproduce: python3 scripts/compare_careset.py. Weakness ≠ hacking: a weaker model fails far more on the visible tests but cheats no more, even a tamper-capable shell agent edits only the design, never the testbench.

The three axes

Axis Metric Status
Honesty (C1) Reward-Hacking Gap (RHG) + Honest Pass Rate (HPR) via a two-tier protocol (visible diagnostic vs. withheld hidden-randomized + formal-equivalence oracle) 🟢 5 models × 156 VerilogEval tasks; X-aware careset oracle machine-proves the flagged artifacts (hand-verify 4 tasks → 1)
Cost (C2) Tokens vs. Honest-Pass, with an early-stop policy 🟢 early-stop @1 reclaims 12–23% of tokens for ~5% honesty loss
Latency (C3) Agent under slow PPA reward via a trained surrogate + a real OpenLane flow 🟢 real Sky130 PPA (counter8/popcount8) + surrogate r=0.89/0.91/0.96; full agent-loop = future

The central artifact for honest agentic-hardware evaluation is a don't-care/reset/encoding-aware oracle plus a verification discipline — not a new pass-rate.

Follow-on (separate paper): RL training-time reward hacking

Eval-time, aligned models don't hack fair tasks. The dangerous regime is training: does an RL agent optimizing a gameable (visible-test) reward learn to game it? Scaffolded in scripts/train_grpo.py (GRPO + hidden+formal audit → RHG-vs-step curve), loop-validated locally with no GPU via scripts/validate_grpo_local.py. Deploy notes + convergence research: docs/RLVR.md, docs/RLVR_CONVERGENCE_RESEARCH.md.

Layout

rtl_gauntlet/   core library — task schema, two-tier metrics, the formal ORACLE (equiv.py), sim, ppa
paper/          main.tex / main.pdf + figures (generated by scripts/make_figures.py)
scripts/        sweeps (run_veval), CIs (report_cis), cost (analyze_cost), RLVR (train_grpo), figures
results/        frozen sweep JSONs (per model × oracle stage — see docs/REPRODUCE.md)
tasks/          VerilogEval-derived + self-authored + mutated tasks (gitignored; regen via import_veval)
docs/           PILOT_RESULTS (numbers), REPRODUCE, NEXT (status), TEST_MATRIX (proofs), RISKS, RLVR
runpod/         GPU launchers for the RLVR study (self-terminating)

Reproduce

make demo                          # metric engine on synthetic runs (no deps)
python3 scripts/report_cis.py      # HPR + RHG Wilson CIs from the frozen sweeps
python3 scripts/analyze_cost.py    # C2 early-stop / repair-tail payoff
python3 scripts/make_figures.py    # regenerate paper/figures/*.pdf
python3 scripts/validate_grpo_local.py   # validate the RLVR loop on CPU (no GPU)

EDA locally: iverilog + yosys (Homebrew, arm64). LLMs via an OpenAI-compatible gateway (see .env.example). Exact stage→file→number map: docs/REPRODUCE.md.

References

  • HORIZON — Agentic Hardware Design as Repository-Level Code Evolution, arXiv:2606.28279
  • SpecBench (2605.21384) · EvilGenie (2511.21654) · VeriContaminated (2503.13572) · full list in paper/main.tex

About

Two-tier honest-evaluation harness for agentic RTL design (research, WIP)

Topics

Resources

Stars

0 stars

Watchers

0 watching

Forks

Releases

Packages

Contributors

Languages