硅奇点：弥合 概率式生成式 AI 与确定性 硬件正确性之间的 鸿沟

1. 执行宣言：千万美元级空 指针

半导体产业正站在一个岌岌可危的十字路口，悬于两股 对立力量之间：生成式人工智能（Generative Artificial Intelligence） （GenAI）无边无际的概率式创造力，与纳米级硅片不容妥协的确定性物理法则。我们正 目睹一场淘金热。电子设计自动化（EDA）正在被重新想象，大批 工程师转向大型语言模型（LLM）以加速 Verilog 与 SystemVerilog 代码的创建。承诺极具诱惑力——将设计周期从 数年缩短至数月，实现芯片设计的民主化，并自动化繁琐的 寄存器传输级（RTL）编码。

然而，在这场生产力革命之下潜伏着系统性风险，威胁要动摇 无晶圆厂半导体模式的根基。这一风险并非以编译 错误或 lint 警告来衡量，而是以硅片重流片来衡量。

Veriprajna 的创立基于一个单一、无可辩驳的前提，它源于痛苦的现实： 在硬件设计中，语法不是语义，似是而非也不是正确性。

本白皮书阐述 Veriprajna 方法论——对标准 「LLM 即助手」范式的激进背离。我们提出一个企业级框架， 将大型语言模型的创造性生成能力与 形式化验证的数学严谨性相融合。我们将其定位为不仅是生产力工具，更是无晶圆厂半导体公司在埃时代生存所必需的风险缓释 引擎。

1.1 一千万美元失误的解剖

Veriprajna 的起源在于我们创始人所强调的一次特定、灾难性失败—— 由单一竞争条件导致的 1000 万美元硅片重流片。这不是 想象力的失败；而是验证覆盖率的失败。

在所描述的事件中，一支高度胜任的设计团队利用先进的 LLM 辅助 工作流加速定制 RISC-V 加速器的开发。该模型训练于 海量开源硬件代码库，生成了一个看似完美的仲裁 模块，用于高速存储器接口。代码仿真干净通过。它通过了标准 回归测试。Lint 无错误。设计已流片。

六个月后，当代工厂首批硅片到货时，芯片死锁。在 热节流与高带宽流量的一种特定、罕见对齐条件下，仲裁器进入 未定义状态。根本原因是微妙的竞争条件——一种「抗仿真」缺陷， 其中阻塞与非阻塞赋值之间的区别造成了 RTL 仿真模型与综合网表之间的不匹配。 ¹

代价是绝对的。5nm 工艺节点的掩模组，估值约 1000 万 美元，变得毫无用处。 ³ 但真正的代价是 机会成本 。为诊断、修复并 重新制造芯片所需的六个月延迟，意味着错过器件集成的关键市场 窗口。在 AI 加速器极度竞争的格局中， 产品代际仅持续 18 个月，六个月延误相当于损失 30-50% 的终身收入。 ⁴

1.2 封装器迷思

业界对 EDA 中 AI 需求的当前回应，是 「封装器」方案的泛滥。这些工具本质上将标准 LLM（如 GPT-4、Llama 3 或 Claude）包裹在聊天界面中，注入一些 Verilog 专用系统提示，并将其呈现为 「芯片设计副驾驶」。 ¹

Veriprajna 拒绝这一模式。我们主张 LLM 本质上是 随机词元 预测器 。它们并不「理解」电路拓扑、时序收敛或亚稳态。它们 根据训练数据中的统计相关性预测下一个最可能的词元。当 应用于软件时，「幻觉」导致可通过空中补丁修复的 运行时错误。当应用于硬件时，幻觉导致无法 修补的报废芯片。

解决方案不是更好的提示工程。而是 神经符号 AI ——一种混合架构， 将神经网络的生成能力与 形式化方法的绝对证明能力相结合。本文详述 Veriprajna 如何实现该架构，以确保 千万美元失误不再重演。

2. 摩尔定律的经济热力学

要理解为何 Veriprajna 的 Deep AI 方法不可或缺，必须首先直面 现代半导体设计的残酷经济学。失败成本并非线性；而是 指数级。

2.1 验证经济学中的「十法则」

业界遵循一项严苛启发式，称为「十法则」。识别 并纠正缺陷的成本，在设计生命周期的每个后续阶段 增加一个数量级。 ⁵

