NoTB：基于跨模型形式共识的无需预言机的LLM生成RTL分类

中文摘要 AI 辅助

大型语言模型（LLM）正越来越多地被用于根据自然语言规范生成寄存器传输级（RTL）设计，但早期阶段的功能正确性评估仍是一项根本性挑战。现有的无需预言机的方法要么依赖基于仿真的一致性，而这取决于可能失效或因模型而异的LLM生成测试平台；要么依赖LLM作为评判者的启发式方法，其预测结果不一致。本文提出NoTB，这是一种无需预言机的分类框架，可通过跨模型形式共识推断正确性。NoTB从多个独立训练的LLM族生成RTL实现，并应用顺序等价性检查（SEC）来识别可证明等价的设计。研究表明，SEC等价簇内的模型族多样性会产生校准后的正确性信号，无需测试平台即可实现风险-覆盖范围权衡。在78项CVDP RTL生成任务上，四族形式共识在27%的覆盖度下达到94.7%的精度，三族共识在33%的覆盖度下达到87%的精度。这些操作点为设计人员在获得可信测试平台或黄金RTL之前提供了可调的接受/弃权（不执行）规则。总体而言，NoTB证明了形式化跨模型一致性为高置信度分类提供了可靠基础，无需依赖模型相关的预言机。

英文摘要

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

发表机构

• Columbia University（哥伦比亚大学）

机构由 AI 辅助整理，请以论文原文为准。

补充信息

备注

MLCAD 2026