PaperlayerView exact revision on arXiv

Source-linked AI summary

NoTB: Oracle-Free Triage of LLM-Generated RTL via Cross-Model Formal Consensus

Elisavet Lydia Alvanaki, Je Yang, Biruk Seyoum, Luca P. Carloni

arXiv:2608.21962v1cs.ARcs.AI

TL;DR

Assessing LLM-generated RTL without trusted testbenches or golden designs is difficult because existing oracle-free signals depend on learned judges or finite simulations. NoTB generates implementations from independent LLM families and applies SEC to cluster provably equivalent designs, using family diversity as a correctness signal. On 78 CVDP tasks, four-family consensus reaches 94.7% precision at 27% coverage, while three-family consensus reaches 87% at 33%, enabling tunable selective triage.

  • Problem

    Trusted testbenches and golden RTL are often unavailable, while simulation-based agreement and LLM judges provide limited or model-dependent correctness evidence.

  • Method

    NoTB generates RTL from multiple independently trained LLM families, applies SEC, clusters provably equivalent implementations, and scores clusters by model count.

  • Results

    94.7% precision at 27% coverage is achieved with four-family consensus, while three-family consensus achieves 87% precision at 33% coverage on 78 CVDP tasks.

  • Takeaways & Limitations

    Formal cross-model agreement provides a tunable accept/defer signal for high-confidence RTL triage without testbenches or model-dependent oracles.

  • Takeaways & Limitations

    The framework represents each LLM family by a single representative model and includes a demonstrated simulation setting where testbench stimulus misses distinguishing behavior.

Abstract

from arXiv · show

Large language models (LLMs) are increasingly used to generate register-transfer-level (RTL) designs from natural-language specifications. However, assessing functional correctness at early stages remains a fundamental challenge. Existing oracle-free approaches rely either on simulation-based agreement, which depends on LLM-generated testbenches that can fail or vary across models, or on LLM-as-a-judge heuristics, which produce inconsistent predictions. We introduce NoTB, an oracle-free triage framework that infers correctness from cross-model formal consensus. NoTB generates RTL implementations from multiple independently trained LLM families and applies Sequential Equivalence Checking (SEC) to identify designs that are provably equivalent. We show that the diversity of model families within an SEC-equivalent cluster induces a calibrated correctness signal, enabling risk-coverage tradeoffs without requiring testbenches. On 78 CVDP RTL-generation tasks, four-family formal consensus achieves 94.7% precision at 27% coverage; three-family consensus achieves 87% precision at 33% coverage. These operating points give designers a tunable accept/defer rule before a trusted testbench or golden RTL is available. Overall, NoTB demonstrates that formal cross-model agreement provides a reliable basis for high-confidence triage without model-dependent oracles

1 Introduction

NoTB addresses the difficulty of assessing LLM-generated RTL without trusted oracles by replacing testbench- and judge-based agreement with formal cross-model consensus. Across 78 CVDP tasks, model diversity in SEC-equivalent clusters provides a calibrated precision–coverage signal.

  • Reliable early correctness assessment is difficult because trusted testbenches or golden RTL are expensive and error-prone.
  • NoTB applies SEC to implementations from independently trained LLM families, clustering designs proven functionally identical over the full input space.
  • Model count measures the number of distinct LLM families in an equivalence cluster and serves as a calibrated correctness signal.
  • 94.7% precision at 27% coverage is achieved with four-family agreement, while three-family agreement reaches 87% precision at 33% coverage.
  • Simulation-based oracle-free triage is testbench dependent, with four-way agreement precision ranging from 43% to 84% across testbench-generating LLMs.

2 Related Work

Prior oracle-free RTL triage uses learned judgment, sample agreement, or finite-test behavioral agreement, each defining correctness through an imperfect proxy. NoTB instead defines agreement through formal SEC over hardware behavior.

  • Oracle-free correctness assessment groups prior methods by learned judgment, sample agreement, and behavioral agreement under generated testbenches.
  • LLM-as-a-judge replaces test execution with a learned heuristic whose predictions can vary across generating models and introduce systematic bias.
  • RTL self-consistency must compare hardware behavior rather than emitted code strings because syntactic similarity does not establish equivalence on corner-case sequences.
  • Simulation-based clustering can merge functionally distinct implementations when finite test inputs fail to exercise their differences.
  • NoTB defines agreement through SEC, clustering implementations only when formal analysis proves convergence to common behavior.