设计阶段	检测方法	修复成本	风险概况
RTL 设计	设计工程师 检查 / Lint	~$100	可忽略。 拼写错误 数分钟内即可修复。
模块验证	单元仿真 / 定向测试	~$1,000	低。 需要 测试平台 修改并 重新运行。
系统 验证	全芯片仿真 / 回归	~$10,000	中等。 消耗 昂贵的仿真器 时间与工程师 工时。
硅后（实验室）	验证板 / 逻辑分析仪	~$10,000,000+	灾难性。 需要重流片 （新掩模）。
现场	客户退货 / 召回	~$100,000,000+	生存性。 品牌 损害、诉讼、 全面召回（例如 FDIV 缺陷）。

表 1：硬件缺陷成本的逐级攀升 ⁶

标准「封装器」AI 方案主要在 RTL 设计 阶段运作，帮助工程师 更快地编写代码。然而，由于缺乏严格验证能力，它们往往 引入绕过模块与系统验证的微妙缺陷，仅在 硅后或现场阶段才显现。通过提高代码生成的 速度 却不提高 验证的 严谨性 ，这些工具实际上加速了高成本缺陷 注入流水线。

Veriprajna 将验证负担左移。通过将形式化验证直接集成到 生成循环中，我们迫使在 $100 阶段发现深层逻辑缺陷，防止 其演变为 1000 万美元负债。

2.2 掩模成本壁垒

硅片中「沉没成本」的物理现实，是软件与 硬件经济学之间的首要区分因素。在成熟节点（如 28nm），掩模组可能花费 200-300 万美元。 然而，随着产业向 5nm、3nm 及高数值孔径 EUV 工艺推进，掩模组 成本已飙升至 1000 万至 2000 万美元之间。 ⁸

这种资本密集度造就了极度风险规避的文化。「一次成功」硅片并非 口号而已；而是财务要务。行业调查数据表明，仅 32% 的 设计实现首次硅片成功。 ⁸ 其余 68% 至少需要一次重流片。 这些重流片的首要原因是逻辑与功能缺陷——正是 LLM 在幻觉接口协议或误解 并发语义时 易于生成的错误类型。 ⁹

2.3 时间的机会成本

除掩模的直接现金支出外，延误成本往往是半导体初创企业的 真正杀手。

●​ 市场窗口： 消费电子、汽车与 AI 硬件遵循严格的 年度或半年度周期。错过窗口意味着错过持续 平台生命周期（3-5 年）的设计中标。

●​ 重流片惩罚： 重流片通常使进度增加 3 至 6 个月。这包括 根因分析（在实验室调试硅片）、RTL 修复、再验证、 再综合、布局布线、时序收敛，以及最终的再制造与封装。 ⁴

●​ 收入影响： 六个月延误可侵蚀产品终身毛利的 50% 。 对于瞄准 1 亿美元收入流的公司，重流片是 5000 万美元损失，远 超 1000 万美元掩模成本。 ¹⁰

Veriprajna 将自己定位为抵御这一延误的保险。我们以计算 强度（在设计期间运行形式化求解器）换取进度确定性。

3. 语言鸿沟：LLM 为何在硬件上产生幻觉

若 LLM 能通过律师资格考试并编写 Python Web 服务器，为何在 设计可靠芯片时如此惨败？答案在于软件与硬件描述语言（HDL）之间 根本性的语言分歧。

3.1 顺序与并发的悖论

标准 LLM（GPT-4、Claude、Llama）训练于以软件 语言（如 Python、Java、C++）为主的数据集。这些语言是 命令式且顺序的 ：第 A 行执行，然后第 B 行执行。系统状态由 操作序列定义。

Verilog 与 VHDL 是 声明式且并发的 。在硬件模块中，每个 always 块、 每个 assign 语句及每个模块实例化 同时 且 持续执行。源代码中的行序往往与 硅片中的执行顺序无关。 ¹¹

LLM 失效模式： LLM 受「顺序偏见」之苦。它们倾向于像写 C 代码一样写 Verilog。它们 频繁误用阻塞赋值（=），而在需要非阻塞赋值（<=）之处 却使用了阻塞赋值。

●​ 软件思维： a = b; b = a; 交换变量。

●​ 硬件现实： 在时钟 always 块中，a = b; b = a; 使用阻塞赋值 会产生 竞争条件 。取决于仿真器内部调度，b 可能被赋值为 a 的 新 值而非旧值，导致 a 与 b 变为 相等而非交换。

