Paper deep dive
NoTB: Oracle-Free Triage of LLM-Generated RTL via Cross-Model Formal Consensus
Elisavet Lydia Alvanaki, Je Yang, Biruk Seyoum, Luca P. Carloni
Intelligence
Status: succeeded | Model: Gemma-4-26B-A4B | Prompt: intel-v1 | Confidence: 91%
Last extracted: 8/25/2026, 7:47:47 AM
Summary
The paper introduces NoTB, an oracle-free triage framework for assessing the functional correctness of LLM-generated RTL designs. NoTB leverages cross-model formal consensus by generating RTL from multiple independent LLM families and applying Sequential Equivalence Checking (SEC) to identify provably equivalent designs. The framework uses the diversity of model families within equivalence clusters as a calibrated correctness signal, enabling designers to balance precision and coverage without relying on testbenches or golden models. Experiments on the CVDP benchmark demonstrate that NoTB achieves high precision (94.7%) with low coverage (27%) using four-family consensus.
Entities (10)
Relation Signals (10)
NoTB ā achievesprecision ā 94.7%
confidence 95% Ā· four-family formal consensus achieves 94.7% precision at 27% coverage
NoTB ā uses ā Sequential Equivalence Checking
confidence 95% Ā· NoTB generates RTL implementations from multiple independently trained LLM families and applies Sequential Equivalence Checking (SEC) to identify designs that are provably equivalent.
NoTB ā evaluatedon ā CVDP Benchmark
confidence 92% Ā· We evaluate NoTB on the CVDP benchmark using four independently trained LLM families.
NoTB ā generatesfrom ā GPT-OSS 120B
confidence 90% Ā· For each specification, we generate candidate RTL implementations using M=4 independently trained LLM families: ... GPT-OSS-120B ...
NoTB ā generatesfrom ā Gemini 2.5 Flash
confidence 90% Ā· For each specification, we generate candidate RTL implementations using M=4 independently trained LLM families: ... Gemini 2.5 Flash ...
NoTB ā generatesfrom ā Qwen 3 Coder
confidence 90% Ā· For each specification, we generate candidate RTL implementations using M=4 independently trained LLM families: ... and Qwen 3 Coder.
NoTB ā generatesfrom ā Claude 3.7 Sonnet
confidence 90% Ā· For each specification, we generate candidate RTL implementations using M=4 independently trained LLM families: Claude 3.7 Sonnet...
Cypher Suggestions (0)
No Cypher suggestions yet.
Abstract
Abstract: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
Tags
Links
- Source: https://arxiv.org/abs/2608.21962v1
- Canonical: https://arxiv.org/abs/2608.21962v1
Trouble viewing inline? Open PDF directly ā
Full Text
73,704 characters extracted from source content.
Expand or collapse full text
NoTB: Oracle-Free Triage of LLM-Generated RTL via Cross-Model Formal ConsensusDOI: X.XXXXXXXConference: International Symposium on Machine Learning for CAD; September 7, 2026; Jeju, South KoreaConference: 2026 ACM/IEEE International Symposium on Machine Learning for CAD; September 07ā09, 2026; Jeju Island, Republic of Korea2026 ACM/IEEE International Symposium on Machine Learning for CAD (MLCAD ā26), September 07ā09, 2026, Jeju Island, Republic of KoreaDOI: 10.1145/3831599.3840342ISBN: 979-8-4007-2878-5/2026/09CCS: Hardware Methodologies for EDA Elisavet Lydia Alvanaki email: ealvanaki@cs.columbia.edu Affiliation: Dept. of Computer Science Columbia University , New York , USA , Je Yang email: je.yang@cs.columbia.edu Affiliation: Dept. of Computer Science Columbia University , New York , USA , Biruk Seyoum email: biruk@cs.columbia.edu Affiliation: Dept. of Computer Science Columbia University , New York , USA and Luca P. Carloni email: luca@cs.columbia.edu Affiliation: Dept. of Computer Science Columbia University , New York , USA 2026; Ā© c Abstract. 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. Keywords: RTL generation, Large Language Models, Equivalence Checking ā c-license: by 1. Introduction Large language models (LLMs) are increasingly capable of generating synthesizable register-transfer-level (RTL) designs directly from natural-language specifications. Given a text description of desired hardware behavior, a model produces hardware-description language (HDL) code that is then compiled, simulated, and checked for correctness 6; 13; 7. Most existing methods rely on an oracle, a trusted artifact, such as a reference testbench or golden RTL model, to evaluate the correctness early in the design process. Recent benchmarks report high pass rates against such oracles, suggesting that LLM-assisted hardware design is maturing 10; 18. In practice, however, constructing a reliable oracle is itself expensive and error-prone, and developers rarely have one at the start of a design task. A key challenge in LLM-assisted RTL design is therefore not candidate generation (models produce many candidates cheaply), but triage: deciding which candidates merit downstream verification before a trusted oracle becomes available. Existing oracle-free approaches attempt to fill this gap, but remain fundamentally limited 19; 17; 20. LLM-as-a-judge 20 replaces execution with model-based prediction, but provides no formal guarantees and exhibits strong model-dependent bias: false-acceptance rates vary by up to 45% across generating models despite similar ground-truth pass rates, making it unreliable as a triage signal (as shown in Section 4.2). Operating on the intuition that the agreement of many models is evidence of correctness 14; 2, simulation-based self-consistency clusters implementations by behavioral agreement under a generated testbench. This intuition rests on two strong assumptions that rarely hold in practice: that the testbench covers the relevant input space and that incorrect implementations disagree with each other. Both can fail simultaneously. A weak testbench can miss a critical input, thus allowing a false consensus to form among incorrect designs; this might collapse precision to 43%, as shown in Section 4.2. Moreover, simulation-based agreement compounds shared-error risk: when multiple models converge on the same wrong behavior, a weak testbench can still falsely detect that behavior as consensus 19; 2. These shortcomings reflect a fundamental limitation of existing heuristic approaches that infer correctness from incomplete or learned signals rather than from formal guarantees. To address these challenges, we introduce NoTB, a framework that replaces a heuristic agreement with a formally certified agreement. The central insight is that if implementations produced by independently trained LLM families11 1 An LLM family is a set of LLMs derived from a common base model (e.g. through fine-tuning, distillation, or versioning) rather than trained independently from scratch. In this paper, we represent each LLM family by a single representative model. are proven equivalent over the full input space via Sequential Equivalence Checking (SEC) 8; 12, their agreement is a property of the designs, not of the testbench. Cross-family agreement is more likely to reflect correctness rather than shared error, since independently trained models exhibit different inductive biases and failure modes 15, making convergence on the same wrong answer unlikely. SEC guarantees that agreement is not an artifact of a finite set of tests. Given a specification, NoTB generates implementations from multiple LLM families and applies SEC 8; 12 to identify sets of designs that provably are functionally identical throughout the input space. These equivalence classes partition the candidate set into clusters of interchangeable implementations. We define the model count of a cluster as the number of distinct LLM families represented within it, and show that model count induces a calibrated correctness signal: a higher model count corresponds systematically to lower error rates. This enables risk-aware triage with explicit control over the precision--coverage22 2 In this paper, coverage denotes the percentage of specifications for which NoTB makes a prediction among those evaluated (e.g., out of all specifications in a given benchmark suite).tradeoff. Crucially, NoTB does not replace verification. It selectively certifies the high-confidence subset so that those designs can bypass early-stage checks, while the remainder proceeds through the existing flow unchanged. We evaluate NoTB on the CVDP benchmark 11 using four independently trained LLM families. When the dominant equivalence cluster contains all four families, NoTB achieves 94.7% precision at 27% coverage; relaxing the threshold to three families yields 87% precision at 33% coverage. This monotonic relationship ā stronger cross-model agreement, lower false-acceptance risk, is the central empirical result and enables users to select a confidence threshold suited to their verification budget. Our paper makes the following contributions: ā¢ We show that simulation-based oracle-free RTL triage is testbench dependent: on a fixed candidate pool, the precision of a four-way agreement varies from 43% to 84% purely as a function of which LLM generated the testbench. ā¢ We introduce NoTB, a novel framework that replaces the learned and simulation-based agreement with formal cross-model consensus. NoTB clusters candidate implementations by SEC and scores each cluster by its model count, i.e., the number of distinct LLM families represented in the cluster. ā¢ Our experiments with 78 CVDP RTL-generation tasks and four LLM families demonstrate that model count is a calibrated correctness signal: four-family agreement reaches 94.7% precision at 27% coverage, and three-family agreement reaches 87% at 33%, with the signal remaining stable under leave-one-out family ablation. 2. Related Work Oracle-free correctness assessment for LLM-generated RTL relies on proxy signals in place of a trusted artifact. We group prior work by such signals: learned judgment (LLM-as-a-judge), sample agreement (self-consistency), and behavioral agreement under a generated testbench (simulation-based clustering). Heuristic Correctness Prediction (LLM-as-a-Judge). To reduce reliance on test execution, recent approaches adopt LLM-as-a-judge 20, where a secondary model predicts correctness given a specification and its RTL implementation. While this eliminates the need for testbenches, it replaces execution with a learned heuristic. Such predictions are inherently model-dependent and can vary significantly between generating models, limiting their reliability as correctness signals. This variability introduces systematic bias, making LLM-based judgment unsuitable as a high-confidence triage signal. Agreement and Self-Consistency. Self-consistency methods use agreement among multiple samples as a confidence signal 14; 5. This requires a meaningful notion of when two answers are the same. For RTL, textual agreement is insufficient: syntactically different designs may be equivalent, while similar designs may differ on corner-case sequences. Hence, oracle-free RTL triage requires agreement on hardware behavior, not on emitted code strings. Agreement under Incomplete Evaluation. Recent work has explored agreement-based selection for RTL generation 14; 5. In particular, VRank 19 generates multiple candidate implementations and clusters them based on behavioral equivalence under a shared testbench, ranking clusters by consistency. However, agreement is defined with respect to a finite set of test inputs. As a result, functionally distinct implementations may appear equivalent if differences are not exercised by the testbench. Moreover, clustering depends on the quality of the testbench itself, which is generated by an LLM, introducing an additional source of bias and uncertainty. Formal Agreement as a Correctness Signal. NoTB differs from prior oracle-free methods in where agreement is defined. LLM-as-a-judge defines agreement through a learned evaluator. Simulation-based clustering defines agreement through a generated testbench and a finite set of observed traces. NoTB defines agreement through SEC: two implementations are clustered only when a formal tool proves convergence to a common behavior. This distinction changes the role of agreement. In prior methods, agreement is an empirical proxy for correctness. In NoTB, agreement identifies a formally proven behavioral class, and model diversity within that class is used as the empirical confidence signal. 3. Proposed Methodology Figure 1. Overall flow of the NoTB framework. NoTB uses formal agreement among independent generators as the triage signal. If implementations produced by different LLM families are proven equivalent for all input sequences, their agreement provides stronger evidence than finite-test agreement or learned judgment. NoTB operationalizes this idea in four stages, as shown in Figure 1. First, it samples RTL implementations from multiple LLM families. Second, it applies SEC to compare candidate implementations. Third, it constructs equivalence clusters from proven SEC results. Finally, it scores the dominant cluster by its model count, defined as the number of distinct LLM families represented in the cluster. This score enables a tunable precisionācoverage tradeoff: increasing the threshold requires agreement among more model families, which reduces the number of accepted specifications but increases confidence that those accepted are correct. 3.1. Multi-Model RTL Generation Given a specification s, NoTB constructs a candidate set by sampling from multiple independently trained LLM families. Let ā³=m1,ā¦,mMM=\m_1,ā¦,m_M\ denote the set of model families. For each model māā³m , we sample K implementations, yielding ā”(s)=āmāā³dm,1,ā¦,dm,K.D(s)= _m \d_m,1,ā¦,d_m,K\. Each implementation dāā”(s)d (s) is associated with its generating model family modelā”(d)āā³model(d) . Sampling across model families, rather than only within a single model, exposes different inductive biases and error modes. NoTB does not assume that any individual model is reliable; it uses cross-family convergence as evidence. All models are prompted to generate synthesizable Verilog under a shared set of constraints: a single top-level module, no SystemVerilog-only constructs, no simulation-only features such as initial blocks or delays, and a single-driver discipline. These constraints standardize the generated implementations and make them compatible with downstream SEC. 3.2. Formal Equivalence Clustering Given the candidate set ā”(s)D(s), NoTB constructs a graph that captures formal equivalence relationships among implementations. For each pair (di,dj)(d_i,d_j), we invoke Cadence JasperGold to determine whether the two designs produce identical outputs for all input sequences. To automate comparisons across independently generated RTL, NoTB infers clock and reset signals from port names such as clk, reset, and rst_n. Each SEC query yields one of three outcomes: equivalent, non-equivalent, or inconclusive. We define diā”djd_iā” d_j only when equivalence is proven. Tool errors, interface mismatches, and inconclusive results do not contribute equivalence edges. NoTB represents the SEC results as an undirected graph Gā”(s)=(V,E)G(s)=(V,E), where V=ā”(s)V=D(s) and (di,dj)āEādiā”dj(d_i,d_j)ā E d_iā” d_j. The connected components of Gā”(s)G(s) define the equivalence clusters ā”(s)=C1,ā¦,Ck.C(s)=\C_1,ā¦,C_k\. Each cluster corresponds to a set of implementations connected through proven equivalence. Equivalence may be direct or transitive: if diā”djd_iā” d_j and djā”dkd_jā” d_k are both proven, then did_i, djd_j, and dkd_k belong to the same cluster. However, a direct graph edge between did_i and dkd_k is added only if their pairwise SEC query also proves equivalence. Thus, clusters use transitive closure, but edges remain faithful to individual SEC proofs. This construction is conservative. NoTB merges implementations only when equivalence has been formally established. Non-equivalence results help separate behaviors, and inconclusive results leave candidates unmerged. Hence, each cluster represents a behavior shared by implementations that are provably equivalent under the SEC model. 3.3. Incremental SEC Pruning Naively evaluating all pairs requires Oā”(|ā”(s)|2)O(|D(s)|^2) SEC queries, or Oā”(M2āK2)O(M^2K^2) queries for M model families and K samples per family. NoTB reduces this cost using lightweight pruning while preserving the invariant that equivalence edges are introduced only by proof. First, NoTB eliminates syntactically identical implementations through hashing. Identical files are merged into the same cluster before SEC. Second, NoTB maintains equivalence components using union-find. When SEC proves diā”djd_iā” d_j, their components are merged, and future comparisons within the resulting cluster are skipped. NoTB also records proven non-equivalences between component representatives to avoid redundant cross-component comparisons. These optimizations affect which comparisons are skipped, not which equivalences are trusted. A cluster is still formed only from implementations connected by proven SEC equivalence. 3.4. Confidence as Model Diversity Given the equivalence clusters ā”(s)C(s) of a specification s, NoTB derives a correctness signal from model diversity. For each cluster Cāā”(s)C (s), we define its model count as the number of distinct model families represented in the cluster: modelā_ācountā(C)=|modelā”(d):dāC|.model\_count(C)= |\model(d):dā C\ |. Let Cā=argā”maxCāā”(s)ā|C|C^*= _C (s)|C| denote the largest equivalence cluster. NoTB assigns specification s the confidence score confidenceā”(s)=modelā_ācountā(Cā).confidence(s)=model\_count(C^*). The largest cluster is treated as the dominant behavioral hypothesis for the specification. Its model count measures how many independent model families converged to that behavior. If multiple clusters tie in size, NoTB selects the cluster with higher model count. Remaining ties are broken deterministically using a fixed ordering over cluster members . These tie-breaking rules affect only ambiguous cases and do not change the definition of the confidence signal. Given a threshold Ļ, NoTB accepts specification s if confidenceā”(s)ā„Ļ.confidence(s)ā„Ļ. Varying Ļ induces a precisionācoverage tradeoff: higher thresholds accept fewer specifications but require stronger cross-model formal consensus. This formulates correctness estimation as a selective prediction. Hence, NoTB is a selective-prediction method, not a universal correctness classifier. It accepts only the specifications whose dominant formally equivalent behavior has sufficient cross-family support, and defers the rest to the existing verification flow. 4. Evaluation We evaluated NoTB on precision and coverage metrics with an experimental setup that consists of datasets, models, and oracle-free baselines. Figure 2. Judge acceptance decomposed into correct accepts (solid) and false accepts (striped), for four judges across four generating models. The dashed line marks the ground-truth pass rate. Figure 3. Precision at each model-count threshold for formal SEC and three simulation-based clusterings. Counts show correct/accepted specifications per bar. 4.1. Experimental Setup Dataset and models. We evaluate NoTB on all 78 code-generation hardware design tasks from the code-generation tasks (cid003) of the NVIDIA CVDP benchmark 11. For each specification, we generate candidate RTL implementations using M=4M=4 independently trained LLM families: Claude 3.7 Sonnet 3, GPT-OSS-120B 9, Gemini 2.5 Flash 4, and Qwen 3 Coder 1. We sample K=5K=5 implementations per model, yielding up to 20 candidates per specification. We use the official cocotb testbenches solely to establish ground truth, not to construct NoTBās triage signal. A selected cluster is counted as correct only if every implementation it contains passes all functional tests. In NoTB, members of the same SEC cluster are functionally identical under the cocotb testbenches, consistent with their proven equivalence. Therefore, if one implementation fails under a given test, other implementations in the equivalence cluster do the same. We report functional correctness after excluding compile-time and spec-level failures, all of which are independent of NoTBās signal as they are determined by ordinary compilation and applied uniformly across all methods. Of the 78 tasks, we remove 5 on which Yosys fails to elaborate the design and the test harness cannot run, 2 for which fewer than 4 candidate implementations are synthesizable, leaving too small a pool for cross-model consensus, and 1 whose LLM-generated testbench fails to compile or deadlocks. In summary, we have 70 specifications evaluated across all models. We construct equivalence clusters using pairwise SEC with JasperGold, following the methodology in Section 3. Baselines. We compare against two oracle-free baselines. First, LLM-as-a-judge 20 uses an LLM to predict correctness from the specification and implementation. We evaluate four judges and aggregate predictions at the specification level. Second, simulation-based consensus clusters implementations by agreement under generated testbenches 19. Metrics. We report precision (correct accepts / total accepts) and coverage (accepts / evaluable specs) at the specification level, with 95% Wilson confidence intervals 16. When reported, false positive (FP) rate normalizes false positives by the total number of incorrect specifications, recall by the total number of correct ones, and accuracy is the fraction of predictions matching ground truth. Statistical significance is assessed using Fisherās exact test when comparing high- and low-consensus groups. 4.2. Why Formal Consensus? We quantify the instability of LLM-as-a-judge- and testbench-dependent oracle-free baselines: 4.2.1. LLM-as-a-Judge Ablation We evaluate LLM-as-a-judge as a correctness proxy using four judge models: Gemini 2.5 Flash 4, GPT-OSS-120B 9, Claude 3.7 Sonnet 3, and Qwen 3 Coder 1. Table 1. Cross-judge ablation on CVDP. Results measured at completion level. Bold denotes best per column. Judge Gen. model FPR (%) Rec (%) Prec (%) Acc (%) Gemini 2.5 Flash Claude 19.1 61.8 82.8 69.5 Gemini 43.4 68.3 68.0 63.3 GPT 47.9 78.3 68.8 67.2 Qwen 10.5 49.5 85.7 67.2 Overall 29.4 64.0 74.7 66.8 Claude 3.7 Sonnet Claude 3.2 11.6 84.4 45.9 Gemini 5.4 18.8 82.4 51.0 GPT 3.6 18.0 87.2 51.4 Qwen 1.2 7.8 89.5 47.9 Overall 3.3 13.9 85.1 49.0 GPT-OSS-120B Claude 11.5 65.2 89.4 74.6 Gemini 26.5 63.4 76.3 67.7 GPT 37.1 75.1 73.2 69.9 Qwen 8.1 39.9 86.1 62.8 Overall 20.2 60.5 80.3 68.7 Qwen 3 Coder Claude 0.0 5.2 100.0 43.3 Gemini 2.4 5.8 76.5 44.9 GPT 2.1 11.1 87.5 48.0 Qwen 0.0 3.2 100.0 45.9 Overall 1.1 6.1 88.3 45.4 Although ground-truth pass rates are similar across generating models (55.9ā59.7%), judge acceptance varies substantially with the code generator: Gemini and GPT each exhibit a 33-point spread across generators (Figure 2). The cross-judge ablation in Table 1 shows that this instability persists across judges: higher-recall judges incur substantial false-positive rates, while conservative judges reduce false positives primarily by abstaining. Thus, LLM-as-a-judge does not provide a stable high-confidence triage signal. 4.2.2. Simulation-Based Clustering is Testbench-Dependent To isolate the effect of the equivalence mechanism, we hold the RTL candidate pool fixed and vary only the generated testbench used for clustering. On the same candidate pool, simulation-based precision at model count (mc)ā„ 4 varies from 43% with Claude-generated testbenches to 84% with Gemini- and GPT-generated testbenches, while formal SEC reaches 94.7% (Figure 3). Simulation agreement is therefore partly a property of the generated testbench, not only of the RTL candidates. The following failure modes emerged as part of our analysis: For the 64b/66b encoder task (specification ID 5), Claude-generated tests place four CVDP-failing candidates and sixteen passing candidates in the same mc=4 cluster because the stimulus does not exercise the distinguishing behavior. On specification ID 122, a GPT-generated testbench deadlocks after reset and produces no clusters despite all candidates compiling. SEC merges candidates only under proven equivalence and requires no stimulus, avoiding both failure modes. Together, these results motivate formal consensus as the confidence signal. Judge-based and simulation-based agreement are properties of the evaluator and testbench, respectively, rather than of the RTL candidates. NoTB instead defines agreement through SEC, so cross-model consensus reflects the designs themselves. 4.3. NoTB Performance 4.3.1. Triage Performance We evaluate whether cross-model agreement under formal equivalence predicts functional correctness. For each specification, we measure the model diversity of the largest equivalence cluster and analyze how this signal relates to correctness. Figure 3 and Table 2 summarize the result. Table 2. Selective prediction as a function of model count. Each row defines a decision rule: accept specifications whose largest cluster contains at least the indicated number of model families. Threshold Acc. Corr. FP Precision 95% CI Coverage ā„4ā„ 4 19 18 1 95% [0.75, 0.99] 27% ā„3ā„ 3 23 20 3 87% [0.68, 0.95] 33% ā„2ā„ 2 34 29 5 85% [0.70, 0.94] 49% All 70 44 26 63% [0.51, 0.73] 100% As shown in Table 2, correctness improves with model count (mācmc). At the lowest threshold, mcā„1ā„ 1, precision is 63%, reflecting the baseline difficulty of the benchmark. Increasing the threshold to mcā„2ā„ 2 and mcā„3ā„ 3 raises precision to 85.3% and 87%, respectively. At full four-family agreement, mcā„4ā„ 4, precision reaches 94.7%. This trend shows that model diversity within the dominant SEC cluster provides a calibrated correctness signal: stronger formal cross-model agreement corresponds to lower empirical error risk. SEC turns agreement into a property of the RTL implementations, rather than of a finite testbench. NoTB therefore prioritizes high-consensus clusters while leaving lower-consensus cases in the standard validation flow. The mcā„4ā„ 4 regime is the highest-precision operating point, accepting 19 specifications at 94.7% precision and 27% coverage. The mcā„3ā„ 3 regime is a broader operating point: it increases coverage to 33% while maintaining 87% precision. This behavior is well aligned with early-stage RTL triage, where the goal is not to classify every generated implementation, but to identify the subset of specifications whose dominant behavior has enough formal cross-model support to advance with lower false-acceptance risk. The separation between high-consensus (mcā„4ā„ 4) and low-consensus (mc<4<4) regimes is statistically significant. Their comparison yields p=4.4Ć10ā4p=4.4Ć 10^-4 under Fisherās exact test. Taken together, these results show that formal cross-model agreement provides a reliable and calibrated basis for early-stage RTL triage. 4.3.2. Model Family Sensitivity To assess whether any single model family is load-bearing for the consensus signal, we re-cluster each specification using only three of the four model families, dropping all five completions from the omitted family. Table 3 reports precision and coverage at each model-count threshold for each leave-one-out setting. Table 3. Leave-one-out ablation. Each row drops one model family (5 completions) and re-clusters the remaining 3 families. mcā„ 3 means all models agree. Dropped mcā„ 3 mcā„ 2 mcā„ 1 model Prec Cov Prec Cov Prec Cov Claude 90% 29% 82% 40% 63% 100% Gemini 95% 27% 83% 43% 63% 100% GPT 95% 27% 89% 40% 63% 100% Qwen 100% 29% 81% 46% 63% 100% Dropping Qwen leaves mcā„3ā„ 3 precision at 100%. Dropping Claude reduces mcā„3ā„ 3 precision to 90%, indicating that Claude completions provide useful discriminative coverage. Importantly, high-precision triage remains possible in every leave-one-out setting. NoTBās confidence signal therefore does not depend on access to any particular model family, making the method portable across deployment settings with different model availability. 4.3.3. Completions per Model We vary the number of completions (generated RTL samples) per model family, Kā1,2,3,4,5Kā\1,2,3,4,5\, and recompute model count using the corresponding formal-equivalence clusters (Figure 4). Figure 4. Precision and coverage at each model-count threshold as K varies from 1 to 5. At mcā„4ā„ 4, precision remains above 93% across the sweep, while coverage increases from 14% at K=1K=1 to 27% at K=5K=5. Gains diminish beyond K=3K=3, suggesting that a modest number of samples per family captures most high-confidence cases. 4.3.4. Cost Analysis Table 4. NoTB pipeline cost vs. baseline costs. All costs computed from measured per-call token rates at current OpenRouter list pricing. Stage Component Calls Cost Generation Claude 3.7 Sonnet 390 $12.29 Gemini 2.5 Flash 390 $1.88 Qwen 3 Coder 390 $0.59 GPT-OSS-120B 380 $0.17 TB Gen. Claude 3.7 Sonnet 77 TBs $10.52 Gemini 2.5 Flash 78 TBs $3.64 GPT-OSS-120B 78 TBs $0.00 Judge Claude 3.7 Sonnet 1,556 $27.99 Gemini 2.5 Flash 1,556 $27.89 Qwen 3 Coder 1,556 $5.00 GPT-OSS-120B 1,556 $0.00 SEC JasperGold 13,133 pairs license We quantify the monetary and computational cost of NoTB across all 78 specifications. Table 4 summarizes candidate generation, judge-based evaluation, and formal equivalence. Figure 5. SEC pairs per specification: theoretical worst case (4āK2) 4K2 versus actual count after hash deduplication and transitivity pruning. Error bars show standard deviation across specifications. Figure 6. Median wall-clock time per specification as K varies. The shaded region shows the 25thā75th percentile. Candidate generation is shared by all evaluated methods. Generating 20 implementations per specification across four model families costs $14.93 over the full dataset. NoTB then performs triage using local SEC checks. It does not require additional judge calls or generated testbenches to construct its confidence signal. In contrast, the LLM-as-a-judge baseline requires 1,556 additional model calls in our evaluation. Without pruning, comparing all candidate pairs would require up to (202)=190 202=190 SEC invocations per specification. Hash-based deduplication and transitivity pruning reduce this by roughly 32% on average, though savings vary across specifications (Figure 5). Across the dataset, the majority of SEC calls yield definitive equivalent or non-equivalent verdicts, with the remainder terminating during elaboration or returning inconclusive. Only proven equivalences contribute to clusters, so inconclusive results reduce coverage but cannot introduce false merges. Median wall-time per specification grows from 1 minute at K=1K=1 to 16 minutes at K=5K=5 (Figure 6). SEC calls are independent across pairs and specifications, so the pipeline is parallelizable. Overall, NoTB trades the per-call LLM spend of judge- and testbench-based baselines for local SEC compute that parallelizes across pairs; the baselinesā costs scale linearly with candidates and specifications, while NoTBās reduce to wall-clock on existing verification hardware. 5. Conclusion NoTB is an oracle-free triage framework for LLM-generated RTL that replaces testbench- and judge-based agreement with formal cross-model consensus. Our approach leverages Sequential Equivalence Checking to cluster candidate implementations using behavioral agreement over the full input space, and scores each cluster by the number of distinct LLM families represented in it. NoTB outperforms existing oracle-free baselines by achieving up to 94.7% precision at 27% coverage on 78 CVDP RTL-generation tasks across four LLM families. Acknowledgements. This work was supported in part by Amazon.com, Inc. References Cao et al. (2026) R. Cao, M. Chen, J. Chen, Z. Cui, Y. Feng, B. Hui, Y. Jing, K. Li, M. Li, J. Lin, Z. Ma, K. Shum, X. Wang, J. Wei, J. Yang, J. Zhang, L. Zhang, Z. Zhang, W. Zhao, and F. Zhou Qwen3-coder-next technical report. arXiv preprint arXiv:2603.00729. Cited by: Ā§4.1, Ā§4.2.1. Chen et al. (2023) B. Chen, F. Zhang, A. Nguyen, D. Zan, Z. Lin, J. Lou, and W. Chen CodeT: code generation with generated tests. In The Eleventh International Conference on Learning Representations (ICLR), Cited by: Ā§1. [3] Claude 3.7 sonnet system card. External Links: Link Cited by: Ā§4.1, Ā§4.2.1. Comanici et al. (2025) G. Comanici, E. Bieber, M. Schaekermann, I. Pasupat, N. Sachdeva, I. Dhillon, M. Blistein, O. Ram, D. Zhang, E. Rosen, L. Marris, S. Petulla, C. Gaffney, A. Aharoni, N. Lintz, T. C. Pais, H. Jacobsson, I. Szpektor, N. Jiang, K. Haridasan, A. Omran, N. Saunshi, D. Bahri, G. Mishra, E. Chu, T. Boyd, B. Hekman, A. Parisi, C. Zhang, K. Kawintiranon, T. Bedrax-Weiss, O. Wang, Y. Xu, O. Purkiss, U. Mendlovic, I. Deutel, N. Nguyen, A. Langley, F. Korn, L. Rossazza, A. RamĆ©, S. Waghmare, H. Miller, N. Byrd, A. Sheshan, R. Hadsell, S. Bhardwaj, P. Janus, T. Rissa, D. Horgan, A. Abdagic, L. Belenki, J. Allingham, A. Singh, T. Guidroz, S. Srinivasan, H. Schmit, K. Chiafullo, A. Elisseeff, N. Jha, P. Kolhar, L. Berrada, F. Ding, X. Si, S. B. Mallick, F. Och, S. Erell, E. Ni, T. Latkar, S. Yang, P. Sirkovic, Z. Feng, R. Leland, R. Hornung, G. Wu, C. Blundell, H. Alvari, P. Huang, C. Yip, S. Deur, L. Liu, G. Surita, P. Duque, D. Damen, J. Jia, A. Guez, M. Mircea, A. Sinha, A. Magni, P. Stradomski, T. Marian, V. GaliÄ, W. Chen, H. Husain, A. Singhal, D. Grewe, F. Aubet, S. Song, L. Blanco, L. Rechis, L. Ho, R. Munoz, K. Zheng, J. Hamrick, K. Mather, H. Taitelbaum, E. Rutherford, Y. Lei, K. Chen, A. Shukla, E. Moreira, E. Doi, B. Isik, N. Shabat, D. RogoziÅska, K. Kolipaka, J. Chang, E. VuÅ”ak, S. Venkatachary, S. Noghabi, T. Bharti, Y. Jun, A. Zaks, S. Green, J. Challagundla, W. Wong, M. Mohammad, D. Hirsch, Y. Cheng, I. Naim, L. Proleev, D. Vincent, A. Singh, M. Krikun, D. Krishnan, Z. Ghahramani, A. Atias, R. Aggarwal, C. Kirov, D. Vytiniotis, C. Koh, A. Chronopoulou, P. Dogra, V. Ion, G. Tyen, J. Lee, F. Weissenberger, T. Strohman, A. Balakrishna, J. Rae, M. Velic, R. de Liedekerke, O. Elyada, W. Yuan, C. Liu, L. Shani, S. Kishchenko, B. Alessio, Y. Li, R. Song, S. Kwei, O. Jankowski, A. Pappu, Y. Namiki, Y. Ma, N. Tripuraneni, C. Cherry, M. Ikonomidis, Y. Ling, C. Ji, B. Westberg, A. Wright, D. Yu, D. Parkinson, S. Ramaswamy, J. Connor, S. H. Yeganeh, S. Grover, G. Kenwright, L. Litchev, C. Apps, A. Tomala, F. Halim, A. Castro-Ros, Z. Li, A. Boral, P. Sho, M. Yarom, E. Malmi, D. Klinghoffer, R. Lin, A. Ansell, P. K. S, S. Zhao, S. Zuo, A. Santoro, H. Cheng, S. Demmessie, Y. Liu, N. Brichtova, A. Culp, N. Braun, D. Graur, W. Ng, N. Mehta, A. Phillips, P. Sundberg, V. Godbole, F. Liu, Y. Katariya, D. Rim, M. Seyedhosseini, S. Ammirati, J. Valfridsson, M. Malihi, T. Knight, A. Toor, T. Lampe, A. Ittycheriah, L. Chiang, C. Yeung, A. FrĆ©chette, J. Rao, H. Wang, H. Srivastava, R. Zhang, R. Rhodes, A. Brand, D. Weesner, I. Figotin, F. Gimeno, R. Fellinger, P. Marcenac, J. Leal, E. Marcus, V. Cotruta, R. Cabrera, S. Luo, D. Garrette, V. Axelrod, S. Baltateanu, D. Barker, D. Chen, H. Toma, B. Ingram, J. Riesa, C. Kulkarni, Y. Zhang, H. Liu, C. Wang, M. Polacek, W. Wu, K. Hui, A. N. Reyes, Y. Su, M. Barnes, I. Malhi, A. Siddiqui, Q. Feng, M. Damaschin, D. Pighin, A. Steiner, S. Yang, R. S. Boppana, S. Ivanov, A. Kandoor, A. Shah, A. Mujika, D. Huang, C. A. Choquette-Choo, M. Patel, T. Yu, T. Creswell, Jerry, Liu, C. Barros, Y. Razeghi, A. Roy, P. Culliton, B. Xiong, J. Pan, T. Strohmann, T. Powell, B. Seal, D. DeCarlo, P. Shyam, K. Katircioglu, X. Wang, C. Hardin, I. Odisho, J. Broder, O. Chang, A. Nair, A. Shtefan, M. OāBrien, M. Agarwal, S. Potluri, S. Goyal, A. Jhindal, S. Thakur, Y. Stuken, J. Lyon, K. Toutanova, F. Feng, A. Wu, B. Horn, A. Wang, A. Cullum, G. Taubman, D. Shrivastava, C. Shi, H. Tomlinson, R. Patel, T. Tu, A. M. Oflazer, F. Pongetti, M. Yang, A. A. TaĆÆga, V. Perot, N. W. Pierse, F. Han, Y. Drori, I. Iturrate, A. Chakrabarti, L. Yeung, D. Dopson, Y. Chen, A. Kulshreshtha, T. Guo, P. Pham, T. Schuster, J. Chen, A. Polozov, J. Xing, H. Zhou, P. Kacham, D. Kukliansky, A. Miech, S. Yaroshenko, E. Chi, S. Douglas, H. Fei, M. Blondel, P. Myla, L. Madmoni, X. Wu, D. Keysers, K. Kjems, I. Albuquerque, L. Yu, J. Dāsa, M. Plantan, V. Ionescu, J. S. Elias, A. Gupta, M. R. Vuyyuru, F. Alcober, T. Zhou, K. Ji, F. Hartmann, S. Puttagunta, H. Song, E. Amid, A. Stefanoiu, A. Lee, P. Pucciarelli, E. Wang, A. Raul, S. Petrov, I. Tian, V. Anklin, N. Nti, V. Gomes, M. Schumacher, G. Vesom, A. Panagopoulos, K. Bousmalis, D. Andor, J. Jacob, Y. Zhang, B. Rosgen, M. Kecman, M. Tung, A. Belias, N. Goodman, P. Covington, B. Wieder, N. Saxena, E. Davoodi, M. Huang, S. Maddineni, V. Roulet, F. Campbell-Ajala, P. G. Sessa, Xintian, Wu, G. Lai, P. Collins, A. Haig, V. Sakenas, X. Xu, M. Giustina, L. E. Shafey, P. Charoenpanit, S. Garg, J. Ainslie, B. Severson, M. G. Arenas, S. Pathak, S. Rajayogam, J. Feng, M. Bakker, S. Li, N. Wichers, J. Rogers, X. Geng, Y. Li, R. Jagerman, C. Jia, N. Olmert, D. Sharon, M. Mauger, S. Mariserla, H. Ma, M. Mohabey, K. Kim, A. Andreev, S. Pollom, J. Love, V. Jain, P. Agrawal, Y. Schroecker, A. Fortin, M. Warmuth, J. Liu, A. Leach, I. Blok, G. P. Girirajan, R. Aharoni, B. Uria, A. Sozanschi, D. Goldberg, L. Ionita, M. T. Ribeiro, M. Zlocha, V. Birodkar, S. Lachgar, L. Yuan, H. Choudhury, M. Ginsberg, F. Zheng, G. Dibb, E. Graves, S. Lokhande, G. Rasskin, G. Muraru, C. Quick, S. Tata, P. Sermanet, A. Chawla, I. Karo, Y. Wang, S. Zhang, O. Keller, A. Dragan, G. Su, I. Chou, X. Liu, Y. Tao, S. Prabhakara, M. Wilson, R. Liu, S. Wang, G. Evans, D. Du, A. CastaƱo, G. Prasad, M. E. Mahdy, S. Gerlach, M. Reid, J. Kahn, A. Zait, T. S. Pillai, T. Ulrich, G. Wang, J. Wassenberg, E. Farkash, K. Yalasangi, C. Wang, M. Bauza, S. Bucher, T. Liu, J. Yan, G. Leung, V. Sindhwani, P. Barnes, A. Singh, I. Jurin, J. Chang, N. K. Bhumihar, S. Eiger, G. Citovsky, B. Withbroe, Z. Li, S. Xue, N. D. Santo, G. Stoyanov, Y. Raimond, S. Zheng, Y. Gao, V. ListĆk, S. Kwasiborski, R. Saputro, A. Ozturel, G. Mallya, K. Majmundar, R. West, P. Caron, J. Wei, L. Castrejon, S. Vikram, D. Ramachandran, N. Dhawan, J. Park, S. Smoot, G. van den Driessche, Y. Blau, C. Malik, W. Liang, R. Hirsch, C. N. dos Santos, E. Weinstein, A. van den Oord, S. Lall, N. FitzGerald, Z. Jiang, X. Yang, D. Webster, A. Elqursh, A. Pope, G. Rotival, D. Raposo, W. Zhu, J. Dean, S. Alabed, D. Tran, A. Gupta, Z. Gleicher, J. Austin, E. Rosseel, M. Umekar, D. Das, Y. Sun, K. Chen, K. Misiunas, X. Zhou, Y. Di, A. Loo, J. Newlan, B. Li, V. Ramasesh, Y. Xu, A. Chen, S. Gandhe, R. Soricut, N. Gupta, S. Hu, S. El-Sayed, X. Garcia, I. Brusilovsky, P. Chen, A. Bolt, L. Huang, A. Gurney, Z. Zhang, A. Pritzel, J. Wilkiewicz, B. Seybold, B. K. Shamanna, F. Fischer, J. Dean, K. Gill, R. Mcilroy, A. Bhowmick, J. Selier, A. Yang, D. Cheng, V. Magay, J. Tan, D. Varma, C. Walder, T. Kocisky, R. Nakashima, P. Natsev, M. Kwong, I. Gog, C. Zhang, S. Dieleman, T. Jimma, A. Ryabtsev, S. Brahma, D. Steiner, D. Du, A. Žužul, M. ŽaniÄ, M. Raghavachari, W. Gierke, Z. Zheng, D. Petrova, Y. Dauphin, Y. Liu, I. Kessler, S. Hand, C. Duvarney, S. Kim, H. Lee, L. Hussenot, J. Hui, J. Smith, D. Jain, J. Xia, G. S. Tomar, K. Amiri, D. Phan, F. Fuchs, T. Weyand, N. Tomasev, A. Cordell, X. Liu, J. Mallinson, P. Joshi, A. Crawford, A. Suggala, S. Chien, N. Fernando, M. Sanchez-Vargas, D. Williams, P. Crone, X. Luo, I. Karpov, J. Shan, T. Thurk, R. Strudel, P. Voigtlaender, P. Patil, T. Dozat, A. Khodaei, S. Singla, P. Ambroszczyk, Q. Wu, Y. Chang, B. Roark, C. Hegde, T. Ding, A. Filos, Z. Wu, A. S. Pinto, S. Liu, S. Khanna, A. Pandey, S. Mcloughlin, Q. Li, S. Haves, A. Zhou, E. Buchatskaya, I. Leal, P. de Boursac, N. Akazawa, N. Anderson, T. Chen, K. Somandepalli, C. Liang, S. Goenka, S. Winkler, A. Grushetsky, Y. Ding, J. Smith, F. Ye, J. Pont-Tuset, E. Li, R. Li, T. Golany, D. Wegner, T. Jiang, O. Barak, Y. Shangguan, E. VĆ©rtes, R. Wong, J. Bornschein, A. Tudor, M. Bevilacqua, T. Schaul, A. S. Rawat, Y. Zhao, K. Axiotis, L. Meng, C. McLean, J. Lai, J. Beattie, N. Kushman, Y. Liu, B. Kutzman, F. Lang, J. Ye, P. Netrapalli, P. Mishra, M. Khan, M. Goel, R. Willoughby, D. Tian, H. Zhuang, J. Chen, Z. Tsai, T. Kementsietsidis, A. Khare, J. Keeling, K. Xu, N. Waters, F. AltchĆ©, A. Popat, B. Mittal, D. Saxton, D. E. Badawy, M. Mathieu, Z. Zheng, H. Zhou, N. Ranka, R. Shin, Q. Duan, T. Salimans, I. Mihailescu, U. Shaham, M. Chang, Y. Assael, N. Dikkala, M. Izzard, V. Cohen-Addad, C. Graves, V. Feinberg, G. Chung, D. Strouse, D. Karmon, S. Sharifzadeh, Z. Ashwood, K. Pham, J. Blanton, A. Vasiloff, J. Barber, M. Geller, A. Zhou, F. Zubach, T. Huang, L. Zhang, H. Gupta, M. Young, J. Proskurnia, R. Votel, V. Gabeur, G. Barcik, A. Tripathi, H. Yu, G. Yan, B. Changpinyo, F. PavetiÄ, A. Coyle, Y. Fujii, J. G. Mendez, T. Zhou, H. Rajamani, B. Hechtman, E. Cao, D. Juan, Y. Tan, V. Dalibard, Y. Du, N. Clay, K. Yao, W. Jia, D. Vijaykumar, Y. Zhou, X. Bai, W. Hung, S. Pecht, G. Todorov, N. Khadke, P. Gupta, P. Lahoti, A. Autef, K. Duddu, J. Lee-Thorp, A. Bykovsky, T. Misiunas, S. Flennerhag, S. Thangaraj, J. McGiffin, Z. Nado, M. Kunesch, A. Noever, A. Hertz, M. Liang, V. Stone, E. Palmer, S. Daruki, A. Pramanik, S. PƵder, A. Kyker, M. Khan, E. Sluzhaev, M. Ritter, A. Ruderman, W. Zhou, C. Nagpal, K. Vodrahalli, G. Necula, P. Barham, E. Pavlick, J. Hartford, I. Shafran, L. Zhao, M. MikuÅa, T. Eccles, H. Shimokawa, K. Garg, L. Vilnis, H. Chen, I. Shumailov, K. Lee, A. Abdelhamed, M. Xie, V. Cohen, E. Hlavnova, D. Malkin, C. Sitawarin, J. Lottes, P. Coquinot, T. Yu, S. Kumar, J. Zhang, A. Mahendru, Z. Ahmed, J. Martens, T. Chen, A. Boag, D. Peng, C. Devin, A. Klimovskiy, M. Phuong, D. Vainstein, J. Xie, B. Ramabhadran, N. Howard, X. Yu, G. Goswami, J. Cui, S. Shleifer, M. Pinto, C. Yeh, M. Yang, S. Javanmardi, D. Ethier, C. Lee, J. Orbay, S. Kotecha, C. Bromberg, P. Shaw, J. Thornton, A. G. Rosenthal, S. Gu, M. Thomas, I. Gemp, A. Ayyar, A. Ushio, A. Selvan, J. Wee, C. Liu, M. Majzoubi, W. Yu, J. Abernethy, T. Liechty, R. Pan, H. Nguyen, Qiong, Hu, S. Perrin, A. Arora, E. Pitler, W. Wang, K. Shivakumar, F. Prost, B. Limonchik, J. Wang, Y. Gao, T. Cour, S. Buch, H. Gui, M. Ivanova, P. Neubeck, K. Chan, L. Kim, H. Chen, N. Goyal, D. Chung, L. Liu, Y. Su, A. Petrushkina, J. Shen, A. Joulin, Y. Xu, S. X. Lin, Y. Kulizhskaya, C. Chelba, S. Vasudevan, E. Collins, V. Bashlovkina, T. Lu, D. Fritz, J. Park, Y. Zhou, C. Su, R. Tanburn, M. Sushkov, M. Rasquinha, J. Li, J. Prendki, Y. Li, P. LV, S. Sharma, H. Fitoussi, H. Huang, A. Dai, P. Dao, M. Burrows, H. Prior, D. Qin, G. Pundak, L. L. Sjoesund, A. Khurshudov, Z. Zhu, A. Webson, E. Kemp, T. Tan, S. Agrawal, S. Sargsyan, L. Cheng, J. Stephan, T. Kwiatkowski, D. Reid, A. Byravan, A. H. Michaely, N. Heess, L. Zhou, S. Goenka, V. Carpenter, A. Levskaya, B. Wang, R. Roberts, R. Leblond, S. Chikkerur, S. Ginzburg, M. Chang, R. Riachi, Chuqiao, Xu, Z. Borsos, M. Pliskin, J. Pawar, M. Lustman, H. Kirkwood, A. Anand, A. Chaudhary, N. Kalb, K. Milan, S. Augenstein, A. Goldie, L. Prince, K. Raman, Y. Sun, V. Xia, A. Cohen, Z. Huo, J. Camp, S. Ellis, L. Zilka, D. V. Torres, L. Patel, S. Arora, B. Chan, J. Adler, K. Ayoub, J. Liang, F. Jamil, J. Jiang, S. Baumgartner, H. Sun, Y. Karov, Y. Akulov, H. Zheng, I. Cai, C. Fantacci, J. Rubin, A. R. Acha, M. Wang, N. DāSouza, R. Sathyanarayana, S. Dai, S. Rowe, A. Simanovsky, O. Goldman, Y. Kuang, X. Pan, A. Rosenberg, T. Rojas-Esponda, P. Dutta, A. Zeng, I. Jurenka, G. Farquhar, Y. Bansal, S. Iqbal, B. Roelofs, G. Joung, P. Beak, C. Ryu, R. Poplin, Y. Wu, J. Alayrac, S. Buthpitiya, O. Ronneberger, C. Habtegebriel, W. Li, P. Cavallaro, A. Wei, G. Bensky, T. Denk, H. Ganapathy, J. Stanway, P. Joshi, F. Bertolini, J. Lo, O. Ma, Z. Charles, G. Sampemane, H. Sahni, X. Chen, H. Askham, D. Gaddy, P. Young, J. Tan, M. Eyal, A. Bražinskas, L. Zhong, Z. Wu, M. Epstein, K. Bailey, A. Hard, K. Lee, S. Goldshtein, A. Ruiz, M. Badawi, M. Lochbrunner, J. Kearns, A. Brown, F. Pardo, T. Weber, H. Yang, P. Jiang, B. Akin, Z. Fu, M. Wainwright, C. Zou, M. Gaba, P. Manzagol, W. Kan, Y. Song, K. Zainullina, R. Lin, J. Ko, S. Deshmukh, A. Jindal, J. Svensson, D. Tyam, H. Zhao, C. Kaeser-Chen, S. Baird, P. Moradi, J. Hall, Q. Guo, V. Tsang, B. Liang, F. Pereira, S. Ganesh, I. Korotkov, J. Adamek, S. Thiagarajan, V. Tran, C. Chen, C. Tar, S. Jain, I. Dasgupta, T. Bilal, D. Reitter, K. Zhao, G. Vezzani, Y. Gehman, P. Mehta, L. Beltrone, X. Dotiwalla, S. Guadarrama, Z. Abbas, S. Karp, P. Georgiev, C. Ferng, M. Brockschmidt, L. Peng, C. Hirnschall, V. Verma, Y. Bi, Y. Xiao, A. Dabush, K. Xu, P. Wallis, R. Parker, Q. Wang, Y. Xu, I. Safarli, D. Tewari, Y. Zhang, S. Kim, A. Gesmundo, M. Thomas, S. Levi, A. Chowdhury, K. Rao, P. Garst, S. Conway-Rahman, H. Ran, K. McKinney, Z. Xiao, W. Yu, R. Agrawal, A. Stjerngren, C. Ionescu, J. Chen, V. Sharma, J. Chiu, F. Liu, K. Franko, C. Sanford, X. Cai, P. Michel, S. Ganapathy, J. Labanowski, Z. Garrett, B. Vargas, S. Sun, B. Gale, T. Buschmann, G. Desjardins, N. Ghelani, P. Jain, M. Verma, C. Asawaroengchai, J. Eisenschlos, J. Harlalka, H. Kazawa, D. Metzler, J. Howland, Y. Jian, J. Ades, V. Shah, T. Gangwani, S. Lee, R. Ring, S. M. Hernandez, D. Reich, A. Sinha, A. Sathe, J. Kovac, A. Gill, A. Kannan, A. Dāolimpio, M. Sevenich, J. Whang, B. Kim, K. C. Sim, J. Chen, J. Zhang, S. Lall, Y. Matias, B. Jia, A. Friesen, S. Nasso, A. Thapliyal, B. Perozzi, T. Yu, A. Shekhawat, S. Huda, P. Grabowski, E. Wang, A. Sreevatsa, H. Dib, M. Hassen, P. Schuh, V. Milutinovic, C. Welty, M. Quinn, A. Shah, B. Wang, G. Barth-Maron, J. Frye, N. Axelsson, T. Zhu, Y. Ma, I. Giannoumis, H. Sedghi, C. Ye, Y. Luan, K. Aydin, B. Chandra, V. Sampathkumar, R. Huang, V. Lavrenko, A. Eleryan, Z. Hong, S. Hansen, S. M. Carthy, B. Samanta, D. Äevid, X. Wang, F. Li, M. Voznesensky, M. Hoffman, A. Terzis, V. Sehwag, G. Fidel, L. He, M. Cai, Y. He, A. Feng, M. Nikoltchev, S. Phatale, J. Chase, R. Lawton, M. Zhang, T. Ouyang, M. Tragut, M. H. Manshadi, A. Narayanan, J. Shen, X. Gao, T. Bolukbasi, N. Roy, X. Li, D. Golovin, L. Panait, Z. Qin, G. Han, T. Anthony, S. Kudugunta, V. Patraucean, A. Ray, X. Chen, X. Yang, T. Bhatia, P. Talluri, A. Morris, A. RažnatoviÄ, B. Brownfield, J. An, S. Peng, P. Kane, C. Zheng, N. Duduta, J. Kessinger, J. Noraky, S. Liu, K. Rong, P. VeliÄkoviÄ, K. Rush, A. Goldin, F. Wei, S. M. R. Garlapati, C. Pantofaru, O. Kwon, J. Ni, E. Noland, J. D. Trapani, F. Beaufays, A. G. Roy, Y. Chow, A. Turker, G. Cideron, L. Mei, J. Clark, Q. Dou, M. BoÅ”njak, R. Leith, Y. Du, A. Yazdanbakhsh, M. Nasr, C. Kwak, S. S. Sheth, A. Kaskasoli, A. Anand, B. Lakshminarayanan, S. Jerome, D. Bieber, C. Chu, A. Senges, T. Shen, M. Sridhar, N. Ndebele, B. Beyret, S. Mohamed, M. Chen, M. Freitag, J. Guo, L. Liu, P. Roit, H. Chen, S. Yan, T. Stone, J. Co-Reyes, J. Cole, S. Scellato, S. Azizi, H. Hashemi, A. Jin, A. Iyer, M. Valentine, A. Gyƶrgy, A. Ahuja, D. H. Diaz, C. Lee, N. Clement, W. Kong, D. Garmon, I. Watts, K. Bhatia, K. Gupta, M. Miecnikowski, H. Vallet, A. Taly, E. Loper, S. Joshi, J. Atwood, J. Chick, M. Collier, F. Iliopoulos, R. Trostle, B. Gunel, R. Leal-Cavazos, A. M. Hrafnkelsson, M. Guzman, X. Ju, A. Forbes, J. Emond, K. Chauhan, B. Caine, L. Xiao, W. Zeng, A. Moufarek, D. Murphy, M. Meng, N. Gupta, F. Riedel, A. Das, E. Lawal, S. Narayan, T. Sosea, J. Swirhun, L. Friso, B. Neyshabur, J. Lu, S. Girgin, M. Wunder, E. Yvinec, A. Pyne, V. Carbune, S. Rijhwani, Y. Guo, T. Doshi, A. Briukhov, M. Bain, A. Hitron, X. Wang, A. Gupta, K. Chen, C. Du, W. Zhang, D. Shah, A. Akula, M. Dylla, A. Kachra, W. Kuo, T. Zou, L. Wang, L. Xu, J. Zhu, J. Snyder, S. Menon, O. Firat, I. Mordatch, Y. Yuan, N. Ponomareva, R. Blevins, L. Moore, W. Wang, P. Chen, M. Scholz, A. Dwornik, J. Lin, S. Li, D. Antognini, T. I, X. Song, M. Miller, U. Kalra, A. Raveret, O. Akerlund, F. Wu, A. Nystrom, N. Godbole, T. Liu, H. DeBalsi, J. Zhao, B. Liu, A. Caciularu, L. Lax, U. Khandelwal, V. Langston, E. Bailey, S. Lattanzi, Y. Wang, N. Kovelamudi, S. Mondal, G. Guruganesh, N. Hua, O. Roval, P. WesoÅowski, R. Ingale, J. Halcrow, T. Sohn, C. Angermueller, B. Raad, E. Stickgold, E. Lu, A. Kosik, J. Xie, T. Lillicrap, A. Huang, L. L. Zhang, D. Paulus, C. Farabet, A. Wertheim, B. Wang, R. Joshi, C. Ko, Y. Wu, S. Agrawal, L. Lin, X. Sheng, P. Sung, T. Breland-King, C. Butterfield, S. Gawde, S. Singh, Q. Zhang, R. Apte, S. Shetty, A. Hutter, T. Li, E. Salesky, F. Lebron, J. Kanerva, M. Paganini, A. Nguyen, R. Vallu, J. Peter, S. Velury, D. Kao, J. Hoover, A. Bortsova, C. Bishop, S. Jakobovits, A. Agostini, A. Agarwal, C. Liu, C. Kwong, S. Tavakkol, I. Bica, A. Greve, A. GP, J. Marcus, L. Hou, T. Duerig, R. Moroshko, D. Lacey, A. Davis, J. Amelot, G. Wang, F. Kim, T. Strinopoulos, H. Wan, C. L. Lan, S. Krishnan, H. Tang, P. Humphreys, J. Bai, I. H. Shtacher, D. Machado, C. Pang, K. Burke, D. Liu, R. Aravamudhan, Y. Song, E. Hirst, A. Singh, B. Jou, L. Bai, F. Piccinno, C. K. Fu, R. Alazard, B. Meiri, D. Winter, C. Chen, M. Zhang, J. Heitkaemper, J. Lambert, J. Lee, A. Frƶmmgen, S. Rogulenko, P. Nair, P. Niemczyk, A. Bulyenov, B. Xu, H. Shemtov, M. Zadimoghaddam, S. Toropov, M. Wirth, H. Dai, S. Gollapudi, D. Zheng, A. Kurakin, C. Lee, K. Bullard, N. Serrano, I. Balazevic, Y. Li, J. Schalkwyk, M. Murphy, M. Zhang, K. Sequeira, R. Datta, N. Agrawal, C. Sutton, N. Attaluri, M. Chiang, W. Farhan, G. Thornton, K. Lin, T. Choma, H. Nguyen, K. Dasgupta, D. Robinson, I. ComÅa, M. Riley, A. Pillai, B. Mustafa, B. Golan, A. Zandieh, J. Lespiau, B. Porter, D. Ross, S. Rajayogam, M. Agarwal, S. Venugopalan, B. Shahriari, Q. Yan, H. Xu, T. Tobin, P. Dubov, H. Shi, A. Recasens, A. Kovsharov, S. Borgeaud, L. Dery, S. Vasanth, E. Gribovskaya, L. Qiu, M. Mahdieh, W. Skut, E. Nielsen, C. Zheng, A. Yu, C. G. Bostock, S. Gupta, A. Archer, C. Rawles, E. Davies, A. Svyatkovskiy, T. Tsai, Y. Halpern, C. Reisswig, B. Wydrowski, B. Chang, J. Puigcerver, M. H. Taege, J. Li, E. Schnider, X. Li, D. Dena, Y. Xu, U. Telang, T. Shi, H. Zen, K. Kastner, Y. Ko, N. Subramaniam, A. Kumar, P. Blois, Z. Dai, J. Wieting, Y. Lu, Y. Zeldes, T. Xie, A. Hauth, A. Å¢ifrea, Y. Li, S. El-Husseini, D. Abolafia, H. Zhou, W. Ding, S. Ghalebikesabi, C. GuĆa, A. Maksai, Ć. Weisz, S. Arik, N. Sukhanov, A. Åwietlik, X. Jia, L. Yu, W. Wang, M. Brand, D. Bloxwich, S. Kirmani, Z. Chen, A. Go, P. Sprechmann, N. Kannen, A. Carin, P. Sandhu, I. Edkins, L. Nooteboom, J. Gupta, L. Maggiore, J. Azizi, Y. Pritch, P. Yin, M. Gupta, D. Tarlow, D. Smith, D. Ivanov, M. Babaeizadeh, A. Goel, S. Kambala, G. Chu, M. Kastelic, M. Liu, H. Soltau, A. Stone, S. Agrawal, M. Kim, K. Soparkar, S. Tadepalli, O. Bunyan, R. Soh, A. Kannan, D. Kim, B. J. Chen, A. Halumi, S. Roy, Y. Wang, O. Sercinoglu, G. Gibson, S. Bhatnagar, M. Sano, D. von Dincklage, Q. Ren, B. Mitrevski, M. OlÅ”Ć”k, J. She, C. Doersch, Jilei, Wang, B. Liu, Q. Tan, T. Yakar, T. Warkentin, A. Ramirez, C. Lebsack, J. Dillon, R. Mathews, T. Cobley, Z. Wu, Z. Chen, J. Simon, S. Nath, T. Sainath, A. Bendebury, R. Julian, B. Mankalale, D. Äurko, P. Zacchello, A. R. Brown, K. Sodhia, H. Howard, S. Caelles, A. Gupta, G. Evans, A. Bulanova, L. Katzen, R. Goldenberg, A. Tsitsulin, J. Stanton, B. Schillings, V. Kovalev, C. Fry, R. Shah, K. Lin, S. Upadhyay, C. Li, S. Radpour, M. Maggioni, J. Xiong, L. Haas, J. Brennan, A. Kamath, N. Savinov, A. Nagrani, T. Yacovone, R. Kappedal, K. Andriopoulos, L. Lao, Y. Li, G. Rozhdestvenskiy, K. Hashimoto, A. Audibert, S. Austin, D. Rodriguez, A. Ruoss, G. Honke, D. Karkhanis, X. Xiong, Q. Wei, J. Huang, Z. Leng, V. Premachandran, S. Bileschi, G. Evangelopoulos, T. Mensink, J. Pavagadhi, D. Teplyashin, P. Chang, L. Xue, G. Tanzer, S. Goldman, K. Patel, S. Li, J. Wiesner, I. Zheng, I. Stewart-Binks, J. Han, Z. Li, L. Luo, K. Lenc, M. LuÄiÄ, F. Xue, R. Mullins, A. Guseynov, C. Chang, I. Galatzer-Levy, A. Zhang, G. Bingham, G. Hu, A. Hartman, Y. Ma, J. Griffith, A. Irpan, C. Radebaugh, S. Yue, L. Fan, V. Ungureanu, C. Sorokin, H. Teufel, P. Li, R. Anil, D. Paparas, T. Wang, C. Lin, H. Peng, M. Shum, G. Petrovic, D. Brady, R. Nguyen, K. Macherey, Z. Li, H. Singh, M. Yenugula, M. Iinuma, X. Chen, K. Kopparapu, A. Stern, S. Dave, C. Thekkath, F. Perot, A. Kumar, F. Li, Y. Xiao, M. Bilotti, M. H. Bateni, I. Noble, L. Lee, A. VĆ”zquez-Reina, J. Salazar, X. Yang, B. Wang, E. Gruzewska, A. Rao, S. Raghuram, Z. Xu, E. Ben-David, J. Mei, S. Dalmia, Z. Zhang, Y. Liu, G. Bansal, H. Pankov, S. Schwarcz, A. Burns, C. Chan, S. Sanghai, R. Liang, E. Liang, A. He, A. Stuart, A. Narayanan, Y. Zhu, C. Frank, B. Fatemi, A. Sabne, O. Lang, I. Bhattacharya, S. Settle, M. Wang, B. McMahan, A. Tacchetti, L. B. Soares, M. Hadian, S. Cabi, T. Chung, N. Putikhin, G. Li, J. Chen, A. Tarango, H. Michalewski, M. Kazemi, H. Masoom, H. Sheftel, R. Shivanna, A. Vadali, R. Comanescu, D. Reid, J. Moore, A. Neelakantan, M. Sander, J. Herzig, A. Rosenberg, M. Dehghani, J. Choi, M. Fink, R. Hayes, E. Ge, S. Weng, C. Ho, J. Karro, K. Krishna, L. N. Thiet, A. Skerry-Ryan, D. Eppens, M. Andreetto, N. Sarma, S. Bonacina, B. K. Ayan, M. Nawhal, Z. Shan, M. Dusenberry, S. Thakoor, S. Gubbi, D. D. Nguyen, R. Tsarfaty, S. Albanie, J. MitroviÄ, M. Gandhi, B. Chen, A. Epasto, G. Stephanov, Y. Jin, S. Gehman, A. Amini, J. Weber, F. Behbahani, S. Xu, M. Allamanis, X. Chen, M. Ott, C. Sha, M. Jastrzebski, H. Qi, D. Greene, X. Wu, A. Toki, D. Vlasic, J. Shapiro, R. Kotikalapudi, Z. Shen, T. Saeki, S. Xie, A. Cassirer, S. Bharadwaj, T. Kiyono, S. Bhojanapalli, E. Rosenfeld, S. Ritter, J. Mao, J. G. Oliveira, Z. Egyed, B. Bandemer, E. Parisotto, K. Kinoshita, J. Pluto, P. Maniatis, S. Li, Y. Guo, G. Ghiasi, J. Tarbouriech, S. Chatterjee, J. Jin, Katrina, Xu, J. Palomaki, S. Arnold, M. Sewak, F. Piccinini, M. Sharma, B. Albrecht, S. Purser-haskell, A. Vaswani, C. Chen, M. Wisniewski, Q. Cao, J. Aslanides, N. M. Phu, M. Sieb, L. Agubuzu, A. Zheng, D. Sohn, M. Selvi, A. Andreassen, K. Subudhi, P. Eruvbetine, O. Woodman, T. Mery, S. Krause, X. Ren, X. Ma, J. Luo, D. Chen, W. Fan, H. Griffiths, C. Schuler, A. Li, S. Zhang, J. Sarr, S. Luo, R. Patana, M. Watson, D. Naboulsi, M. Collins, S. Sidhwani, E. Hoogeboom, S. Silver, E. Caveness, X. Zhao, M. Rodriguez, M. Deines, L. Bai, P. Griffin, M. Tagliasacchi, E. Xue, S. R. Babbula, B. Pang, N. Ding, G. Shen, E. Peake, R. Crocker, S. S. Raghvendra, D. Swisher, W. Han, R. Singh, L. Wu, V. Pchelin, T. Munkhdalai, D. Alon, G. Bacon, E. Robles, J. Bulian, M. Johnson, G. Powell, F. T. Ferreira, Y. Li, F. Benzing, M. VelimiroviÄ, H. Soyer, W. Kong, Tony, NguyĆŖn, Z. Yang, J. Liu, J. van Amersfoort, D. Gillick, B. Sun, N. Rauschmayr, K. Zhang, S. Zhan, T. Zhou, A. Frolov, C. Yang, D. Vnukov, L. Rouillard, H. Li, A. Mandhane, N. Fallen, R. Venkataraman, C. H. Hu, J. Brennan, J. Lee, J. Chang, M. Sundermeyer, Z. Pan, R. Ke, S. Tong, A. Fabrikant, W. Bono, J. Gu, R. Foley, Y. Mao, M. Delakis, D. Bhaswar, R. Frostig, N. Li, A. Zipori, C. Hope, O. Kozlova, S. Mishra, J. Djolonga, C. Schiff, M. A. Merey, E. Briakou, P. Morgan, A. Wan, A. Hassidim, R. Skerry-Ryan, K. Sengupta, M. Jasarevic, P. Kallakuri, P. Kunkle, H. Brennan, T. Lieber, H. Mansoor, J. Walker, B. Zhang, A. Xie, G. ŽužiÄ, A. Chukwuka, A. Druinsky, D. Cho, R. Yao, F. Naeem, S. Butt, E. Kim, Z. Jia, M. Jordan, A. Lelkes, M. Kurzeja, S. Wang, J. Zhao, A. Over, A. Chakladar, M. Prasetya, N. Jha, S. Ganapathy, Y. Cong, P. Shroff, C. Saroufim, S. Miryoosefi, M. Hammad, T. Nasir, W. Xi, Y. Gao, Y. Maeng, B. Hora, C. Cheng, P. Haghani, Y. Lewenberg, C. Lu, M. Matysiak, N. Raisinghani, H. Wang, L. Baugher, R. Sukthankar, M. Giang, J. Schultz, N. Fiedel, M. Chen, C. Lee, T. Dey, H. Zheng, S. Paul, C. Smith, A. Ly, Y. Wang, R. Bansal, B. Perz, S. Ricco, S. Blank, V. Keshava, D. Sharma, M. Chow, K. Lad, K. Jalan, S. Osindero, C. Swanson, J. Scott, A. IliÄ, X. Li, S. R. Jonnalagadda, A. S. Soudagar, Y. Xiong, B. Batsaikhan, D. Jarrett, N. Kumar, M. Shah, M. Lawlor, A. Waters, M. Graham, R. May, S. Ramos, S. Lefdal, Z. Cankara, N. Cano, B. OāDonoghue, J. Borovik, F. Liu, J. Grimstad, M. Alnahlawi, K. Tsihlas, T. Hudson, N. Grigorev, Y. Jia, T. Huang, T. P. Igwe, S. Lebedev, X. Tang, I. Krivokon, F. Garcia, M. Tan, E. Jia, P. Stys, S. Vashishth, Y. Liang, B. Venkatraman, C. Gu, A. Kementsietsidis, C. Zhu, J. Jung, Y. Bai, M. J. Hosseini, F. Ahmed, A. Gupta, X. Yuan, S. Ashraf, S. Nigam, G. Vasudevan, P. Awasthi, A. M. Gilady, Z. Mariet, R. Eskander, H. Li, H. Hu, G. Garrido, P. Schlattner, G. Zhang, R. Saxena, P. DeviÄ, K. Muralidharan, A. Murthy, Y. Zhou, M. Choi, A. Wongpanich, Z. Wang, P. Shah, Y. Xu, Y. Huang, S. Spencer, A. Chen, J. Cohan, J. Wang, J. Tompson, J. Wu, R. Haroun, H. Li, B. Huergo, F. Yang, T. Yin, J. Wendt, M. Bendersky, R. Chaabouni, J. Snaider, J. Ferret, A. Jindal, T. Thompson, A. Xue, W. Bishop, S. M. Phal, A. Sharma, Y. Sung, P. Radhakrishnan, M. Shomrat, R. Ingle, R. Vij, J. Gilmer, M. D. Istin, S. Sobell, Y. Lu, E. Nottage, D. Sadigh, J. Willcock, T. Zhang, S. Xu, S. Brown, K. Lee, G. Wang, Y. Zhu, Y. Tay, C. Kim, A. Gutierrez, A. Sharma, Y. Xian, S. Seo, C. Cui, E. Pochernina, C. Baetu, K. JastrzÄbski, M. Ly, M. Elhawaty, D. Suh, E. Sezener, P. Wang, N. Yuen, G. Tucker, J. Cai, Z. Yang, C. Wang, A. Muzio, H. Qian, J. Yoo, D. Lockhart, K. R. McKee, M. Guo, M. Mehrotra, A. MendonƧa, S. V. Mehta, S. Ben, C. Tekur, J. Mu, M. Zhu, V. Krakovna, H. Lee, A. Maschinot, S. Cevey, H. Choe, A. Bai, H. Srinivasan, D. Gasaway, N. Young, P. Siegler, D. Holtmann-Rice, V. Piratla, K. Baumli, R. Yogev, A. Hofer, H. van Hasselt, S. Grant, Y. Chervonyi, D. Silver, A. Hogue, A. Agarwal, K. Wang, P. Singh, F. Flynn, J. Lipschultz, R. David, L. Bellot, Y. Yang, L. Le, F. Graziano, K. Olszewska, K. Hui, A. Maurya, N. Parotsidis, W. Chen, T. Oguntebi, J. Kelley, A. Baddepudi, J. Mauerer, G. Shaw, A. Siegman, L. Yang, S. Shetty, S. Roy, Y. Song, W. Stokowiec, R. Burnell, O. Savant, R. Busa-Fekete, J. Miao, S. Ghosh, L. MacDermed, P. Lippe, M. Dektiarev, Z. Behrman, F. Mentzer, K. Nguyen, M. Wei, S. Verma, C. Knutsen, S. Dasari, Z. Yan, P. Mitrichev, X. Wang, V. Shejwalkar, J. Austin, S. Sunkara, N. Potti, Y. Virin, C. Wright, G. Liu, O. Riva, E. Pot, G. Kochanski, Q. Le, G. Balasubramaniam, A. Dhar, Y. Liao, A. Bloniarz, D. Shukla, E. Cole, J. Lee, S. Zhang, S. Kafle, S. Vashishtha, P. Mahmoudieh, G. Chen, R. Hoffmann, P. Srinivasan, A. D. Lago, Y. B. Shalom, Z. Wang, M. Elabd, A. Sharma, J. Oh, S. Kothawade, M. Le, M. Monteiro, S. Yang, K. Alarakyia, R. Geirhos, D. Mincu, H. Garnes, H. Kobayashi, S. Mariooryad, K. Krasowiak, Zhixin, Lai, S. Mourad, M. Wang, F. Bu, O. Aharoni, G. Chen, A. Goyal, V. Zubov, A. Bapna, E. Dabir, N. Kothari, K. Lamerigts, N. D. Cao, J. Shar, C. Yew, N. Kulkarni, D. Mahaarachchi, M. Joshi, Z. Zhu, J. Lichtarge, Y. Zhou, H. Muckenhirn, V. Selo, O. Vinyals, P. Chen, A. Brohan, V. Mehta, S. Cogan, R. Wang, T. Geri, W. Ko, W. Chen, F. Viola, K. Shivam, L. Wang, M. C. Elish, R. A. Popa, S. Pereira, J. Liu, R. Koster, D. Kim, G. Zhang, S. Ebrahimi, P. Talukdar, Y. Zheng, P. Poklukar, A. Mikhalap, D. Johnson, A. Vijayakumar, M. Omernick, M. Dibb, A. Dubey, Q. Hu, A. Suman, V. Aggarwal, I. Kornakov, F. Xia, W. Lowe, A. Kolganov, T. Xiao, V. Nikolaev, S. Hemingray, B. Li, J. Iljazi, M. RybiÅski, B. Sandhu, P. Lu, T. Luong, R. Jenatton, V. Govindaraj, Hui, Li, G. Dulac-Arnold, W. Park, H. Wang, A. Modi, J. Pouget-Abadie, K. Greller, R. Gupta, R. Berry, P. Ramachandran, J. Xie, L. McCafferty, J. Wang, K. Gupta, H. Lim, B. BrataniÄ, A. Brock, I. Akolzin, J. Sproch, D. Karliner, D. Kim, A. Goedeckemeyer, N. Shazeer, C. Schmid, D. Calandriello, P. Bhatia, K. Choromanski, C. Montgomery, D. Dua, A. Ramalho, H. King, Y. Gao, L. Nguyen, D. Lindner, D. Pitta, O. Johnson, K. Salama, D. Ardila, M. Han, E. Farnese, S. Odoom, Z. Wang, X. Ding, N. Rink, R. Smith, H. T. Lehri, E. Cohen, N. Vats, T. He, P. Gopavarapu, A. Paszke, M. Patel, W. V. Gansbeke, L. Loher, L. Castro, M. Voitovich, T. von Glehn, N. George, S. Niklaus, Z. Eaton-Rosen, N. RakiÄeviÄ, E. Jue, S. Perel, C. Zhang, Y. Bahat, A. Pouget, Z. Xing, F. Huot, A. Shenoy, T. Bos, V. Coriou, B. Richter, N. Noy, Y. Wang, S. Ontanon, S. Qin, G. Makarchuk, D. Hassabis, Z. Li, M. Sharma, K. Venkatesan, I. Kemaev, R. Daniel, S. Huang, S. Shah, O. Ponce, Warren, Chen, M. Faruqui, J. Wu, S. AndaÄiÄ, S. Payrits, D. McDuff, T. Hume, Y. Cao, M. Tessler, Q. Wang, Y. Wang, I. Rendulic, E. Agustsson, M. Johnson, T. Lando, A. Howard, S. G. S. Padmanabhan, M. Daswani, A. Banino, M. Kilgore, J. Heek, Z. Ji, A. Caceres, C. Li, N. Kassner, A. Vlaskin, Z. Liu, A. Grills, Y. Hou, R. Sukkerd, G. Cheon, N. Shetty, L. Markeeva, P. Stanczyk, T. Iyer, Y. Gong, S. Gao, K. Gopalakrishnan, T. Blyth, M. Reynolds, A. Bhoopchand, M. Bilenko, D. Gharibian, V. Zayats, A. Faust, A. Singh, M. Ma, H. Jiao, S. Vijayanarasimhan, L. Aroyo, V. Yadav, S. Chakera, A. Kakarla, V. Meshram, K. Gregor, G. Botea, E. Senter, D. Jia, G. Kovacs, N. Sharma, S. Baur, K. Kang, Y. He, L. Zhuo, M. Kostelac, I. Laish, S. Peng, L. OāBryan, D. Kasenberg, G. R. Rao, E. Leurent, B. Zhang, S. Stevens, A. Salazar, Y. Zhang, I. Lobov, J. Walker, A. Porter, M. Redshaw, H. Ke, A. Rao, A. Lee, H. Lam, M. Moffitt, J. Kim, S. Qiao, T. Koo, R. Dadashi, X. Song, M. Sundararajan, P. Xu, C. Kawamoto, Y. Zhong, C. Barbu, A. Reddy, M. Verzetti, L. Li, G. Papamakarios, H. Klimczak-PluciÅska, M. Cassin, K. Kavukcuoglu, R. Swavely, A. Vaucher, J. Zhao, R. Hemsley, M. Tschannen, H. Ge, G. Menghani, Y. Yu, N. Ha, W. He, X. Wu, M. Song, R. Sterneck, S. Zinke, D. A. Calian, A. Marsden, A. C. Ruiz, M. Hessel, A. Gueta, B. Lee, B. Farris, M. Gupta, Y. Li, M. Saleh, V. Misra, K. Xiao, P. Mendolicchio, G. Buttimore, V. Krayvanova, N. Nayakanti, M. Wiethoff, Y. Pande, A. Mirhoseini, N. Lao, J. Liu, Y. Hua, A. Chen, Y. Malkov, D. Kalashnikov, S. Gupta, K. Audhkhasi, Y. Zhai, S. Kopalle, P. Jain, E. Ofek, C. Meyer, K. Baatarsukh, H. StrejÄek, J. Qian, J. Freedman, R. Figueira, M. Sokolik, O. Bachem, R. Lin, D. Kharrat, C. Hidey, P. Xu, D. Duan, Y. Li, M. Ersoy, R. Everett, K. Cen, R. Santamaria-Fernandez, A. Taubenfeld, I. Mackinnon, L. Deng, P. Zablotskaia, S. Viswanadha, S. Goel, D. Yates, Y. Deng, P. Choy, M. Chen, A. Sinha, A. Mossin, Y. Wang, A. Szlam, S. Hao, P. K. Rubenstein, M. Toksoz-Exley, M. Aperghis, Y. Zhong, J. Ahn, M. Isard, O. Lacombe, F. Luisier, C. Anastasiou, Y. Kalley, U. Prabhu, E. Dunleavy, S. Bijwadia, J. Mao-Jones, K. Chen, R. Pasumarthi, E. Wood, A. Dostmohamed, N. Hurley, J. Simsa, A. Parrish, M. Pajarskas, M. Harvey, O. Skopek, Y. Kochinski, J. Rey, V. Rieser, D. Zhou, S. J. Lee, T. Acharya, G. Li, J. Jiang, X. Zhang, B. Gipson, E. Mahintorabi, M. Gelmi, N. Khajehnouri, A. Yeh, K. Lee, L. Matthey, L. Baker, T. Pham, H. Fu, A. Pak, P. Gupta, C. Vasconcelos, A. Sadovsky, B. Walker, S. Hsiao, P. Zochbauer, A. Marzoca, N. Velan, J. Zeng, G. Baechler, D. Driess, D. Jain, Y. Huang, L. Tao, J. Maggs, N. Levine, J. Schneider, E. Gemzer, S. Petit, S. Han, Z. Fisher, D. Zelle, C. Biles, E. Ie, A. Fadeeva, C. Liu, J. V. Franco, A. Collister, H. Zhang, R. Wang, R. Zhao, L. Kieliger, K. Shuster, R. Zhu, B. Gong, L. Chan, R. Sun, S. Basu, R. Zimmermann, J. Hayes, A. Bapna, J. Snoek, W. Yang, P. Datta, J. A. Abdallah, K. Kilgour, L. Li, S. Mah, Y. Jun, M. RiviĆØre, A. Karmarkar, T. Spalink, T. Huang, L. Gonzalez, D. Tran, A. Nowak, J. Palowitch, M. Chadwick, E. Talius, H. Mehta, T. Sellam, P. FrƤnken, M. Nicosia, K. He, A. Kini, D. Amos, S. Basu, H. Jobe, E. Shaw, Q. Xu, C. Evans, D. Ikeda, C. Yan, L. Jin, L. Wang, S. Yadav, I. Labzovsky, R. Sampath, A. Ma, C. Schumann, A. Siddhant, R. Shah, J. Youssef, R. Agarwal, N. Dabney, A. Tonioni, M. Ambar, J. Li, I. Guyon, B. Li, D. Soergel, B. Fang, G. Karadzhov, C. Udrescu, T. Trinh, V. Raunak, S. Noury, D. Guo, S. Gupta, M. Finkelstein, D. Petek, L. Liang, G. Billock, P. Sun, D. Wood, Y. Song, X. Yu, T. Matejovicova, R. Cohen, K. Andra, D. DāAmbrosio, Z. Deng, V. Nallatamby, E. Songhori, R. Dangovski, A. Lampinen, P. Botadra, A. Hillier, J. Cao, N. Baddi, A. Kuncoro, T. Yoshino, A. Bhagatwala, M. Ranzato, R. Schaeffer, T. Liu, S. Ye, O. Sarvana, J. Nham, C. Kuang, I. Gao, J. Baek, S. Mittal, A. Wahid, A. Gergely, B. Ni, J. Feldman, C. Muir, P. Lamblin, W. Macherey, E. Dyer, L. Kilpatrick, V. Campos, M. Bhutani, S. Fort, Y. Ahmad, A. Severyn, K. Chatziprimou, O. Ferludin, M. Dimarco, A. Kusupati, J. Heyward, D. Bahir, K. Villela, K. Millican, D. Marcus, S. Bahargam, C. Unlu, N. Roth, Z. Wei, S. Gopal, D. Ghoshal, E. Lee, S. Lin, J. Lees, D. Lee, A. Hosseini, C. Fan, S. Neel, M. Wu, Y. Altun, H. Cai, E. Piqueras, J. Woodward, A. Bissacco, S. Haykal, M. Bordbar, P. Sundaram, S. Hodkinson, D. Toyama, G. Polovets, A. Myers, A. Sinha, T. Levinboim, K. Krishnakumar, R. Chhaparia, T. Sholokhova, N. B. Gundavarapu, G. Jawahar, H. Qureshi, J. Hu, N. Momchev, M. Rahtz, R. Wu, A. P. S, K. Dhamdhere, M. Guo, U. Gupta, A. Eslami, M. Schain, M. Blokzijl, D. Welling, D. Orr, L. Bolelli, N. Perez-Nieves, M. Sirotenko, A. Prasad, A. Kar, B. D. B. Pigem, T. Terzi, G. Weisz, D. Ghosh, A. Mavalankar, D. Madeka, K. Daugaard, H. Adam, V. Shah, D. Berman, M. Tran, S. Baker, E. Andrejczuk, G. Chole, G. Raboshchuk, M. Mirzazadeh, T. Kagohara, S. Wu, C. Schallhart, B. Orlando, C. Wang, A. Rrustemi, H. Xiong, H. Liu, A. Vezer, N. Ramsden, S. Chang, S. Mudgal, Y. Li, N. Vieillard, Y. Hoshen, F. Ahmad, A. Slone, A. Hua, N. Potikha, M. Rossini, J. Stritar, S. Prakash, Z. Wang, X. Dong, A. Nazari, E. Nehoran, K. Tekelioglu, Y. Li, K. Badola, T. Funkhouser, Y. Li, V. Yerram, R. Ganeshan, D. Formoso, K. Langner, T. Shi, H. Li, Y. Yamamori, A. Panda, A. Saade, A. S. Scarpati, C. Breaux, C. Carey, Z. Zhou, C. Hsieh, S. Bridgers, A. Butryna, N. Gupta, V. Tulsyan, S. Woo, E. Eltyshev, W. Grathwohl, C. Parks, S. Benjamin, R. Panigrahy, S. Dodhia, D. D. Freitas, C. Sauer, W. Song, F. Alet, J. Tolins, C. Paduraru, X. Zhou, B. Albert, Z. Zhang, L. Shu, M. Bansal, S. Nguyen, A. Globerson, O. Xiao, J. Manyika, T. Hennigan, R. Rong, J. Matak, A. Bakalov, A. Sharma, D. Sinopalnikov, A. Pierson, S. Roller, G. Brown, M. Gao, T. Fukuzawa, A. Ghafouri, K. Vassigh, I. Barr, Z. Wang, A. Korsun, R. Jayaram, L. Ren, T. Zaman, S. Khan, Y. Lunts, D. Deutsch, D. Uthus, N. Katz, M. Samsikova, A. Khalifa, N. Sethi, J. Sun, L. Tang, U. Alon, X. Luo, D. Yu, A. Nayyar, B. Petrini, W. Truong, V. Hellendoorn, N. Chinaev, C. Alberti, W. Wang, J. Hu, V. Mirrokni, A. Balashankar, A. Aharon, A. Mehta, A. Iscen, J. Kready, L. Manning, A. Mohananey, Y. Chen, A. Tripathi, A. Wu, I. Petrovski, D. Hwang, M. Baeuml, S. Chandrakaladharan, Y. Liu, R. Coaguila, M. Chen, S. Ma, P. Tafti, S. Tatineni, T. Spitz, J. Ye, P. Vicol, M. Rosca, A. PuigdomĆØnech, Z. Yahav, S. Ghemawat, H. Lin, P. Kirk, Z. Nabulsi, S. Brin, B. Bohnet, K. Caluwaerts, A. S. Veerubhotla, D. Zheng, Z. Dai, P. Petrov, Y. Xu, R. Mehran, Z. Xu, L. Zintgraf, J. Choi, S. A. Hombaiah, R. Thoppilan, S. Reddi, L. Lew, L. Li, K. Webster, K. Sawhney, L. Lamprou, S. Shakeri, M. Lunayach, J. Chen, S. Bagri, A. Salcianu, Y. Chen, Y. Donchev, C. Magister, S. NĆørly, V. Rodrigues, T. Izo, H. Noga, J. Zou, T. Kƶppe, W. Zhou, K. Lee, X. Long, D. Eisenbud, A. Chen, C. Schenck, C. M. To, P. Zhong, E. Taropa, M. Truong, O. Levy, D. Martins, Z. Zhang, C. Semturs, K. Zhang, A. Yakubovich, P. Moreno, L. McConnaughey, D. Lu, S. Redmond, L. Weerts, Y. Bitton, T. Refice, N. Lacasse, A. Conmy, C. Tallec, J. Odell, H. Forbes-Pollard, A. Socala, J. Hoech, P. Kohli, A. Walton, R. Wang, M. Sazanovich, K. Zhu, A. Kapishnikov, R. Galt, M. Denton, B. Murdoch, C. Sikora, K. Mohamed, W. Wei, U. First, T. McConnell, L. C. Cobo, J. Qin, T. Avrahami, D. Balle, Y. Watanabe, A. Louis, A. Kraft, S. Ariafar, Y. Gu, E. Rives, C. Yoon, A. Rusu, J. Cobon-Kerr, C. Hahn, J. Luo, Yuvein, Zhu, N. Ahuja, R. Benenson, R. L. Kaufman, H. Yu, L. Hightower, J. Zhang, D. Ni, L. A. Hendricks, G. Wang, G. Yona, L. Jain, P. Barrio, S. Bhupatiraju, S. Velusamy, A. Dafoe, S. Riedel, T. Thomas, Z. Yuan, M. Bellaiche, S. Panthaplackel, K. Kloboves, S. Jauhari, C. Akbulut, T. Davchev, E. Gladchenko, D. Madras, A. Chuklin, T. Hill, Q. Yuan, M. Madhavan, L. Leonhard, D. Scandinaro, Q. Chen, N. Niu, A. Douillard, B. Damoc, Y. Onoe, F. Pedregosa, F. Bertsch, C. Leichner, J. Pagadora, J. Malmaud, S. Ponda, A. Twigg, O. Duzhyi, J. Shen, M. Wang, R. Garg, J. Chen, U. Evci, J. Lee, L. Liu, K. Kojima, M. Yamaguchi, A. Rajendran, A. Piergiovanni, V. K. Rajendran, M. Fornoni, G. Ibagon, H. Ragan, S. M. Khan, J. Blitzer, A. Bunner, G. Sun, T. Kosakai, S. Lundberg, N. Elue, K. Guu, S. Park, J. Park, A. Narayanaswamy, C. Wu, J. Mudigonda, T. Cohn, H. Mu, R. Kumar, L. Graesser, Y. Zhang, R. Killam, V. Zhuang, M. GimĆ©nez, W. A. Jishi, R. Ley-Wild, A. Zhai, K. Osawa, D. Cedillo, J. Liu, M. Upadhyay, M. Sieniek, R. Sharma, T. Paine, A. Angelova, S. Addepalli, C. Parada, K. Majumder, A. Lamp, S. Kumar, X. Deng, A. Myaskovsky, T. SaboliÄ, J. Dudek, S. York, F. de Chaumont Quitry, J. Nie, D. Cattle, A. Gunjan, B. Piot, W. Khawaja, S. Bang, S. Wang, S. Khodadadeh, R. R, P. Rawlani, R. Powell, K. Lee, J. Griesser, G. Oh, C. Magalhaes, Y. Li, S. Tokumine, H. N. Vogel, D. Hsu, A. BC, D. Jindal, M. Cohen, Z. Yang, J. Yuan, D. de Cesare, T. Bruguier, J. Xu, M. Roy, A. Jacovi, D. Belov, R. Arya, P. Meadowlark, S. Cohen-Ganor, W. Ye, P. Morris-Suzuki, P. Banzal, G. Song, P. Ponnuramu, F. Zhang, G. Scrivener, S. Zaiem, A. R. Rochman, K. Han, B. Ghazi, K. Lee, S. Drath, D. Suo, A. Girgis, P. Shenoy, D. Nguyen, D. Eck, S. Gupta, L. Yan, J. Carreira, A. Gulati, R. Sang, D. Mirylenka, E. Cooney, E. Chou, M. Ling, C. Fan, B. Coleman, G. Tubone, R. Kumar, J. Baldridge, F. Hernandez-Campos, A. Lazaridou, J. Besley, I. Yona, N. Bulut, Q. Wellens, A. Pierigiovanni, J. George, R. Green, P. Han, C. Tao, G. Clark, C. You, A. Abdolmaleki, J. Fu, T. Chen, A. Chaugule, A. Chandorkar, A. Rahman, W. Thompson, P. Koanantakool, M. Bernico, J. Ren, A. Vlasov, S. Vassilvitskii, M. Kula, Y. Liang, D. Kim, Y. Huang, C. Ye, D. Lepikhin, and W. Helmholz Gemini 2.5: pushing the frontier with advanced reasoning, multimodality, long context, and next generation agentic capabilities. External Links: 2507.06261, Link Cited by: Ā§4.1, Ā§4.2.1. Li et al. (2022) Y. Li, D. Choi, J. Chung, N. Kushman, J. Schrittwieser, R. Leblond, T. Eccles, J. Keeling, F. Gimeno, A. D. Lago, T. Hubert, P. Choy, C. de Masson dāAutume, I. Babuschkin, X. Chen, P. Huang, J. Welbl, S. Gowal, A. Cherepanov, J. Molloy, D. J. Mankowitz, E. S. Robson, P. Kohli, N. de Freitas, K. Kavukcuoglu, and O. Vinyals Competition-level code generation with alphacode. Science 378 (6624), p. 1092ā1097. External Links: Document Cited by: Ā§2, Ā§2. Liu et al. (2023) M. Liu, N. R. Pinckney, B. Khailany, and H. Ren Invited paper: verilogeval: evaluating large language models for verilog code generation. In International Conference on Computer-Aided Design (ICCAD), p. 1ā8. External Links: Document Cited by: Ā§1. Lu et al. (2024) Y. Lu, S. Liu, Q. Zhang, and Z. Xie RTLLM: an open-source benchmark for design rtl generation with large language model. In Asia and South Pacific Design Automation Conference (ASP-DAC), p. 722ā727. External Links: Document Cited by: Ā§1. Mneimneh and Sakallah (2005) M. N. Mneimneh and K. A. Sakallah Principles of sequential-equivalence verification. IEEE Design & Test of Computers 22 (3), p. 248ā257. External Links: Document Cited by: Ā§1. OpenAI (2025) OpenAI Gpt-oss-120b & gpt-oss-20b model card. External Links: 2508.10925, Link Cited by: Ā§4.1, Ā§4.2.1. Pinckney et al. (2025a) N. Pinckney, C. Batten, M. Liu, H. Ren, and B. Khailany Revisiting verilogeval: a year of improvements in large-language models for hardware code generation. ACM Transactions on Design Automation of Electronic Systems 30 (6), p. 91:1ā91:20. External Links: Document Cited by: Ā§1. Pinckney et al. (2025b) N. Pinckney, C. Deng, C. Ho, Y. Tsai, M. Liu, W. Zhou, B. Khailany, and H. Ren Comprehensive verilog design problems: a next-generation benchmark dataset for evaluating large language models and agents on rtl design and verification. CoRR abs/2506.14074. External Links: 2506.14074, Document Cited by: Ā§1, Ā§4.1. Pixley (1992) C. Pixley A theory and implementation of sequential hardware equivalence. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems 11 (12), p. 1469ā1478. External Links: Document Cited by: Ā§1. Thakur et al. (2023) S. Thakur, B. Ahmad, Z. Fan, H. Pearce, B. Tan, R. Karri, B. Dolan-Gavitt, and S. Garg Benchmarking large language models for automated verilog rtl code generation. In Design, Automation and Test in Europe Conference and Exhibition (DATE), p. 1ā6. External Links: Document Cited by: Ā§1. Wang et al. (2023) X. Wang, J. Wei, D. Schuurmans, Q. V. Le, E. H. Chi, S. Narang, A. Chowdhery, and D. Zhou Self-consistency improves chain of thought reasoning in language models. In The Eleventh International Conference on Learning Representations (ICLR), Cited by: Ā§1, Ā§2, Ā§2. Wang et al. (2025) Z. Wang, Z. Zhou, D. Song, Y. Huang, S. Chen, L. Ma, and T. Zhang Towards understanding the characteristics of code generation errors made by large language models. In Proceedings of the IEEE/ACM 47th International Conference on Software Engineering (ICSE), p. 2587ā2599. External Links: Document Cited by: Ā§1. Wilson (1927) E. B. Wilson Probable inference, the law of succession, and statistical inference. Journal of the American Statistical Association 22 (158), p. 209ā212. External Links: Document Cited by: Ā§4.1. Yan et al. (2025) Z. Yan, W. Fang, M. Li, M. Li, S. Liu, Z. Xie, and H. Zhang AssertLLM: generating hardware verification assertions from design specifications via multi-llms. In Asia and South Pacific Design Automation Conference (ASP-DAC), p. 614ā621. External Links: Document Cited by: Ā§1. Yu et al. (2025) Z. Yu, M. Liu, M. Zimmer, Y. C. Lin, Y. Liu, and H. Ren Spec2RTL-agent: automated hardware code generation from complex specifications using llm agent systems. In 2025 IEEE International Conference on LLM-Aided Design (ICLAD), p. 37ā43. Cited by: Ā§1. Zhao et al. (2025) Z. Zhao, R. Qiu, I. Lin, G. L. Zhang, B. Li, and U. Schlichtmann VRank: enhancing verilog code generation from large language models via self-consistency. In International Symposium on Quality Electronic Design (ISQED), p. 1ā7. External Links: Document Cited by: Ā§1, Ā§2, Ā§4.1. Zheng et al. (2023) L. Zheng, W. Chiang, Y. Sheng, S. Zhuang, Z. Wu, Y. Zhuang, Z. Lin, Z. Li, D. Li, E. P. Xing, H. Zhang, J. E. Gonzalez, and I. Stoica Judging llm-as-a-judge with mt-bench and chatbot arena. In Advances in Neural Information Processing Systems 36 (NeurIPS 2023), Cited by: Ā§1, Ā§2, Ā§4.1.