3 Proposed Methodology

NoTB uses SEC-proven equivalence across independently generated RTL implementations to form conservative clusters and scores the dominant cluster by represented model-family diversity. A threshold on this confidence signal creates a selective accept/defer rule that trades precision against coverage.

  • 3. Proposed Methodology: NoTB samples RTL from multiple LLM families, applies SEC pairwise, builds equivalence clusters, and scores the dominant cluster by its distinct model-family count.The pipeline samples implementations, proves equivalence, constructs clusters, and uses cross-family convergence rather than individual-model reliability.
  • 3.2 Formal Equivalence Clustering: SEC comparisons accept equivalence only when formally proven; non-equivalent and inconclusive results do not create equivalence edges.This conservative rule ensures clusters represent behaviors connected by proven equivalence, while preserving individual proof fidelity.
  • 3.2 Formal Equivalence Clustering: NoTB represents proven equivalences as graph edges and uses connected components as clusters, including transitive equivalence without inventing unsupported direct edges.If two links are proven, their implementations share a cluster; a direct pairwise edge still requires its own SEC proof.
  • 3.3 Efficient Equivalence Clustering: Lightweight hashing, union-find, and non-equivalence caching reduce SEC comparisons while preserving the invariant that only proven equivalences form clusters.The naive cost is O(|D(s)|^2), or O(M^2K^2) for M families and K samples per family.
  • 3.4 Confidence as Model Diversity: The dominant cluster represents the largest behavioral hypothesis, with ties resolved by model count and then a fixed deterministic member ordering.Its model count measures how many independent model families converged to that behavior.
  • 3.4 Confidence as Model Diversity: Higher confidence thresholds require stronger cross-model formal consensus, accepting fewer specifications and producing a precision–coverage tradeoff.NoTB therefore performs selective prediction: it accepts sufficiently supported dominant behaviors and defers the rest to existing verification.

4 Evaluation

NoTB is evaluated using precision and coverage in an experimental setup spanning datasets, models, and oracle-free baselines.

  • 4. Evaluation: The evaluation reports precision and coverage for NoTB using datasets, models, and oracle-free baselines.These metrics and comparison components define the evaluation setup described here.

4.1 Experimental Setup

The experimental setup evaluates NoTB on 78 CVDP hardware-generation tasks using four LLM families and five samples per family, while reserving official testbenches for ground truth. It compares NoTB with LLM-as-a-judge and simulation-based consensus using specification-level precision and coverage.

  • Dataset and models: NoTB uses all 78 CVDP code-generation hardware tasks, four independently trained LLM families, and up to 20 candidates per specification.The setup samples five implementations from each family: Claude 3.7 Sonnet, GPT-OSS-120B, Gemini 2.5 Flash, and Qwen 3 Coder.
  • Ground truth: Official cocotb testbenches establish ground truth only; NoTB’s triage signal comes from SEC clustering rather than those testbenches.A selected cluster is correct only when every implementation it contains passes all functional tests.
  • Dataset and models: The reported functional-correctness evaluation excludes tasks with elaboration failures, too few synthesizable candidates, or unusable generated testbenches.These exclusions are described as independent of NoTB’s signal and applied uniformly across methods.
  • Baselines: The baselines are LLM-as-a-judge prediction and simulation-based consensus clustering under generated testbenches.The first predicts correctness from the specification and implementation; the second clusters implementations by behavioral agreement.
  • Metrics: Precision is correct accepts divided by total accepts, while coverage is accepts divided by evaluable specifications, both reported at specification level.False-positive rate, recall, and accuracy use separate denominators when reported, with Fisher’s exact test for high- versus low-consensus comparisons.

4.2 Why Formal Consensus?