这一区分在语法上微妙，在物理上却灾难性。「封装器」AI 看到合法 语法便予以通过。Veriprajna 的形式化引擎立即检测到竞争条件。 ¹²

3.2 协议的幻觉

硬件设计高度依赖严格协议（AXI、AHB、PCIe、TileLink）。这些协议 具有复杂时序规则（例如「Ready 不得等待 Valid」，或「Grant 必须在 5 个周期内置位」）。 LLM 通过统计概率模拟「理解」。它们可能生成一个 90% 时间看起来正确的 AXI 主设备，

却在角落情形失败——例如，在违反 AMBA 规范 特定子条款的方式下，于 AWREADY（Address Write Ready）之前置位 WVALID （Write Valid）。这不是语法错误；而是 功能性 幻觉 。代码可编译，但芯片在连接至合规存储器控制器时将挂起。 可用于训练的高质量开源 Verilog 代码体量，比 Python 或 JavaScript 代码 ¹⁴

3.3 训练数据稀缺

小几个数量级。 GitHub 上大量可用 Verilog ¹ 由学生项目、废弃原型或「玩具」实现构成， 不符合工业编码标准或时序约束。 向训练集引入偏见与幻觉，导致「模型崩溃」，

●​ 递归退化： 使用商业 LLM 生成合成训练数据可能 AI 强化自身错误。 相关约束（SDC 文件）、综合日志或形式化验证测试平台。 ¹¹

●​ 缺乏物理语境： 标准训练数据包含 RTL，但很少包含 LLM 看到 代码 却看不到 意图 或 物理约束（时序、面积、功耗）。 要理解 Veriprajna 所解决问题的规模，必须仔细审视 ¹

4. 竞争条件：技术尸检

「竞争条件」——数字设计者的宿敌。本节解构 竞争条件机制，说明为何标准 LLM 对其视而不见， 而形式化验证却一目了然。 最阴险的缺陷形式之一是仿真-综合不匹配。当 RTL 代码

4.1 仿真-综合不匹配

以一种方式仿真（掩盖缺陷）却综合为行为不同的逻辑门时，便会发生。 考虑一个简单的流水线寄存器更新： Verilog ¹⁶

在此片段中，由于使用阻塞赋值（=），stage2 立即以

stage1 的值更新。然后 stage3 以 stage2 的 新 值更新。实际上，数据

always @(posedge clk) begin
stage2 = stage1; // Blocking assignment
stage3 = stage2; // Blocking assignment
end

在单个时钟周期内从 stage1 移至 stage3。 然而，设计者可能意图数据需 两个 周期才能移动。若 综合工具或不同仿真器以不同方式优化执行顺序（或若代码

分散在多个块中），行为将变得非确定性。LLM 训练于 变量立即更新的软件语境，偏好此语法。所得硬件 无法时序收敛或在高速下功能错误。 表现为流水线冒险。 在 Veriprajna 专精的 RISC-V 处理器语境中，竞争条件往往 ¹⁷

4.2 RISC-V 中的流水线冒险

五级流水线（取指、译码、执行、访存、 写回）需要复杂的「转发」逻辑，将数据从后续阶段传回较早 ¹⁸ 阶段以避免停顿。

1000 万美元场景： 设想 LLM 为 ALU 生成转发逻辑。它正确地将数据从

访存阶段转发至执行阶段以处理简单算术。然而，它未能处理 特定角落情形： 寄存器文件拾取「陈旧」数据。 依赖 ADD 指令，同时发生外部中断。

●​ 指令序列： 一条 LOAD 指令（具有延迟）紧随其后是一条 「forward」信号相互竞争。ADD 指令在 LOAD 写回新数据之前，从

●​ 缺陷： 逻辑未能正确停顿流水线，因为「stall」信号与 纳秒级精确时刻注入中断。 因为标准测试平台很少在 LOAD-ADD 依赖发生的 ¹⁴

●​ 结果： 处理器计算 2 + 2 = random_value。此缺陷「抗仿真」， 错误的物理竞争条件。当信号从快时钟域（例如 2GHz CPU）传至慢时钟 除逻辑外，还存在称为时钟域交叉（CDC）

4.3 物理错误：CDC 与亚稳态

域（例如 400MHz 外设）时，必须同步。 不确定时间。这可像病毒一样在芯片中传播，导致全系统 接收触发器可进入「亚稳态」——既非 0 也非 1——持续

