半导体 AI 验证与硅片正确性

您的团队已经在 Verilog 上使用 LLM。它无法捕获的那几类缺陷，恰恰是会葬送硅片的那几类。

2024 年 Wilson Research Group / Siemens EDA 功能验证研究将首次流片成功率定在 14%，是二十年追踪以来的最低数字。2020 年时还是 32%。原因并非工程偷懒，而是复杂度超越了验证工具、规格变异比测试平台还快，以及通用 LLM 给 RTL 引入的一类新型失效。我们在 HDL 代码中看到五种行业尚未清晰命名的幻觉模式。

第 1 类

语法幻觉

无法编译的代码。Verilator、Icarus 或综合前端在几秒内就能捕获。这是行业已经知道如何处理的一类。

第 2 类

语义幻觉（阻塞式 vs 非阻塞式）

在 Python 和 C 上训练的 LLM 编写 Verilog 时，仿佛语句是顺序执行的。它们使用阻塞赋值（=），却用在了时钟驱动的 always_ff 块中——而此处需要非阻塞赋值（<=）。仿真器可能以一种掩盖竞态的顺序来调度事件。综合则产生不同的逻辑。硅片陷入死锁。

// LLM 写出的代码。在某些仿真器中仿真“正常”。
always_ff @(posedge clk) begin
  stage2 = stage1;  // 阻塞式
  stage3 = stage2;  // 现在看到的是新的 stage2，而不是旧的
end
// 设计者想要一个 2 周期流水线。硅片出货的却是 1 周期旁路。

第 3 类

协议幻觉（AXI、AHB、TileLink、PCIe）

代码可以编译，并通过 90% 的定向测试。然后它在 AWREADY 之前断言 WVALID，或在翻转数据时把 VALID 保持为高，或违反了埋在 AMBA 规格书第 84 页里的某个子条款。芯片在内部测试平台上正常工作，但一连接到第三方内存控制器就挂起。我们用针对每种协议的预验证 SVA 库来捕获这类问题，而不是靠更多仿真周期。

第 4 类

空泛幻觉（危险的那种）

LLM 生成一条 SVA 属性。形式化引擎证明了它。您出货了。该属性之所以平凡为真，是因为其前件从未触发。这比没有验证更糟糕，因为您手握一份对一个有缺陷设计宣称“已证明”的证书。任何不运行空泛性检查的形式化流程都是作秀。Siemens 自 2017 年以来一直在警告这一点，而业界至今仍在交付不带此功能的工具。

// LLM 生成的“授权随请求而来”属性
property p_grant;
  @(posedge clk) req |-> ##[1:$] gnt;
endproperty
// 如果 LLM 还设置了一个强制 req 永远等于 0 的 assume，
// 形式化引擎会在几毫秒内“证明”这条属性。
// 真正的仲裁器是坏的。这份证书一文不值。

第 5 类

CDC / 亚稳态盲区

LLM 看到的是信号名称，而不是时钟域。它们把 2 GHz CPU 域的信号直接连到 400 MHz 外设域的触发器上，跳过双触发器同步器，而仿真无法捕获，因为 RTL 仿真不建模亚稳态。Accellera 在 2024 年发起了 CDC/RDC/Glitch 互操作性标准，正是因为 SpyGlass、Questa CDC 和 Conformal CDC 之间的碎片化正在破坏签核。

为什么这事关金钱： 70% 的重新流片是由规格变更引起的，而非纯粹的逻辑缺陷（2024 年 Wilson / Siemens 数据）。因此，一个只捕获逻辑缺陷的验证流程只解决了其中一个子集。上文的第 2 类到第 5 类正是仍会葬送流片的那个子集，因为它们绕过仿真，只在硅片中才显现。一次 5nm 重新流片意味着 1000 万美元的掩模版，外加 3 到 6 个月的进度延误。在 18 个月的产品周期里，6 个月的延误可能抹去一半的生命周期收入。

无晶圆厂 DV 负责人实际上正在从中做选择的供应商格局

您真正的备选方案并非理论上的。它们是三大 EDA 巨头（您几乎肯定已经在向他们付费）、六家资金充裕的智能体 AI 初创公司（在 DVCon 和 DAC 上向您推销）、四大系统集成商，以及专业的形式化咨询公司。我们没有产品要与它们竞争。我们帮助您挑选、集成并运营正确的组合。