The evaluation shows that judge-based and simulation-based oracle-free agreement can depend strongly on the evaluator, testbench, or stimulus. Formal SEC instead makes consensus a property of the RTL designs and supports selective prediction by model-count thresholds.

  • 4.2.1 LLM-as-a-Judge Ablation.: Judge acceptance varies by code generator despite similar ground-truth pass rates, so LLM-as-a-judge does not provide a stable high-confidence triage signal.Ground-truth pass rates are 55.9–59.7%, while Gemini and GPT show a 33-point acceptance spread across generators.
  • 4.2.2 Simulation-Based Clustering is Testbench-Dependent.: Simulation-based precision at mc≥4 ranges from 43% to 84% when only the generated testbench changes on a fixed RTL candidate pool.The variation occurs across Claude-, Gemini-, and GPT-generated testbenches.
  • 4.2.2 Simulation-Based Clustering is Testbench-Dependent.: Figure 3 compares precision across model-count thresholds for formal SEC and three simulation-based clusterings, with each bar showing correct and accepted specifications.The comparison isolates formal equivalence from testbench-dependent behavioral agreement.
  • 4.2.2 Simulation-Based Clustering is Testbench-Dependent.: Table 2 defines selective accept rules by requiring the largest equivalence cluster to contain at least the indicated number of model families.Model count is therefore used as the decision threshold for accepting specifications.
  • 4.2.2 Simulation-Based Clustering is Testbench-Dependent.: Simulation can merge four failing and sixteen passing 64b/66b encoder candidates into one mc=4 cluster when generated stimulus misses distinguishing behavior.A GPT-generated testbench can also deadlock after reset and produce no clusters despite all candidates compiling.
  • 4.2 Why Formal Consensus?: NoTB replaces heuristic agreement with SEC-certified agreement, making cross-model consensus a property of the designs rather than the evaluator or testbench.SEC identifies candidate sets proven functionally identical throughout the input space.

4.3 NoTB Performance

NoTB’s formal cross-model consensus predicts correctness: precision increases as more model families appear in the dominant SEC-equivalent cluster, while coverage and computation trade off against stricter thresholds and more samples.

  • Triage Performance: 63% precision at mc≥1 rises to 85.3%, 87%, and 94.7% at mc≥2, mc≥3, and mc≥4, respectively.Correctness improves with model count within the dominant SEC cluster.
  • Triage Performance: 94.7% precision at mc≥4 and 27% coverage provides the highest-precision operating point.The broader mc≥3 regime reaches 87% precision at 33% coverage.
  • Model Family Sensitivity: High-precision triage remains possible after omitting any one model family, although dropping Claude reduces mc≥3 precision to 90%.Dropping Qwen leaves mc≥3 precision at 100%, indicating sensitivity to the omitted family while preserving portability.
  • Completions per Model: At mc≥4, precision stays above 93% as completions per family increase from K=1 to K=5, while coverage rises from 14% to 27%.Gains diminish beyond K=3, suggesting that a modest number of samples captures most high-confidence cases.
  • Cost Analysis: Hash deduplication and transitivity pruning reduce the theoretical 190 SEC invocations per specification by roughly 32% on average.Only proven equivalences enter clusters; inconclusive results reduce coverage but cannot introduce false merges.
  • Cost Analysis: Median wall-clock time grows from 1 minute at K=1 to 16 minutes at K=5, while independent SEC checks permit parallel execution.NoTB exchanges judge- and testbench-based per-call spending for local SEC computation.

5 Conclusion

NoTB replaces testbench- and judge-based agreement with formal cross-model consensus for oracle-free RTL triage. Across 78 CVDP tasks and four LLM families, it reaches up to 94.7% precision at 27% coverage.

  • 5 Conclusion: NoTB clusters RTL candidates by SEC-proven behavioral equivalence and scores clusters by the number of represented LLM families.The framework uses formal consensus instead of testbench- or judge-based agreement.
  • 5 Conclusion: 94.7% precision at 27% coverage is achieved on 78 CVDP RTL-generation tasks across four LLM families.This is the reported highest-precision operating point.
  • 5 Conclusion: Formal cross-model consensus provides an oracle-free basis for high-confidence triage before trusted testbenches or golden RTL are available.The conclusion frames NoTB as a correctness-triage framework rather than a replacement for full validation.
Loading 2608.21962v1…