●​ 亚稳态： 若信号恰在接收时钟上升沿改变值， 损坏。 双触发器同步器或 FIFO 桥接。没有详细时序模型的仿真 时钟域。它们常直接连接这些信号，省略所需的 ¹

●​ LLM 盲点： LLM 看到信号名（cpu_data、peri_data）。它们看不到 将通过。硅片将失败。 双触发器同步器或 FIFO 桥接。没有详细时序模型的仿真 将通过。硅片将失败。

5. 形式化验证的复兴：真理 引擎

为弥合 AI 幻觉与硬件现实之间的鸿沟，Veriprajna 借助 形式化 验证 。LLM 运行于 概率 领域，形式化验证运行于 证明 领域。

5.1 从仿真到证明

传统验证依赖 仿真（动态验证）。这相当于 绕街区驾驶汽车 1000 次来测试刹车。若刹车未失效，便假定 安全。但若仅在下雨、车速 60mph 且收音机 开启时才失效呢？仿真只能验证其明确测试的场景。 ¹⁹

形式化验证（静态验证）并不「运行」设计。它将设计转换为 数学公式。这相当于运用物理学与结构工程 计算刹车片的应力极限。它证明 在任何可能条件下 刹车 都不会失效。

5.2 SMT 求解器机制

Veriprajna 引擎的核心是 可满足性模理论（SMT） 求解器，如 Microsoft 的 Z3 或 CVC5。 ²⁰

1.​ 位展开（Bit-Blasting）： 求解器将高层 Verilog（整数、数组、向量）转换为 表示设计中每个逻辑门与触发器的 巨型布尔公式（SAT 实例）。

2.​ 约束求解： 求解器接受「属性」（正确行为的断言） 并尝试寻找「反例」。

○​ 属性： assert(!(req == 1 && grant == 0) );

○​ 求解器查询： 「寻找 req == 1 且 grant == 0 的状态。」

3.​ 穷举搜索： 求解器运用高级代数启发式搜索整个 状态空间——所有 $2^{N}$ 种输入与内部状态组合。

4.​ 裁决：

○​ UNSAT（不可满足）： 求解器 证明 不存在缺陷。设计相对于该属性 在数学上完美。

○​ SAT（可满足）： 求解器找到打破设计的 特定输入序列。该序列作为 反例轨迹 返回。

5.3 SystemVerilog 断言（SVA）

形式化验证的语言是 SVA。这些断言充当硬件的「契约」。 SVA 构造 ²³

表 2：Veriprajna 使用的常见 SVA 构造

含义	验证中的用途	$rose(signal)
信号从 0	跳变至 1 检测	事务起始。 $stable(signal)
信号值未	改变 确保数据有效性	在保持时间内。 （蕴含）
`	->` 若左侧为真，则检查右侧	在整个期间

条件持续成立	持续时间 整个 reset 期间（active ==	0） $past(signal, N)
N 个周期前信号	的值 检查流水线延迟	正确性。 编写这些断言对人类而言极其困难，这正是形式化验证

编写这些断言对人类而言极其困难，这正是形式化验证 历来是小众学科的原因。Veriprajna 的突破在于用 AI 编写 断言，并用形式化工具 检查 AI 的代码。 ²⁵

6. Veriprajna 方法论：神经符号 「形式化三明治」

Veriprajna 不是「副驾驶」。我们是 神经符号验证引擎 。我们采用 专有工作流 「形式化三明治」 以确保 构造即正确（Correctness-by-Construction）。 ²⁶

6.1 架构概览

我们的平台融合两种截然不同的 AI 范式：

1.​ 神经层（创造性）： 在 Verilog 与 SystemVerilog 上微调的 LLM。它 处理「什么」（解读人类意图）并生成初始 RTL 与 断言。

2.​ 符号层（批判者）： SMT 求解器（形式化验证引擎）， 处理「如何」（证明正确性）。它充当神经层输出的 毫不妥协的裁判。 ²⁷

6.2 分步工作流

步骤 1：多模态意图提取

用户提供规格。可以是文本（「设计 APB 到 AXI 桥」）或 多模态输入，如时序图图像或数据手册截图。 ²⁹

●​ 操作： 规格分析智能体 将请求分解为功能需求 （接口定义、时序约束、复位行为）。

步骤 2：双路径生成（生成器）

LLM 不仅生成代码，还被提示生成两个相互强化的 产物：