选项	他们实际做什么	优势	诚实的差距
Cadence JasperGold、Cerebrus AI Studio、ChipStack Super Agent	黄金标准形式化引擎。多模块 RL 驱动的数字实现。智能体 AI 超级代理于 2026 年 2 月发布。	JasperGold 是形式化工具的参考标杆。深度的晶圆厂集成。约占 EDA 市场的 30%。	JasperGold 的历史基准定价（22.5 万美元起 + 每席位 4.5 万美元）对大多数早期 RISC-V / AI 加速器初创公司来说遥不可及。云优先的智能体功能不满足对 IP 敏感的本地部署要求。
Synopsys VC Formal、DSO.ai、AgentEngineer	L4 智能体工作流（AgentEngineer，2026 年 3 月），宣称 2 到 5 倍的生产力提升。基于 RL 的设计空间探索。350 亿美元收购 Ansys 增加了多物理场能力。	最深厚的客户基础。每家大型无晶圆厂公司都已拥有 VC Formal 合同。AgentEngineer 是当今最可信的供应商智能体技术栈。	有鲜明主张的定制流程不是他们的业务。他们不会建议您使用开放权重模型或 SymbiYosys。小型团队只能得到模板化的关注。
Siemens EDA Questa Formal、Questa CDC、Catapult HLS	强大的 Questa 形式化与 CDC 业务。发布 Wilson 研究。最深厚的汽车 ISO 26262 业绩记录。	汽车认证专长。出色的 CDC / RDC 方案。工具认证套件就绪。	智能体 AI 方面落后于 Cadence 和 Synopsys。对 RISC-V 生态的聚焦较少。
ChipAgents 总计 7400 万美元，2026 年 2 月	多智能体 RTL 设计与验证。在 DVCon 2026 上演示了无人在环的多智能体根因分析。	最强的纯智能体故事。Matter Ventures（TSMC 支持）、Bessemer、Micron、MediaTek、Ericsson 位列其股东名册。	云平台。对 IP 敏感客户而言，本地 / 气隙隔离部署路径尚不明确。集成到现有的 Jenkins/CI 签核流程仍需自行实现。
Normal Computing 总计 8500 万美元以上，2026 年 3 月	自动形式化：LLM 将工程师意图翻译为形式化属性并加以证明。三星 Catalyst 领投了上一轮融资。ARIA Scaling Compute 计划。	在 LLM + 形式化论题上最接近的同行。宣称排名前十的半导体设计公司中有一半在使用 Normal EDA。已交付真实硅片（CN101）。	是产品，而非咨询。如果您需要在专有 RTL 语料上进行定制微调，或集成到一个您不会推倒重来的遗留流程中，那它并不合适。
Axiomise 专业形式化咨询公司	formalISA 应用已部署于 Ibex、CVA6、cheriot-ibex、0riscy、cv32e40p、WARP-V。在 Ibex 中发现 65 个以上缺陷，包括六个调试单元分支缺陷。	业界最可信的 RISC-V 形式化验证业绩记录。真实、可发布的缺陷发现。深厚的 ISA 专长。	团队小。仅限形式化方法；没有 LLM 辅助的 SVA 生成，没有本地 LLM 方案，没有与智能体 AI 浪潮的集成。
四大 / 大型 SI Accenture、Deloitte、Wipro、HCL	大型 VLSI / 验证服务业务。现成的人力储备。	规模。离岸交付。与您采购部门已有的 MSA。	人力外包经济模式。有鲜明主张的 AI 验证架构不是他们的业务。向您兜售这项业务的合伙人这辈子从没写过一条 SVA 属性。
Veriprajna 供应商中立的定制构建	在您的 RTL 语料上微调一个开放权重的编码器 LLM，将其包裹在您已经拥有的任何形式化引擎之外，接入您的 Jenkins/CI，并加入空泛性与覆盖率指标。全部运行在您的硬件上。	没有产品要推销。默认本地 / 气隙隔离。RISC-V、AXI4、RISC-V 调试以及形式化覆盖率经济学是我们的舒适区。对形式化方法能做什么、不能做什么诚实以待。	我们不替换您的形式化引擎。我们不交付我们自己认证过的 ISO 26262 工具。规格漂移和组织变革是咨询无法解决的问题；我们只能围绕它们做设计。

定价、融资和产品信息反映截至 2026 年初的公开披露。请务必直接向各供应商核实当前条款。

我们构建什么

每一次合作都是定制的。以下是大多数无晶圆厂客户最终会要求的五种形态，以及我们在每一种内部所做的有鲜明主张的选择。

1. 本地 LLM + 形式化粘合层