●​ 产物 A：RTL 实现。（Verilog 代码）。

●​ 产物 B：形式化规格。（一组 从需求衍生的 SVA 属性集）。

○​ 示例： 若规格说「Grant 必须跟随 Request」，LLM 生成 Verilog FSM 以及 SVA：property p_grant; @(posedge clk) req |-> ##[1:$] gnt; endproperty.

步骤 3：符号裁判（对抗者）

Veriprajna 启动形式化验证实例（使用 JasperGold 等引擎或 封装于我们 Symbiosis 层的开源等价物）。它尝试证明产物 A 符合产物 B。 ³⁰

●​ 空虚性检查： 求解器首先检查断言是否「空虚为真」（例如，若 req 始终未置高，断言将平凡通过）。这可捕获「懒惰」的 AI 生成。 ³¹

●​ 有界模型检测（BMC）： 求解器深入探索状态空间（例如 50-100 个周期深度）以发现死锁或竞争条件。

步骤 4：反例引导精炼（修复器）

若求解器发现缺陷（SAT），它将生成波形轨迹，精确展示缺陷 如何 显现。

●​ 创新点： 我们不仅向用户展示此轨迹。我们将数学 反例 反馈 给 LLM 作为提示。 ²⁶

●​ 提示： 「你的设计失败了。这是轨迹：周期 1：Reset=0。周期 2：Req=1。周期 10： Grant=0。Grant 从未到达。修复状态机。」

●​ LLM 分析轨迹，识别逻辑缺陷（例如缺失状态转移），并 重写代码。

此循环自动重复，直至设计被证明正确（UNSAT）。

6.3 应对「状态空间爆炸」

形式化验证可能计算成本高昂。Veriprajna 通过 自动化抽象技术 ³² 加以缓解：

●​ 黑盒化： 我们在验证胶合逻辑时，将大型子模块（如 RAM 或 复杂 ALU）视为黑盒。

●​ 切割点： 我们切断 valid/ready 路径，独立于数据处理 验证流控。

●​ 对称性归约： 我们为路由器的一个通道证明属性，并 数学归纳至所有 N 个通道。

7. 案例研究：RISC-V 与开源

战场

为展示 Veriprajna 方法论的功效，我们考察其在 RISC-V 处理器设计中的应用——这一领域充满复杂性与开源缺陷。

7.1「Ibex」与「PULP」缺陷

开源 RISC-V 社区产出了优秀内核，如 Ibex（用于 OpenTitan）与 PULP 平台。然而，即使这些经过严格审查的设计也包含 仅形式化验证才能发现的缺陷。

●​ 调试单元死锁： Axiomise 的形式化验证在 Ibex 内核中发现缺陷：分支指令执行期间特定周期到达的调试请求 可导致内核死锁或执行错误指令。 ³³

●​ AXI 饥饿： 在 PULP 平台中，发现 AXI 互连 在 AWVALID 与 AWREADY 以特定 「繁忙」模式交互时，可无限期饿死主设备。这是典型的活性失败。 ¹⁴

7.2 Veriprajna 实战

当 Veriprajna 受命生成 RISC-V 加载-存储单元（LSU）时，它自动生成 以下断言：

●​ 接口合规： 「若 valid 置位，则必须保持高电平直至收到 ready」 （AXI4 要求）。

●​ 数据完整性： 「从地址 X 读取的数据必须与最后写入地址 X 的数据匹配」（记分板）。

●​ 前向进展： 「LSU 必须最终向内核返回响应」（活性）。

通过在生成期间强制执行这些属性，Veriprajna 产出能够抵御 困扰手动设计角落情形的稳健内核。我们不仅依赖开源 IP； 我们验证它。

8. 战略路线图：从副驾驶到自动驾驶

Veriprajna 正引领从「计算机辅助设计」（CAD）向 「计算机 自动化设计」 的转型。

8.1 面向 EDA 的 Agentic AI

我们正超越单次提示交互，迈向 Agentic 工作流 。 ³⁵ 在 Veriprajna 生态系统中，自主智能体协作：

●​ 智能体 A： 架构师（高层布局规划与划分）。

●​ 智能体 B： RTL 编码器（详细实现）。

●​ 智能体 C： 验证工程师（编写 UVM 测试平台与 SVA）。

●​ 智能体 D： 管理者（编排流程并检查功耗/面积 约束）。