一个经过微调的开放权重编码器模型（Qwen 2.5 Coder、DeepSeek Coder、Llama 3.3 或 Mistral Large），运行在您自己的 H100 或 H200 集群上，包裹在您已经拥有的任何形式化引擎之外。绝无任何 RTL 离开您的网络。

我们会采用的：用 vLLM 进行推理，每个 IP 家族一套 LoRA 适配器以便基础权重保持共享，在您的规格文档和过往缺陷历史上做本地 RAG，以及一个轻薄的编排层，通过 JasperGold、VC Formal、Questa Formal 或 SymbiYosys 的 Tcl/Python API 调用它们。LLM 从不运行求解器。它编写属性并解释反例。

为什么这不是托管 API：因为您的 RTL 是皇冠上的明珠级 IP，而您的 CISO 不会与一家去年才成立的美国或欧洲初创公司签署数据处理协议。

2. RISC-V 形式化测试平台与 SVA 库

针对 AXI4、AXI4-Lite、APB、AHB 和 TileLink 合规性的预构建 SystemVerilog 断言库，外加 RISC-V 流水线冒险检测、Load-Store 单元记分板、调试单元正确性以及 CSR 访问检查，并针对您的自定义扩展 ISA 进行调优。

参考点： Axiomise 通过形式化在 Ibex 内核中发现 65 个以上缺陷，包括六个仿真漏过的调试单元分支缺陷。形式化在 RISC-V 上行得通。瓶颈在于能编写断言的工程师稀缺。我们构建这个库，这样您的团队就不必去做。

诚实的告诫：一个精心策划的断言库比 LLM 从零生成更可靠，但仍无法证明每一类缺陷的不存在。我们将其与 COI（影响锥）和基于变异的覆盖率分析配对使用。

3. 供应商中立的工具选型与试点

您的 DV 负责人正被 ChipAgents、Normal Computing、MooresLabAI、Silimate、Bronco AI 以及内部的 Cadence 和 Synopsys 智能体产品轮番推销。六款产品，六种不同的宣称，在您实际的 RTL 上没有任何独立的基准测试。

我们做什么：在保密协议下，对您的代码库进行为期四周的结构化比拼。相同的测试套件、相同的缺陷预算、相同的覆盖率目标。一份诚实的报告，比较缺陷发现率、误报率、搭建工作量、集成负债，以及每家供应商实际向您开出的定价条款。

为什么买家在这件事上信任我们：我们不转售这些产品中的任何一款。如果正确答案是“留用 JasperGold 并加上一层轻薄的 LLM 辅助”，我们就会这么说。

4. 在您的 CI 中进行智能体 RTL 评审

每一个触及 RTL 的拉取请求，在人工查看之前都会先由一条多智能体流水线评审。一个智能体进行代码风格检查与 lint。第二个运行从变更文件派生的一组形式化属性。第三个检查 CDC 和 RDC 路径。第四个生成一份人类可读的摘要，并在属性失败处附上反例轨迹。

有鲜明主张的选择：我们在您现有的 CI（Jenkins、GitLab、BuildKite，无论哪一种）内部运行这些智能体。我们不会用一个新平台替换您的 CI。这些智能体是流水线调用的服务。当您解雇我们时，流水线归您保留。

我们拒绝构建什么：一个无需人工评审就自动合并 RTL 的智能体。硅片不是微服务。您无法给芯片发布热修复。

5. Chiplet / 3D-IC 热感知布局规划（适当情况下采用 RL 布局）

这是我们认为强化学习用于布局确实值得部署的唯一场景。现有厂商（Cadence Cerebrus、Synopsys DSO.ai）是为单片 2D SoC 调优的。Chiplet / UCIe 浪潮开启了一类全新的布局规划问题（芯粒间连线长度、热堆叠、凸点间距约束），而公开的工具链尚不成熟。

我们构建什么：在 OpenROAD 之上为 chiplet 划分阶段构建一个混合的模拟退火 + RL 布局规划器，以热约束作为一等奖励项。在我们触碰您的设计之前，先针对已发表的 ISPD / ICCAD 结果进行基准测试。

我们直接承认 AlphaChip 争议。 Igor Markov 在 2023 年的批评显示，Google Circuit Training 耗时 32 小时，而经过调优的模拟退火运行只需 12.5 小时，一款 Cadence 商用工具仅需 0.05 小时。在那些充分理解的问题上，我们不会把 RL 标榜为调优过的 SA 的替代品。我们在设计空间确实全新、人类直觉无先验可循之处才使用它。

我们如何工作