这些智能体通过共享上下文通信，迭代精炼设计直至满足 所有 PPA（功耗、性能、面积）与功能目标。

8.2 面向硬件知识的 RAG

我们采用 检索增强生成（RAG） ，不仅用于代码，更用于 知识 。 ³⁶ 我们的数据库包括：

●​ 标准接口协议（AXI、AHB、APB、PCIe）。

●​ 7nm/5nm 节点的工艺设计套件（PDK）规则。

●​ 企业内部知识库（历史缺陷报告、设计指南）。

当 LLM 生成代码时，它检索企业编码标准中的特定「规则 34」 关于复位极性，确保合规而不产生幻觉。

8.3 通往零缺陷硅片之路

我们的终极目标是 零缺陷硅片（Zero-Bug Silicon） 。通过将形式化验证集成到生成 循环中，我们将断言覆盖逻辑的缺陷逃逸率降至接近零。虽然 模拟物理始终带来挑战，但逻辑缺陷——竞争条件、 死锁、协议违规——在生成代码中变得数学上不可能。

9. 结论：Veriprajna 的承诺

半导体产业再也承担不起「先试再看」的验证方式。 「十法则」规定：实验室发现的缺陷成本是编辑器中发现的缺陷的 10,000 倍。 我们创始人引用的 1000 万美元失误并非异常；它是 将概率工具（LLM）应用于确定性问题 （硬件）而缺乏安全网的必然统计结果。

Veriprajna 就是那张安全网。我们不是封装器。我们不是聊天机器人。我们是 形式化 验证铸造厂 。我们提供唯一尊重硅片 无情物理的生成式 AI 方案。我们以 AI 的速度提供数学的确定性。

对现代芯片设计者而言，选择很明确： 你可以使用聊天机器人，然后祈祷最好结果。 或者使用 Veriprajna，并证明它。

Veriprajna Deep AI. Formal Proof. Zero Respins.

参考文献

1. Large Language Model for Verilog Code Generation: Literature Review and the Road Ahead - Preprints.org, 2025年12月11日访问， https://www.preprints.org/manuscript/202511.0656/v2

2. Former AMD engineer, my first build with an AMD chip that I worked on! - Reddit, 2025年12月11日访问， https://www.reddit.com/r/Amd/comments/jyi8c6/former_amd_engineer_my_first_build_with_an_amd/

3. How to Maximize Productivity and Lower Cost for Enterprise Prototyping Cadence Blogs, 2025年12月11日访问， https://community.cadence.com/cadence_blogs_8/b/fv/posts/how-to-maximize-productivity-and-lower-cost-for-enterprise-prototyping

4. A Winning Formula - Semiconductor Engineering, 2025年12月11日访问， https://semiengineering.com/a-winning-formula/

5. Formal Analysis: A Valuable Tool for Post-Silicon Debug | Electronic Design, 2025年12月11日访问， https://www.electronicdesign.com/news/products/article/21789371/formal-analysis-a-valuable-tool-for-post-silicon-debug

6. The Cost of Finding Bugs Later in the SDLC - Functionize, 2025年12月11日访问， https://www.functionize.com/blog/the-cost-of-finding-bugs-later-in-the-sdlc

7. Automated Regression Testing | The True Cost of Software Bugs in 2025 | CloudQA, 2025年12月11日访问， https://cloudqa.io/how-much-do-software-bugs-cost-2025-report/

8. Rising respins and need for re-evaluation of chip design strategies - EDN Network, 2025年12月11日访问， https://www.edn.com/rising-respins-and-need-for-reavaluation-of-chip-design-strategies/

9. Verification In Crisis - Semiconductor Engineering, 2025年12月11日访问， https://semiengineering.com/verification-in-crisis/

10. The Risk/Reward Realities of Chip Development - Embedded, 2025年12月11日访问， https://www.embedded.com/the-risk-reward-realities-of-chip-development/

11. Large Language Model for Verilog Generation with Code-Structure-Guided Reinforcement Learning - arXiv, 2025年12月11日访问， https://arxiv.org/html/2407.18271v3

12. Race Conditions: The Root of All Verilog Evil - StittHub, 2025年12月11日访问， https://stitt-hub.com/race-conditions-the-root-of-all-verilog-evil/

13. How to avoid a race condition - SystemVerilog - Verification Academy, 2025年12月11日访问， https://verificationacademy.com/forums/t/how-to-avoid-a-race-condition/39103

14. Corner-Case Bug Hunting for RISC-V - Semiconductor Engineering, 2025年12月11日访问， https://semiengineering.com/corner-case-bug-hunting-for-risc-v/

15. Slow Progress On Generative EDA - Semiconductor Engineering, 2025年12月11日访问， https://semiengineering.com/slow-progress-on-generative-eda/

16. Detecting Harmful Race Conditions in SystemC Models Using Formal Techniques - DVCon Proceedings, 2025年12月11日访问， https://dvcon-proceedings.org/wp-content/uploads/detecting-harmful-race-conditions-in-systemc-models-using-formal-techniques.pdf

17. Verilog Races | VLSI Design Interview Questions With Answers - Ebook, 2025年12月11日访问， https://vlsiinterviewquestions.org/2012/07/27/verilog-races/

18. Please help me with a 5 stage Pipeline : r/RISCV - Reddit, 2025年12月11日访问， https://www.reddit.com/r/RISCV/comments/1iny04h/please_help_me_with_a_5_stage_pipeline/

19. From Simulation Bottlenecks to Formal Confidence: Leveraging Formal for Exhaustive RISC-V Verification, 2025年12月11日访问， https://riscv.org/blog/from-simulation-bottlenecks-to-formal-confidence-leveraging-formal-for-exhaustive-risc-v-verification/

20. Satisfiability modulo theories - Wikipedia, 2025年12月11日访问， https://en.wikipedia.org/wiki/Satisfiability_modulo_theories

21. Z3 - Microsoft Research, 2025年12月11日访问， https://www.microsoft.com/en-us/research/project/z3-3/

22. Lessons Learned With the Z3 SAT/SMT Solver - Applied Mathematics Consulting, 2025年12月11日访问， https://www.johndcook.com/blog/2025/03/17/lessons-learned-with-the-z3-sat-smt-solver/

23. SystemVerilog assertions for formal verification - Electrical Engineering Stack Exchange, 2025年12月11日访问， https://electronics.stackexchange.com/questions/737399/systemverilog-assertions-for-formal-verification

24. Assertion-based Verification - GitHub Pages, 2025年12月11日访问， https://uobdv.github.io/Design-Verification/Lectures/Current/9_ABV.v.pdf

25. LAAG-RV: LLM Assisted Assertion Generation for RTL Design Verification - arXiv, 2025年12月11日访问， https://arxiv.org/html/2409.15281v1

26. Faver: Boosting LLM-based RTL Generation with Function Abstracted Verifiable Middleware, 2025年12月11日访问， https://arxiv.org/html/2510.08664v1

27. Revolution or Hype? Seeking the Limits of Large Models in Hardware Design arXiv, 2025年12月11日访问， https://arxiv.org/html/2509.04905v1

28. A Roadmap towards Neurosymbolic Approaches in AI Design - IEEE Xplore, 2025年12月11日访问， https://ieeexplore.ieee.org/iel8/6287639/6514899/11192262.pdf

29. SANGAM: SystemVerilog Assertion Generation via Monte Carlo Tree Self-Refine arXiv, 2025年12月11日访问， https://arxiv.org/html/2506.13983v1

30. achieve-lab/assertion_data_for_LLM - GitHub, 2025年12月11日访问， https://github.com/achieve-lab/assertion_data_for_LLM

31. 1 The Traditional Req/Ack Handshake, It's More Complicated Than You Think! Ben Cohen 9/1/2024, 2025年12月11日访问， https://systemverilog.us/vf/ReqAck90224.pdf

32. Formal And AI Hybrid Techniques For Scalable Verification Of Large System-On-Chips - jicrcr, 2025年12月11日访问， http://jicrcr.com/index.php/jicrcr/article/download/3429/2917/7352

33. RISC-V Formal Verification - Axiomise, 2025年12月11日访问， https://www.axiomise.com/risc-v-formal-verification/

34. Verifying security of RISC-V processors - Embedded, 2025年12月11日访问， https://www.embedded.com/verifying-security-of-risc-v-processors/

35. Thinklab-SJTU/Awesome-LLM4EDA - GitHub, 2025年12月11日访问， https://github.com/Thinklab-SJTU/Awesome-LLM4EDA

36. Understanding and Mitigating Errors of LLM-Generated RTL Code - alphaXiv, 2025年12月11日访问， https://www.alphaxiv.org/overview/2508.05266v1