每一次合作都从一个为期两周的范围界定阶段开始，针对您 RTL 的一小块，在我们触碰任何更大规模的东西之前进行。我们宁愿在第二周就抽身离开，也不愿因不合适而消耗您的进度。完整构建的典型节奏。

范围界定 · 2 周

阅读您的规格，走查您现有的流程，挑选一个有代表性的模块（通常是总线接口、仲裁器，或单个 RISC-V 流水线级），并在其上运行我们的基线形式化测试平台。产出：一份书面报告，列出我们看到的缺陷类别、我们会构建的断言，以及完整合作的成本估算。如果答案是“您应该继续照现在的做法做”，我们就这么说，并只就这两周计费。

基础设施 · 4 到 6 周

在您的集群上部署本地 LLM 技术栈。在您的 RTL 语料上用 LoRA 适配器微调基础模型。在您的规格和过往缺陷数据库上建立 RAG 索引。接入您的形式化引擎、您的 Jenkins/CI 以及您的问题跟踪系统。从第一天起，我们就用证明覆盖率、空泛性和有界深度指标对一切进行检测埋点。

断言库与上线 · 6 到 10 周

我们为您排名前 3 到 5 的 IP 模块移植或编写 SVA 库（协议合规性、流水线、CDC）。我们运行形式化回归。我们与您的 DV 负责人一起分诊发现的问题。到该阶段结束时，您的团队拥有每一条断言。没有黑盒。

交接 · 2 到 4 周

您的工程师在我们的注视下运行该流程两个完整的冲刺周期。我们记录我们所做的每一个有鲜明主张的选择，以便下一个人能够理解原因。我们退出。如果您愿意，可选保留聘约用于回归调优。

时间线是诚实的范围区间，而非销售数字。一个 2 级流水线模块可以在三周内完成。一个带自定义扩展的完整 RISC-V 内核则接近五个月。我们事先就这么讲，而且不会为了赶上一个人为设定的日期而压缩。

重新流片风险敞口计算器

三项输入。告诉您掩模版成本敞口、预期进度延误，以及在您所用节点上一次硅片重新流片的风险收入。这些数字来自 2024 年 Wilson Research Group / Siemens 研究、近期 SemiAnalysis 掩模版成本数据，以及典型的 18 个月产品周期。请在您下一次流片就绪评审中使用它。结果会推荐一些您无需雇用我们就能采取的具体行动。

工艺节点

该产品的年收入目标（百万美元）

专职形式化验证工程师

DV 负责人和 CTO 实际会问的问题

这些是来自无晶圆厂和 RISC-V 客户的真实问题。每个回答都补充了上述章节未涵盖的深度。

是否有任何 RTL 或 GDSII 离开我们的网络？

不会。我们交付的每一种部署架构都运行在您的硬件上。经过微调的模型权重驻留在您的集群上。带有您 IP 专属调优的 LoRA 适配器驻留在您的防火墙之后。vLLM 推理运行在您的 GPU 上。RAG 从您自己的文档库中索引您的规格文档。我们的工程师通过您标准的 VPN 和 SSO（带审计日志）访问该环境。对于国防、航空航天和 SCIF 客户，我们以签名的离线更新捆绑包交付整个技术栈，并且不要求该环境有任何对外连接。唯一的例外是初始基础模型的下载，这在一个非密系统上完成，然后再转移进来。如果您需要比这更严格的气隙隔离，我们也做过。

我们怎么知道 LLM 生成的断言不是空泛的？

空泛性是我们最担忧的失效模式，也正因如此，我们交付的每一条形式化流程都运行一个三层检查。第一，形式化引擎的原生空泛性检查（JasperGold 和 VC Formal 都有；SymbiYosys 需要我们提供的封装）。第二，一个基于变异的健全性检查，我们在设计中注入一个缺陷，并确认断言触发。一条通过空泛性检查但抓不住注入缺陷的断言对您毫无价值。第三，一份 COI（影响锥）报告，精确显示每条属性触及哪些信号。如果一条属性的 COI 为空，它就是死代码，我们将其删除。这些正是 Siemens 自 2017 年以来一直在 Verification Horizons 上发表的同样指标，我们将其视为基本门槛。

我们是一家瞄准 ISO 26262 ASIL D 的汽车客户。我们能用这套流程进行签核吗？

不能直接用于签核，我们也不会假装可以。ISO 26262 要求工具认证（视您如何使用工具而定，为 TCL2 或 TCL3），并附带文档化的认证套件。Synopsys、Cadence 和 Siemens 都交付经过认证的流程；一个定制的 LLM 辅助工具不在该名单之列。我们为汽车客户构建的，是一个与经认证工具并行运行、而非取而代之的 AI 辅助层。经认证的工具仍然产出签核证据。我们的层加速断言编写、对属性进行空泛性评审，并标记 CDC 路径供人工检查。您已签核工具的认证链丝毫不受影响。ASIL D 客户还应计划在辅助层与经认证验证之间进行一次文档化的独立性评审，我们会帮助您搭建这一结构。

我们为什么不干脆改买 ChipAgents 或 Normal Computing？

您可能会。两者都资金充裕、技术上可信，并拥有真实客户。团队在评估它们之后转向我们的原因，通常是三件事之一。第一，云部署模式没能通过他们的安全评审（常见）。第二，他们需要在一个专有自定义扩展 ISA 上进行微调，而产品团队无法优先处理。第三，他们想要一个集成到现有 Jenkins / 回归 / 签核流程的定制方案，而产品团队若不投入一笔六位数的专业服务合约就无法支持。如果这些对您都不适用，那产品很可能就是正确答案，我们也会这么说。如果它们确实适用，我们就构建那一层定制层，并留给您一个您自己的工程师能够维护的系统。在试点上，我们建议把这三个选项放在同一份 RTL 上跑四周。相比一个错误的押注，这场比拼很便宜。

对于 RL 布局的 AlphaChip / Markov 争议，您的立场是什么？

我们认为 Igor Markov 的批评在具体数字上技术上是正确的。Google Circuit Training 32 小时，对比调优过的模拟退火 12.5 小时，以及一款 Cadence 商用工具 0.05 小时，这并不是 RL 在主流 SoC 上赢得布局的故事。这并不意味着 RL 对硅片毫无用处。它意味着 2020 年的论调是错的。我们认为 RL 布局如今值得耗费算力的场景是：设计空间确实全新的 chiplet 和 3D-IC 布局规划、现有工具薄弱的热感知模拟版图，以及在紧密相关的 RISC-V IP 家族之间进行迁移学习——在您上一代上训练的智能体能给您一个热启动。我们不会在 5nm 的单片数字 SoC 上拿 RL 布局去对抗 DSO.ai 或 Cerebrus。那是一场我们会输、而您会买单的较量。

你们如何应对“70% 的重新流片来自规格变更而非逻辑缺陷”这一事实？

老实说，这是验证中最棘手的问题，没有任何 AI 工具能干净地解决它。我们的做法是把规格当作验证流程的一等输入。LLM 监视规格仓库（Confluence、Google Docs、Git，无论您用哪一个），并标记那些底层假设已经改变的属性。当评审者将规格的某一节标记为已修订时，依赖它的属性会被自动重新运行，差异报告会在下一次回归收尾之前送达 DV 负责人。这并不能消除规格漂移。没有什么能消除。它让漂移在数小时内、而不是在硅片中变得可见。我们在这方面看到的最大单项收益，是在“规格两个冲刺之前就改了、却没人重新运行受影响的形式化属性”一事沿层级蔓延之前将其抓住。

我们已经拥有 JasperGold。我们应该替换它吗？

不应该。JasperGold 是最好的商用形式化引擎，当客户已经拥有它时我们就使用它。我们所增加的，是在其之上的 LLM 辅助层（断言生成、反例解释、空泛性健全性检查），以及一个大多数团队还没花时间干净地搭建过的 CI 集成。您对现有 JasperGold 投资的回报是上升的，而不是下降的。如果您不拥有 JasperGold，又无法为基础价 + 每席位定价辩护，我们通常会推荐一种混合方案：用 Questa Formal（每席位更便宜）做批量回归，用 SymbiYosys（开源）做自动化属性调试。我们曾把这套技术栈交付给那些购买 JasperGold 并非选项的 RISC-V IP 初创公司。

这套方案能适用于多小的团队？

我们为一个 6 人的 RISC-V IP 初创公司构建过有用的流程，也为一家 400 人的 AI 加速器公司构建过。下限是团队中至少有一名工程师能够自如地阅读 SVA 并解释形式化反例轨迹。如果团队里没有人能读懂一条 SVA 属性，那么任何 LLM 辅助流程都无法弥补那道缺口，您应该在与我们或任何人合作之前，先招聘或外包这项技能。在那条基线之上，合作的规模随纳入范围的 RTL 多少而扩展。一个单独的总线接口模块是一个六周的活儿。一个带自定义扩展和互连结构的完整 RISC-V 内核则是四到六个月。

您的首次流片成功率只有 14%。LLM 生成 RTL 的胜算更糟。