调研日期：2026-10-08　|　覆盖范围：2026 年（含 2025 年下半年）DAC / ICCAD / DATE / DVCon（US·China·India·Europe）/ ASP-DAC 为主要目标，辅以 MLCAD / ICLAD / ISEDA / MDTS / ICICDT / IJCAI / TACAS / ISCA / ICML / ICLR / NeurIPS workshop，以及 arXiv 预印本
证据分级：【会议录用】 论文 arXiv/DOI 元数据中的录用标注（本报告引述原文）　【预印本】 仅 arXiv　【官方程序】 会议官方页面（本环境多不可达）　【厂商宣称】 厂商新闻稿/博客，未独立验证
数据说明：本次调研期间 web_search 工具因 API 端点鉴权失败不可用（HTTP 401），ACM DL / IEEE Xplore / GitHub / dblp 亦不可达；全部结论基于对 arXiv Atom API、OpenAlex、DOI 系统、会议官网的直接抓取。未能核实的内容在第 7 节逐条列出。
一句话结论：2026 年 LLM 辅助 EDA 验证已从”生成工具”转变为”工具在环的闭环系统“，技术重心是形式/覆盖率反馈 + 门控验收；同时出现一波实证”打假”，证明当前 benchmark 与指标普遍不足以支撑选型决策。

0. 结论速览（TL;DR）

1. 技术重心已从「生成」转向「闭环 + 可信」。2024–2025 年的主流范式是”给定规格，让 LLM 一次性生成 SVA/测试平台”；2026 年的论文几乎全部把 仿真器/形式验证工具放进循环（JasperGold、SymbiYosys+Z3、Pono、Yosys、Verilator、Calibre），并引入反例（CEX）、覆盖率、语法诊断三类反馈。
2. SVA/断言生成是竞争最激烈、也最”卷”的赛道，且已经被做透到需要”数据合成 + 强化学习”才能提升的地步（如 QiMeng-CodeV-SVA 在 DAC 2026、RWOPD 用性质等价检查器做奖励）。指标也从”语法通过率”转向 形式可证明率、非空洞率（non-vacuous）、变异覆盖率、形式覆盖率。
3. 2026 年出现了一批”打假”论文，这是该领域成熟的标志：GateTruth 用变异测试审计 RTL benchmark，发现 RTLLM v2.0 有 72% 的设计未达到 95% 变异杀伤下限；另一篇 DAC/预印本工作证明”语义等价的 RTL 改写”会让 9.7%–27.0% 的 LLM 断言从正确变错误。“点准确率”已被证明不足以刻画 LLM 在验证中的可靠性。
4. 多智能体（multi-agent）成为默认架构：ChatSVA（DAC 2026）、UVMarvel（DAC 2026）、CHARGE（ICCAD 2026）、Knowledge-Graph agentic FV（ICICDT 2026）等，普遍采用”规格解析 agent + 生成 agent + 工具执行 agent + 修复 agent”的分工。
5. 形式验证侧已分化为四条路线：① LLM 作为搜索启发式（LLM4PDR 给 PDR 生成谓词/子句/辅助断言，实现在 Pono 中解出 28/33 算术基准）；② LLM 作为证明工程师 + 内核门控（乱序多处理器在 Rocq 中机械化证明；Rtl2lean 把 RTL 翻成 Lean 4，403 条定理全部通过内核检查）；③ 神经符号修复（NeuroAssertion 用 SyGuS 保证可合成性，NeuroAbs 用 SMT 校验抽象可靠性 + CEGAR）；④ 证书/反例门控（IC3-Evolve 要求 SAFE 附可独立校验证书、UNSAFE 附可重放反例）。
6. 安全验证是增速最快的子领域：CHARGE（ICCAD 2026）用 CWE 层次结构生成安全 SVA，Hack@DAC18/19/21 上检出 27/42 个已知缺陷并新发现 1 个；ATLAS（DAC 2026）从 CWE 威胁模型推导 SoC 安全断言，检出 39/48 个 CWE、为 33 个 bug 生成正确属性；AutoTrans 专门防安全断言的”信号幻觉”。三条共识：CWE/威胁模型是最好的知识源、必须报非空洞率、断言生成必须能抓到 bug 而不只是”编译通过”。
7. 工业界的真实数据仍然稀缺。DVCon U.S. 2026 有明确的 “AI & ML in Verification”、”AI & ML Coverage Closure”、”Testbench Generation” 技术分会，Synopsys/Cadence/Siemens 三家均已发布 agentic 验证品牌（AgentEngineer / ChipStack AI / Questa One）；但第三方复现的工业级基准在 2026-10 之前不存在，可公开验证的量化收益主要来自厂商自述（见第 5 节与第 7 节）。
8. 最值得警惕的一条实证结论：一项自审研究显示，1,857 条被模型 provider 接受（通过 schema 校验）的回复中，只有 9 条通过真实验证器；另有研究表明未分级的 agent + verifier 组合能在 50% 精确率下”证明”98% 的已知有 bug 程序。“编译通过””验证器说通过”都不能作为验收依据。

1. 2026 年相关会议时间线与程序公开状态

要点：

• 截至 2026-10-08，DAC 2026（7 月，已闭幕）与 DVCon U.S. 2026（3 月，已闭幕）是完成度最高的两个会议；ICCAD 2026（11 月）尚未公布论文表；DATE 2026 论文集已出版但官网程序页不可读。
• 因此本报告对”今年顶级会议”的判定采用三级证据：【会议录用】（作者 arXiv 标注，可逐条引用）> 【官方程序】（会议官方页面）> 【预印本】。凡标注为录用但无官方程序交叉验证的，均在文中明确写出其证据级别。
• 重要局限：多数 DAC/ICCAD/DATE/DVCon 论文不上 arXiv，因此本报告的论文清单是”可在线验证的子集”，不是完整录用列表；完整列表需等 ICCAD 2026 论文表发布与 ACM DL/IEEE Xplore 可访问后才能补齐。

1.1 ⚠️ 用 arXiv comment 字段做会议归属的两个陷阱（方法论，必读）

本报告大量依赖论文作者在 arXiv 元数据里的录用标注。专门的归属统计（venue-attribution.md）证明这个字段既少算也多算，务必按”下界/上界”理解本报告的计数：

陷阱一：少算（漏报）

• 2511.13139（Backtrack-ToT） 在 OpenAlex/Crossref 里是 DATE 2026 正式论文，但其 arXiv comment 只有 “6 pages, 5 figures”——毫无会议信息。
• FVDebug（2510.15906） 在 DVCon 会议论文库中确认是 DVCon U.S. 2026 论文，但 arXiv 页面上完全没有 venue 字段（无 Comments、无 journal_ref）。
• → 任何基于 comment 的会场计数都只是下界。

陷阱二：多算（误报）

• 投稿被写成”已录用”：2512.06537 写 “Submitted to DAC 2026”、2605.27757 写 “Submitted to ICCAD 2026”、2605.05786 与 2509.20138 写 “submitted to CAV 2026”——这些都不是录用。
• 工作坊/特邀/特别研究分会冒充主会："Invited paper at the DAC 2026 Special Research Session"、"40th NeurIPS'26 Workshop"、"AIMACS workshop at CAV 2026"、"ICLAD 2026, Long Oral" 全部自称 accepted，但都不是主会论文。
• → comment 无法告诉你是主会 / 工作坊 / 特邀 / 短文 / 海报，也无法告诉你录用日期、是否被撤稿、arXiv 版本是否等于 camera-ready。

两个具体的检索陷阱：

• all:"DVCon 2026" 在 arXiv 返回 0 条——该字面串根本不存在（因为加了 U.S./Europe/India/China 后缀）。必须用 all:"DVCon" 再人工筛。
• all:"ITC 2026" 的 9 条命中全是引用 ITCS 2026（理论计算机科学）的密码学论文，与 IEEE International Test Conference 无关——别用这个查询找测试会议的工作。

一个重要的负面发现：FMCAD 2026（5 条命中）与 CAV 2026（22 条命中）中，硬件/EDA 功能验证论文数为 0。FMCAD 命中的全是通用形式方法/求解器/DNN 验证；CAV 命中的全是软件验证、分布式算法、概率模型检查、神经网络验证。这说明”LLM 辅助硬件验证”目前几乎完全发生在 EDA 会议（DAC/ICCAD/DATE/ASP-DAC/DVCon/MLCAD/ICLAD/ISEDA），而非形式方法会议——如果你要找”形式方法社区的严肃工作”，方向可能选错了会。

2. 技术地图：八条主线与代表工作

2.1 主线一：断言 / SVA 生成（最热，已进入”内卷”阶段）

这一主线的共识与分歧：

• 共识：必须有工具在环（形式证明器或仿真器反馈），纯 prompt 方案已到天花板。
• 分歧：提升性能的杠杆是”数据“（ChatSVA / CodeV-SVA）还是”搜索/反馈“（ProofLoop / NeuroAssertion / KG-agent）还是”训练目标“（RWOPD）——2026 年三条路线都有 SOTA 主张。

2.2 主线二：形式验证、模型检查与证明自动化

2.3 主线三：测试平台 / UVM / 激励生成

这一主线的关键洞察 —— “不要让 LLM 写 HDL”：

• HAVEN、UCAgent 两条独立路线给出了同一个反直觉结论：让 LLM 写 UVM/SystemVerilog 是错误的设计选择。HAVEN 用”LLM 解析规格 → 模板引擎生成 UVM”达到 100% 编译成功；UCAgent 直接用纯 Python 验证环境（Picker + Toffee）绕开 SystemVerilog，达到 100% 功能覆盖率。两者都把 LLM 的角色限制在”理解规格 + 决策”，把”代码正确性”交给确定性的模板/框架。
• GoGoTB 的”确定性执行层 / LLM 推理层”分离是同一思想的另一种表达（在工具与阶段边界上分离确定性强制与 LLM 推理）。
• 对工程团队的直接建议：如果你的 LLM 验证流程产出的是语法错误频发的 SV 代码，架构可能选错了，而不是模型不够强。

2.4 主线四：覆盖率闭环（形式覆盖率 / 功能覆盖率 / 变异覆盖率）

这是 2026 年度量标准换代的主战场：

• 从”语法通过率”到”非空洞 + 形式覆盖率 + 变异杀伤率”：ICICDT 2026 的 KG-agent 工作报形式覆盖率 78.5%–99.4%；MLCAD 2026 的 NeuroAssertion 用变异覆盖率（约 2×）；ISEDA 2026 的 SVA Generator 用”性质等价率”。
• HierSVA（预印本 2026-06）把断言质量拆成 6 个轴：语法正确、断言证明成功率、空洞性（vacuity）、规格忠实度、变异覆盖率、形式核心覆盖率。在 BaseJump STL 上构建 342 个模块（层次深度 0–9）的数据集与 benchmark。实测：模块级编译率 67.1%；可评估运行中 82.1% 的断言非空洞证明；但这些断言集只检出 70.2% 的可注入故障、覆盖 36.2% 的形式核心；深层子集上”标记有缺陷 RTL”的召回 0.87 但精确率仅 0.60（40% 的”预测有缺陷”是正确 RTL 上的误报）；agent 模式能提升可证明性与强度，但收益会平台化甚至振荡。
• CoverAssert（+9.57% 分支 / +9.64% 语句 / +15.69% 翻转覆盖率）用功能覆盖率反馈驱动断言补全。
• CovR 用仿真覆盖率作为 RL 奖励，是”覆盖率闭环”最完整的工程化实现（cov@10 93.81% / 87.76%，完整流程覆盖率 +18.95%）。
• GoGoTB 把每个覆盖率 bin 绑定到一条规格行为——这是解决”覆盖率闭合了但没验证到东西”这一经典问题的语义化思路（行/分支/翻转 98.4% / 97.2% / 97.0%）。
• Spec2Cov 给出了最重要的现实数据点：26 个设计中，简单设计覆盖率可达 100%，复杂设计只有 49%。这条”复杂度悬崖”比任何 SOTA 数字都更能说明当前技术水平。
• Token Allocation & Coverage Limits 提出了覆盖率空洞的分类学：一类是”方法学天花板“（在这个抽象层次/激励空间下根本不可达，再多推理也没用），一类是”推理前沿“（模型能力不足）。这个区分对工程排期极其有用：前者应该改验证计划，后者才值得加算力。
• RL 与专用小模型正在取代通用大模型：CHORUS 把多个 SFT/RL 专家合并为 4B 模型，CVDP-ECov Pass@1 达 88.0%，超 DeepSeek-R1 671B 13.5 个百分点；LLM4Cov 用离线智能体学习达到 69.2% 通过 / 90.4% 覆盖率；CovR 用工具奖励微调。结论：在验证这类”有确定性反馈信号”的任务上，4B 专用模型 > 671B 通用模型。

2.5 主线五：调试、波形与根因分析

2.6 主线六：安全验证与硬件安全

• CHARGE（ICCAD 2026） — CWE 层次的推理式安全性质生成，是当前最完整的开源 SoC 安全断言工作（Hack@DAC18/19/21，27/42 缺陷，89% 可在 JasperGold 运行，92.2% 非空洞）。
• ATLAS: AI-Assisted Threat-to-Assertion Learning for System-on-Chip Security Verification（DAC 2026，DOI 10.1145/3770743.3804400，arXiv 2603.01170）— 从 CWE 威胁模型推导 SoC 安全断言与 JasperGold 脚本；3 个 HACK@DAC 基准检出 39/48 个 CWE，为 33 个 bug 生成正确属性。与 CHARGE 并列为 2026 年最重要的两项”LLM 安全断言生成”工作。
• Assertain: Automated Security Assertion Generation Using Large Language Models（MDTS 2026，预印本 2026-04）— 融合 RTL 分析 + CWE 映射 + 威胁模型情报，配自反思精修；11 个硬件设计上相对 GPT-5：正确断言生成 +61.22%、CWE 覆盖 +59.49%、架构缺陷检出 +67.92%。
• LAsset（DATE 2026，DOI 10.23919/date69613.2026.11539092，Univ. of Florida）— LLM + 结构/语义分析从规格与 RTL 两侧识别主/次安全资产，并推导模块间依赖关系；把”安全资产识别”定位为硅前安全验证的第一步，向下游驱动威胁建模、性质生成与漏洞检测。摘要原文：“up to 90% recall for intra-module asset classification/identification and 93% recall at SoC design level”。（该数字经第二轮独立调研核实，来源为 DATE 2026 的 DOI 索引会议摘要，非付费墙全文。）
• LASA: Enhancing SoC Security Verification with LLM-Aided Property Generation（arXiv 2506.17865）— LLM 辅助的性质生成，覆盖率约 88%，在 Hack@DAC’24 OpenTitan 上发现 5 个独有缺陷。
• MARVEL: Multi-Agent RTL Vulnerability Extraction using LLMs（arXiv 2505.11963）— 多智能体 RTL 漏洞抽取，面向 Hack@DATE 的 SoC。⚠️ 最值得引用的一个数字：报告 51 个问题，其中 19 个有效、14 个告警、18 个是幻觉（35%）——幻觉率已被直接测量在安全验证流水线内部。
• ThreatLens: LLM-guided Threat Modeling and Test Plan Generation for Hardware Security Verification（arXiv 2505.06821，VTS 2025）— 从威胁建模到测试计划生成，NEORV32 平台。
• Security Properties for Open-Source Hardware Designs（arXiv 2412.08769）— 面向 OR1200 与 Hack@DAC 2018/2019/2021 的开源安全 SVA 语料库（是这一领域的公共基准基础设施）。
• (Security) Assertions by LLMs（arXiv 2306.14027，IEEE TIFS 2024）— 该方向早期代表工作，也是少数在 arXiv 元数据中自带作者单位的记录。
• Translating Common Security Assertions（arXiv 2502.10194）— 常见安全断言的形式化翻译，跨 5 个安全模块接近 100% 翻译成功率，并用 LLM 定义的木马做验证。
• AutoTrans: AI-Assisted Automatic Translation of Security Assertions for RISC-V Processors（arXiv 2609.10057）— 把安全断言跨核迁移，专门防”信号幻觉”（安全断言里引用不存在的信号是致命错误）；自动接受率 78%，每一条都由 JasperGold FPV 把关。
• ADVERSARIAL: And-Inverter Graph-Assisted Hardware Trojan Detection At Scale（ICCAD 2026，arXiv 2607.23882）— ⚠️ 更正：该工作并非 LLM 方法，而是用 And-Inverter Graph 的知识图谱嵌入做大规模硬件木马检测。列在此处仅供”硬件木马检测现状”参照，不应算作 LLM 工作。
• RTLGuard: A Lightweight Teacher-Student Defense for Poisoned RTL Code Generation Models（ICCAD 2026）— 面向”被投毒的 RTL 生成模型”的防御，属于”AI 供应链安全”，与验证交叉。
• Robustness of LLM-Generated SVA to Semantics-Preserving RTL Transformations（预印本 2026-09）— 不是安全论文，但结论对验证可靠性至关重要，见 §4。

这一主线的判断：安全验证是 2026 年增速最快、工业需求最刚性的子领域（Hack@DAC 这类竞赛提供了现成的量化基准）。三条技术共识已经形成：① CWE/威胁模型是安全性质生成的最佳知识源（CHARGE、ATLAS、Assertain 都走这条路）；② 必须声明非空洞率，否则生成的”安全性质”可能永远为真、毫无保护作用（CHARGE 报 92.2% 非空洞是正面示范）；③ 幻觉已经在安全流水线内部被直接测量——MARVEL 在 Hack@DATE SoC 上报告 51 个问题里 18 个是幻觉（约 35%），AutoTrans 明确命名”信号幻觉”并工程化规避。“LLM 报了一个安全漏洞”的默认可信度约为 2/3，必须逐条过形式验证。

⚠️ 一条引用纪律：Assertain 报出的”相对 GPT-5 +61.22% / +59.49% / +67.92%”是依赖 LLM 自反思（self-reflection）而非求解器门控得到的。这类数字度量的是”生成质量”，不是”验证可靠度”，不能与 CHARGE/ATLAS 的求解器门控结果并列比较。 这是 2026 年新出现的一种反模式。

2.7 主线七：规格自动形式化（支撑所有主线的基础设施）

• 规格自动形式化是 2025–2026 新增的基础设施层：DRAM 标准 → DRAMPyML + DRAMBench（ICLR 2026 Verif-AI Workshop）、CNL 规格 → FPV Gherkin 场景。
• 五个”疑似不存在”的名称，处理如下（含一次实际的交叉核对）：
  • AssertLLM2（arXiv 2605.27472）确实存在。我直接抓取了 arXiv Atom API，完整读到其标题与摘要（83 个真实设计 / 13 个功能类别 / 首次以带缺陷 RTL 作为输入）。⚠️ 另有一个并行调研小组因检索时遇到接口限流，得出”AssertLLM2 不存在”的结论——该结论是错的，正确的参照是我方的直接元数据抓取。
  • FVBench 很可能不存在：ti:"FVBench" 在 arXiv 返回 0 条命中。请勿引用这个名称。
  • VeriBench（硬件版）：多个检索路径均未命中，本报告不引用。
  • RTLLM v2.0 的原始论文：被大量论文用作主 benchmark，但原始论文未检索到；引用其分数时请注明来源是该论文的二次引用。
  • Hack@DAC 2025/2026 的官方成绩榜：arXiv 上不存在竞赛结果论文；ATLAS / CHARGE / LASA 在 Hack@DAC 上的数字均为论文自报，未与官方成绩榜交叉核对。
• 裁定标准：凡遇到不同轮次调研或子报告之间的结论冲突，一律以”能否直接读到元数据/摘要原文“为准，并以逐字引述作为记录依据。本报告据此更正过两次：AssertLLM2 存在性（我方对）、LAsset 召回数字（第二轮对）。
• LLM for EDA in Front-End Design: Challenges and Opportunities（DAC 2026 特别研究分会特邀论文，arXiv 2607.09616）— 前端设计（含 testbench 构建与 agentic EDA）中 LLM 的挑战与机会综述。
• DRAMPyML as Timed Petri Nets（arXiv 2602.10654）— DRAM 自动形式化工作底下的非 LLM 形式化基座（时序 Petri 网模型）。理解 Autoformalizing Memory Specs 那条线时要知道：真正保证语义的是这个 Petri 网表示，LLM 只负责把自然语言映射进去。
• ⚠️ AMBA/AXI 协议规范的自动形式化：除 FLAG（arXiv 2504.17226）外未找到第二篇经核实的工作。独立检索 AMBA+LLM 得到的全是误命中（例如撞到某作者姓氏）。不要把”协议自动形式化已经很成熟”作为前提。

2.8 主线八：硬件木马攻防（2026 年新增的独立战场，且双方都不用形式方法）

这是第一轮调研完全遗漏的一整条轴。2026 年它演变成一场真正的双向军备竞赛：

攻击侧（用 LLM 生成/插入木马）

防御侧（正在转向”模型供应链安全”）

• RTLGuard（ICCAD 2026，DOI 10.1145/3831252.3834219，arXiv 2608.26049）— 威胁模型是”第三方微调的 RTL 生成模型内嵌后门”；防御用干净小教师模型 + 特征对齐 + 知识蒸馏压制恶意行为，避免全参数重训。
• SafeTune（IEEE VTS 2026，arXiv 2604.27238）— GNN 检测异常电路 + 语义验证（embedding + XGBoost）过滤被投毒的微调数据，不改模型架构。
• Semantic Consensus Decoding（arXiv 2602.04195）— 把攻击成功率从 89% 压到 <3%。
• HarmChip（arXiv 2604.17093）— 硬件安全 jailbreak benchmark：16 个领域 / 120 种威胁 / 360 条提示；发现”对齐悖论“——模型拒绝正当的安全查询，却配合语义伪装过的攻击。

这一主线的判断：① 木马攻防双方都没有使用形式方法——这是一个显眼的空白，考虑到验证领域的其余部分都在向”求解器/内核门控”收敛；② 攻击侧的进展（CITADEL 的”仿真不可见”、TrojanGYM 的 68.75% 规避）快于防御侧；③ 防御的重心正在从”检测 RTL 里的木马”转向”防止模型被投毒“，这本质上是 AI 供应链安全而非传统验证——如果你的团队在用第三方微调的 RTL/验证模型，这是 2026 年必须评估的新风险面。

3. 重点论文速查表（共 80 条，按”与 LLM 辅助验证的相关度”排序）

4. Benchmark 与”评测危机”（2026 年最重要的元趋势）

4.1 新一代 benchmark

4.2 十一条”打假”结论（务必在内部汇报时强调）

1. GateTruth（2608.12635）：用变异测试审计 RTL benchmark 的 testbench 严格性。自建 68 任务双轨套件中，60 个 Track A testbench 里 46 个能杀掉 ≥95% 变异体，其余 14 个被作者如实披露原因（含”为通过本关卡而被修订的 testbench 产生的 Goodhart 效应”）。同样引擎原样指向 RTLLM v2.0：46 个可审计设计中 72% 低于 95% 下限，3 个为 0%。NVIDIA CVDP 因公开版本不提供参考解，结构上无法做此审计。另外发现：统一的 4096 token 输出上限曾静默截断 7 个被测模型中的 3 个，改成 16,384 后某模型从第 5 名升至第 1 名。
   → 含义：现有 RTL/验证 benchmark 的排名可能不可靠。
2. 语义保持变换鲁棒性（2609.05658）：对 VERT 数据集做受控变形测试（操作数重排、标识符重命名、冗余括号）。在 6 组”模型 × 变换”条件下，9.7%–27.0% 原本正确的行为在语义等价改写后变错。例如标识符重命名下 DeepSeek-Coder-V2-Lite 总体准确率从 53.9% 升到 63.7%，但其中 19.5% 原本正确的行为失效——聚合准确率掩盖了严重的不稳定性。人工复核 30 个”对→错”样本，归因于丢失路径谓词、分支极性错误、布尔结构损坏、输出契约违反。
   → 含义：”点准确率”不足以刻画 LLM 断言生成的可靠性，需要鲁棒性感知的评测。
3. HierSVA（2606.13706）：即使断言 82.1% 非空洞可证明，也只能检出 70.2% 的可注入故障、覆盖 36.2% 的形式核心；”报告有缺陷”的精确率仅 0.60。
   → 含义：断言”能证明”≠”能抓到 bug”，验证有效性的度量必须包含变异/形式核心覆盖率。
4. “有验证器”不等于”安全”（NFV 研究）：未分级的 agent + verifier 组合在 50% 精确率下”证明”了 98% 的已知有 bug 程序；Assertain 等依赖自反思验收的工作明显弱于求解器门控；Benchproofer 明确指出薄弱环节是”规格”本身而不是证明器（25% 通过测试的补丁实际存在反例）。
   → 含义：门控必须分级 + 对抗性校验，”验证器说通过”不能作为唯一验收依据。
5. 已知危害最大的失效模式排名（按实测证据强度）：
   ① 空洞断言（永远为真、零保护）> ② 规格本身写错（门控再严也无效）> ③ 语法/编译通过但执行无效（1,857 → 9）> ④ 语义保持改写导致失效（9.7%–27.0%）> ⑤ 规格幻觉/信号幻觉（AutoTrans 专门防这个）
   → 含义：验收优先级应从”能不能编译”彻底转向”断言是否非空洞、规格是否正确”。
6. 被撤回与被质疑的论文（务必注意）：
   • AgentDV: Closed-Loop Agentic AI for Hardware Design Verification（arXiv 2608.27148）已被作者主动撤回。arXiv 元数据中的原文为：”The authors are withdrawing this preliminary manuscript due to errors in the methodology and experimental setup in Section 4 and 5. The work is undergoing a comprehensive revision and re-evaluation.” → 该论文的任何数字都不得引用。
   • Trust, but Validate the Instrument（arXiv 2609.19844） 是一篇重要的”工具自审”论文：31 个任务 / 124 条自撰硬件安全回归用例，确定性非 AI 基线在递增资源下分别杀死 36、75、78 个变异体；作者明确报告”未能给出 prompt 效应估计”，并把失败运行保留为”工具验证事故”，主张 provider 或 schema 接受 ≠ 执行有效，编译与覆盖率只是诊断信号，不能作为验证有效性的证据。
   • ICLR 2026 审稿人对某模型在 VerilogEval-Machine 上的高分明确提出数据污染质疑〔此项未能独立复核，标记为待核实〕。
   • GateTruth 另发现：统一的 4096 token 输出上限会静默截断 7 个被测模型中的 3 个，放宽到 16,384 后某模型从第 5 名升至第 1 名。
     → 含义：引用任何 LLM-EDA 结果时，应先确认该论文是否仍有效、评测配置（输出上限、prompt、解码参数）是否公开，以及有无数据污染声明。
7. 最令人警醒的一个数字（SecTB-RTL，2609.19844）：在一个 31 任务 / 124 条自撰硬件安全回归用例的实验中，1,857 条被模型 provider 实际接受（通过 schema 校验）的回复里，只有 9 条通过了真实的验证器。作者由此主张：“provider 接受了”或”schema 通过了”完全不等于”执行有效”，编译成功与覆盖率数字只能当诊断信号，不能当作验证有效性的证据。
   → 含义：所有以”编译通过率/语法通过率”为主指标的 LLM 验证论文，其数字与真实工程有效性之间存在巨大鸿沟。
8. 超参数敏感性足以颠覆结论：研究显示评测配置变化可让同一模型的 pass 率摆动 25.5 个百分点（arXiv 2604.17102）；GateTruth 也证明输出上限设置改变了模型排名。VerilogEval 上前沿模型停在 90.8%，且残余失败被归因为”不可解的功能错误”而非能力不足（arXiv 2606.19347）。
   → 含义：跨论文比较 SOTA 数字在 2026 年基本不可靠，除非评测配置完全公开且一致。
9. 新反模式：”用自反思代替求解器门控”：Assertain 的高分（相对 GPT-5 +61.22% / +59.49% / +67.92%）来自 LLM 自反思，而非求解器/内核裁决。这类数字度量的是生成质量，不是验证可靠度，不能与 CHARGE / ATLAS / IC3-Evolve 的求解器门控结果并列比较。
   → 含义：读论文时先确认”正确性由谁判定”。如果判定者还是 LLM，这份结果不能用于采购决策。
10. 幻觉率已被直接测量在安全流水线内部（MARVEL，2505.11963）：在 Hack@DATE 的 SoC 上报告 51 个问题，其中 19 个有效、14 个告警、18 个是幻觉（约 35%）。“LLM 报了一个安全漏洞”的默认准确率约为 2/3。 另有 TrojanWhisper 揭示系统性不对称：LLM 定位木马 trigger 的覆盖 0.82–0.98，但 payload 只有 0.32–0.46。
    → 含义：安全验证场景下 LLM 的每条告警都必须过形式验证，且”找到触发条件”不等于”定位到载荷”。
11. 收益不累积——agentic 循环存在隐性天花板：harness 演化把”完成的尝试数”提到 71–76%、”命中过至少一次的任务覆盖率”提到 80–100%，但**”正确尝试数”只提升 18–24%**（arXiv 2609.28908）。这与 HierSVA 的”agent 模式收益平台化甚至振荡”结论一致。
    → 含义：不要用”任务覆盖率/尝试成功率”作为 agent 有效性的证据，必须看”正确率”。

5. 工业界与开源

5.1 三大 EDA 厂商的 agentic 验证布局（均已核实公告存在与日期；能力叙述属厂商营销）

5.2 中小厂商 / 初创的真实声音（比大厂新闻稿更有信息量）

• Axiomise：spec → SVA 草稿”数百条属性从数天缩短到数分钟“，但同时警告 false confidence、空洞属性、以及评审成本可能反超节省——这是本报告所见最诚实的厂商表述。
• ChipAgents（Alpha Design AI）：波形调试与自主根因分析；2026-08-09 报道融资 1.34 亿美元；客户 Whalechip 称”根因分析压缩到分钟级”（厂商博文，未独立验证）。
• Moores Lab AI：AXI-to-APB 桥”一行代码不写”完成全套 testbench 与覆盖率收敛，48 小时 vs 传统两个月（厂商宣称）。
• Normal Computing：auto-formalization + ontology，主张需要 AI-native 形式工具，并坦承”是否真省工程师时间目前不清楚”。
• KeySilicon / Breker：用 AI 在 RISC-V 规范中定位功能点”非常成功”，再由 PSS 后端生成测试，失败可回标注到测试/验证计划/规范。
• Arteris：主张”关键指标不是生成了多少代码或测试，而是能否更快达到签核信心、减少硅后逃逸“。
• Keysight EDA / AMIQ：只核到专家观点——模拟 IP 几乎没有公开语料、首次使用”更慢更差”；以及准确性/非确定性/成本顾虑。

5.3 标准与联盟（一个重要负面发现）

• Accellera 的 17 个活跃工作组中，没有任何 AI/LLM 工作组。 AI 只以 DAC 2026 圆桌与 DVCon 主题演讲的形式出现；实际推进的是 PSS 3.0、CDC/RDC 1.0（2026-03-02 批准发布）、UVM/UVM-MS、功能安全白皮书。
• 标准化的工具调用接口（MCP 等）：零证据。 即目前不存在”EDA 工具 agent 接口”的行业标准，各家自建。这对工具厂商是机会，对用户是锁定风险。

5.4 开源 / 学术可及工具

• AssertLLM（单设计 89% 断言正确）→ AssertMiner → CoverAssert（+9.57/9.64/15.69%）→ AssertLLM2（2026 benchmark）
• AutoSVA（2021）及其 GPT-4 扩展（在 CVA6 上发现真实缺陷）
• RTLFixer（98.5% 编译错误修复；VerilogEval pass@1 +32.3%/+10.1%）
• FVDebug、Saarthi、HAVEN、UCAgent、STG、VeriPilot、VeriTrace、ChipMEM、ChipFuzzer（均见 §2、§3）
• AssertionBench + AssertionLLM（DATE 2025）— 结论是”商用 LLM 尚不可用于生产”，是一个重要的负面基准。
• 中国团队已有商业化在线服务：ChatSVA 论文标注 https://www.nctieda.com/CHATDV.html（CHATDV）；其作者群与 QiMeng/CodeV 系列（中科院计算所）有交叉。这是本报告所见唯一由论文作者直接运营的 SVA 生成服务。
• 工业界真实采纳的最强信号：DVCon U.S. 2026 设有专门的 AI/ML 验证分会——“Session 3: AI & ML in Verification”、”Session 5: AI & ML Coverage Closure”、”Session 11: Testbench Generation”、”Session 9: Coverage Modeling”、”Session 6: Regression Management”（来源：dvcon.org 分会页标题。⚠️ 站点正文为前端渲染、且已切换为 DVCon U.S. 2027，分会年份归属未能从正文确认；DVCon 论文全文只有 PDF，本环境无法读取）。

5.5 “厂商营销” vs “可独立验证”（引用纪律）

• 属于营销、不可作为事实引用：AgentEngineer/Autopilot 的能力叙述、Cadence “Level-5”、48 小时 vs 两个月、分钟级 RCA、”ROI 压倒性正面”、”10X 生产率”标题、Cadence 在 DVCon China 宣称的 >70% 效率提升、Axiomise 在 DVCon India 宣称的 >99% 穷尽证明、Real Intent 宣称的”违规报告精确度提升 20 倍、评审负担下降 95%”。
• 可独立验证的只有：产品与公告的存在及日期；Accellera 无 AI 工作组；Wilson Research 调研的持续存在；以及学术论文的标题/日期/自报数字（且是自评基准，非第三方复现）。
• 核心结论：截至 2026-10，不存在任何第三方复现的工业级 LLM 验证流程基准。 这也是本报告建议内部自建评测、而非采信任何厂商 ROI 数字的直接理由。

6. 趋势判断与建议

6.1 十六条技术判断

1. 闭环是入场券：2026 年没有工具在环的纯 prompt 方案已很难发表。闭环的三类信号按价值排序：形式反例（CEX）> 覆盖率空洞 > 语法诊断。
2. 度量体系正在换代：语法通过率 → 形式可证率 → 非空洞率 → 变异杀伤率 → 形式核心覆盖率。采购/自研评估时，只看 pass@1 会被误导。
3. 强化学习正在进入验证：CovR（覆盖率奖励）、RWOPD（性质等价奖励）代表”用工具输出的确定性信号训练模型”，比人工标注更可扩展。这是 2026 年最值得跟进的技术方向之一。
4. 神经符号是解决”幻觉/不可合成”的工程解：NeuroAssertion 用 SyGuS 约束符号合成、NeuroAbs 用抽象、RWOPD 用 PEC 做奖励，本质都是”LLM 只提建议，符号工具保正确“。
5. 多智能体架构已趋同：分工大体是「规格/上下文解析 → 生成 → 工具执行 → 诊断修复」，差异在于上下文载体（知识图谱 / AST 索引向量库 / 结构化 IR）。
6. 工业级规模仍是硬边界：多数工作的实验对象是模块级或子系统级 RTL；ICCAD 2026 的 KG-agent 工作也明确承认复杂时序与算术推理仍受限于 LLM 能力；Spec2Cov 更直接量化了这条边界——复杂设计覆盖率只有 49%。
7. “专用小模型 > 通用大模型”在验证任务上已被反复验证：CHORUS（4B 超 671B 13.5pp）、LLM4Cov、CovR、QiMeng-CodeV-SVA（14B 追平 GPT-5）。原因是验证任务有确定性的工具反馈可以做 RL/蒸馏，而通用大模型的能力无法直接转化为验证正确性。选型时不要迷信参数量。
8. “混合”路线（LLM 做语义、传统工具做搜索）性价比最高：ChipFuzzer 不做完整 testbench 而只做 fuzzing 语义引导，取得条件覆盖率 +5.8pp、缺陷检出率 +21.1pp；VSpector 直接拿官方规格审 RTL，找到 42 个新缺陷而传统 fuzzer 24 小时零命中。LLM 的价值在”理解规格与语义”，不在重复传统工具的搜索。
9. 瓶颈常常是基础设施而非模型：BTTF 论文统计出 74.6% 的 LLM-EDA 工作只做静态 RTL 生成，几乎不碰真实工具链；并主张把仿真 dump 转成 SQLite 让 agent 用 SQL 查询（150 查询 95.33% 准确）。对工程团队的直接启示：先把波形/日志/覆盖率数据变成 agent 可查询的结构化形式，收益可能大于换更强的模型。
10. 形式验证领域的”门控（gating）”范式值得借鉴到所有子领域：IC3-Evolve 要求 SAFE 结论必须附带可独立校验的证书、UNSAFE 结论必须附可重放的完整反例；SLED-IFV 让求解器做唯一裁判（最高 603× 加速）。“LLM 提议、工具裁决、结论可复现”应成为采纳 LLM 输出的统一验收标准。
11. “不要让 LLM 写 HDL”正在成为架构共识：HAVEN（模板引擎生成 UVM，100% 编译成功）、UCAgent（纯 Python 验证环境，100% 功能覆盖率）、GoGoTB（确定性与推理分层）三条独立路线得出同一结论。把 LLM 限定在”理解规格 + 决策”，把代码正确性交给确定性框架或模板。
12. 评测危机是本年度最重要的元趋势：GateTruth 证明 RTLLM v2.0 的 72% 设计未达 95% 变异杀伤下限、3 个为 0%；语义保持变换使 9.7%–27.0% 的”正确”断言失效；CVDP 因不公开参考解而结构上无法审计。2026 年读论文时，”在 X benchmark 上达到 SOTA”这句话的信息量已经大幅下降。
13. “内核门控（kernel gating）”是形式验证侧最硬的技术路线：Rtl2lean 把 RTL 翻译为 Lean 4 可执行模型，403 条定理全部通过 Lean 内核检查、80.2% 引理可复用；CktFormalizer/CKTLEAN 在 Lean 内嵌类型化硬件基础设施，引入证明状态反馈（而非仅编译器诊断）后等价证明完成率从 53.3% 提升到 63.3%；Trivet 要求每个判定由 Lean 内核检查，EquiVM 产出可重放的机器可检查证书。LLM 从”写证明”变成”探索证明空间”，正确性由内核兜底。
14. 但”有验证器奖励”本身并不安全——NFV 反例值得所有人警惕：一项研究表明，未分级的 agent + verifier 组合在 50% 精确率下”证明”了 98% 的已知有 bug 程序。另有工作（arXiv 2604.15149，LLMs Gaming Verifiers: RLVR can Lead to Reward Hacking，⚠️ 尚未获取全文，仅作线索）指出带验证器奖励的强化学习会导致奖励作弊。这对 CovR / RWOPD 这类”用验证器奖励做 RL”的路线是直接的警示：门控必须分级、防作弊，且必须保留独立的对抗性检查。
15. LLM 尚未在”纯形式方法”赛道站稳——这既是空白也是机会：FMCAD 2026 与 CAV 2026 的全部命中里，硬件/EDA 功能验证论文数为 0。反过来看，EDA 会议里的 LLM 形式验证工作普遍缺少形式方法社区最看重的东西（可判定性论证、复杂度分析、与 SOTA 求解器的严格对比）。把 EDA 会议里的 LLM 启发式拿去做严格的形式化分析，是目前明显没人做的富矿。
16. “LLM 引导搜索” vs “学习引导搜索”的对立是最值得关注的对照实验：LLM4PDR（LLM 生成谓词/子句/断言引导字级 PDR，33 个算术基准解出 28 个，原版 Pono 13 个）对 AutoPDR（图学习预测 PDR 求解器配置，ISEDA 2026）——同一个目标、两条对立路线，但两者并未互相比较。谁能先把这两条路线放在同一基准上做严格对比，谁就能定义这个子领域。同理，SecIC3（DATE 2026，非 LLM，针对自复合结构定制 IC3 做非干涉证明，最高 49.3× 加速）是任何 LLM 安全验证方案必须超越的基线。

6.2 对不同角色的行动建议

• 验证工程师：先把 LLM 用在”低风险、高重复”的环节——断言草案、覆盖率空洞归因、回归失败日志聚类、波形问答；断言上生产前必须过 FPV + 非空洞 + 变异杀伤三重检查。另注意：波形喂给 LLM 时用”事件时间 JSON”而非原始 VCD（WaveformQA 已验证前者更优）。
• EDA 工具厂商：竞争点已从”生成能力”转向”反馈回路的质量“——谁能把工具内部的确定性信号（CEX、覆盖率、lint、时序报告）以 agent 友好、token 经济的方式暴露出来，谁就掌握护城河。但注意：Accellera 目前没有任何 AI 工作组，MCP/工具调用接口零标准，这是先手机会，也是客户锁定风险。
• 研究者：benchmark 的严格性审计（GateTruth 路线）、鲁棒性评测（EquivSVA / 语义保持变换路线）、以及波形时序调试（2026 年 7–10 月才出现、基准最薄）是低竞争、高影响力的空位。
• 技术选型：① 优先看论文是否报告 非空洞率 + 变异覆盖率 + 形式覆盖率；只报语法通过率与 pass@1 的不建议作为选型依据。② 不要被参数规模误导，验证任务上 4B 专用模型已多次超过 671B 通用模型。③ 优先复用有确定性兜底的方案（模板生成、求解器裁决、证书门控），而不是”让 LLM 自由发挥”的方案。④ 内部自建评测：外部不存在可信的工业级基准，自建 20–50 个真实模块的评测集，比追逐 SOTA 数字更有价值。

6.3 给你的技术路线建议（如果要在内部落地）

按投入产出排序，建议分三步走：

1. 先做基础设施（1–2 个月，风险最低、收益最确定）：把仿真波形、回归日志、覆盖率报告、lint 输出统一成 agent 可查询的结构化形式（BTTF 证明这条路线可用 SQL 达到 95%+ 准确率；ChipMEM 证明”只在验证通过后才记忆”能提升 agent 表现）。这一步不依赖任何前沿模型能力提升。
2. 再做低风险生成（2–4 个月）：断言草案、覆盖率空洞归因、失败日志聚类。用 HAVEN/UCAgent 式架构（LLM 只解析规格与决策，代码由模板/框架生成），把编译通过率从”需要修”变成”天然 100%”。
3. 最后做闭环与门控（持续）：为每一类 LLM 输出定义可独立校验的验收条件（形式证明 + 非空洞检查 + 变异杀伤），对齐 IC3-Evolve 的证书门控范式。没有门控的闭环会积累虚假信心——Axiomise 和 SecTB-RTL 都明确警告过这一点。

7. 未能核实的内容（诚实清单）

以下内容在 2026-10-08 的调研条件下未能验证，本报告不做推测：

1. web_search 工具不可用：所有调用返回 HTTP 401 Authentication Fails ... api key invalid（搜索端点配置问题，需在 Settings > Plugins > Plugin configuration > Web search 中由用户修改）。因此本报告没有使用任何搜索引擎索引，全部依赖 arXiv API、会议官网、DOI 系统的直接抓取。可能遗漏未被 arXiv 收录、或会议官网以 JS 渲染而无法抓取的论文。
2. ICCAD 2026 论文程序未公开：官网截至调研日只有 Keynote / Workshop / Special Session / Tutorial / Panel 页面，没有论文列表。本报告中的 ICCAD 2026 论文均依据作者在 arXiv 元数据中的录用标注。
3. DATE 2026 程序：date-conference.com 已切换为 DATE 2027（2027-03-22~24，Dresden），2026 子站程序页返回无法解析的 HTML、/venue 与 /call-for-papers 报 Drupal 500，DATE 2026 的确切会期、城市与会话名未核实（仅确认论文集已出版，DOI 前缀 10.23919/date69613.2026）。
4. DVCon U.S. 2026 论文清单：站点正文为前端渲染，脚本抓取仅得到导航；且站点已切换为 DVCon U.S. 2027，分会标题的年份归属无法从正文确认。仅确认了分会标题存在。
5. ACM DL / IEEE Xplore 全文与目录：ACM DL 返回 HTTP 403（Cloudflare 拦截），IEEE Xplore 未做批量抓取；DAC 2026 的 ACM 论文集目录未能读取。论文 DOI 10.1145/3770743.3804146（ChatSVA 标注的 DAC 2026 DOI）在 DOI 系统中尚未生效。
6. DAC 2026 程序的完整论文表：官网提供可检索程序（63dac.conference-program.com）与 PDF 程序表，但前者为 JS 应用、后者为 PDF（抓取工具不支持 PDF），均未能读取正文。因此本报告的 DAC 2026 论文清单是”arXiv 上标注录用”的子集，不是完整录用列表。
7. 厂商量化宣称：未做独立验证的厂商数据本报告一律不引述，详见 industry.md 的证据分级。
8. 本文中标注”待核实具体数值”的条目（如 NeuroAbs、STELLAR、PALM 的量化结果），表示我确认了论文存在与录用信息，但未读到其具体实验数字。
9. VeriBench（硬件版）：多个独立检索路径均未命中，其存在性、任务类型、指标与年份均无法确认，本报告不引用。若你的团队内部沿用了这一名称，请以你们自己的来源为准。
10. AssertLLM2 的存在性已由我方直接元数据抓取确认（arXiv 2605.27472），与另一路调研的相反结论不一致，以我方直接抓取为准（见 §2.7）。
11. 一个被撤回的论文：AgentDV（arXiv 2608.27148）已被作者以”方法与实验设置有误”为由撤回，其任何数字不得引用（原文引述见 §4.2 第 6 条）。
12. “LLM 用于硅后验证/芯片 bring-up”在 arXiv 上完全空白：检索 "silicon bring-up" 返回 0 条；唯一所见是 DVCon U.S. 2026 的一篇 Elasticsearch 智能体论文（来自会议论文集，非预印本）。不要指望这一方向有成熟工作可借鉴。
13. 没有任何量化的 bug-escape 降低数据，也没有受控的厂商/工业级生成式 AI 效率提升研究。 唯一的厂商工具数据点是 Cadence Xcelium ML 约 3× 回归压缩（arXiv 2405.17481，DVCon Europe 2022）——属 ML 而非 LLM，且已超出本报告时间窗。
14. ML 顶会（ICLR 2026 / ICML 2026 / NeurIPS 2025–2026）的接收列表未能枚举：这些会议的论文只能通过作者在 arXiv 元数据中的自述来确认（例如 LLM4Cov 自称 ICML 2026 camera-ready、BTTF 自称 NeurIPS 2026 workshop、VeriTrace 自称 ICLAD 2026 Long Oral），未与官方接收列表交叉核对。
15. 作者单位未做任何推测：arXiv 元数据基本不含机构信息，报告中的机构信息（如”中科院计算所”）仅来自论文摘要自述或公开标注，请勿作为确切单位引用。
16. 会议官网普遍不可用：ACM DL 返回 HTTP 403、IEEE Xplore 未做批量抓取、GitHub/dblp 不可达。因此本报告没有任何一条”official program”级别的证据用于确认 2026 年论文的 session 归属；DAC 2026 的完整论文集目录、DVCon 全部论文摘要（只有 PDF）均未能读取。
17. LAsset（DATE 2026）为付费墙论文：只核实到标题、作者、单位（Univ. of Florida）与 DOI，摘要与召回数字均未取得；一度流传的”90% / 93% 召回”未经核实，本报告不作为事实引用。
18. 未能找到专门工作的若干方向（按”确实没有”处理，不要期待可借鉴成果）：LLM 用于 常数时间 / 推测执行泄漏的形式验证、LLM 用于硬件木马检测（只有非 LLM 的 ADVERSARIAL）、安全启动验证、ACL2 或 Isabelle + 硬件 + LLM（目前只有 Rocq/Coq 与 Lean 两条路线）、LLM 用于硅后 bring-up / 芯片调试、LLM 专用的回归日志分诊论文。
19. LLMs Gaming Verifiers: RLVR can Lead to Reward Hacking（arXiv 2604.15149）：仅通过 OpenAlex 发现条目，全文未获取，本报告仅作为线索列出，不作为证据。
20. 若干已知 ID 经复核后与最初简报的分类不符，已在正文更正：CHORUS（2608.10090） 是激励/测试平台生成，不是模型检查或 PDR 工作；ADVERSARIAL（2607.23882） 不是 LLM 方法。此外 IC3-Evolve、Large Lemma Miners、CHORUS、2607.18727、Autoformalizing Memory Specifications、FLAG 的 arXiv 元数据中均无任何会议录用标注，全部按”预印本”处理。
21. 部分论文摘要中根本没有数字：2511.10007（AssertMiner）、2509.14668（DeepAssert）、2503.19174（AssertionForge）、2502.16662（Saarthi）、2510.15902（Configurable IP 验证框架）、2507.21694（MAVF）、2603.03147（Agentic Coverage Closure）等只给出”显著提升”而无数值，本报告未为它们编造数字。
22. “作者自述录用”未经任何独立核实：arXiv 不审核 comment 字段，也不记录”先录用后撤稿”。本报告中凡只有 arXiv comment 的会场声明，均为作者自述；只有带出版商 DOI（如 ICCAD 的 10.1145/3831252.*、DATE 的 10.23919/DATE69613.2026.*）或 journal_ref 的才算较强证据。已识别的”投稿冒充录用”案例见 §1.1。
23. 若干会场确实”零命中”，但这是”无证据”而非”不存在”：FMCAD 2026、CAV 2026、HOST 2026、ITC 2026、ISCA 2026 的 arXiv 检索均未发现硬件/EDA 功能验证工作；dblp 被 Anubis 机器人墙拦截、aclanthology 超出抓取上限，因此无法排除这些会场有未被 arXiv 收录的论文。Hack@DAC 2025/2026 官方成绩榜、ICLR 2026 录用名单同样未能枚举（唯一触达的 ICLR 2026 条目 VeriReason 的 OpenReview venueid 实际是 Rejected_Submission——是拒稿，不是录用）。
24. 一个具体的方法论坑（用于后续检索）：all:"DVCon 2026" 返回 0 条（必须用 all:"DVCon"）；all:"ITC 2026" 返回的是 ITCS 2026 密码学论文；all:"ASP-DAC 2026" 未命中任何已知的 ASP-DAC 2026 验证论文（SuperSAGA / VeriRAG / AssertMiner / LLM 验证综述）——说明这些论文在 arXiv 上完全没有 venue 戳或根本不在 arXiv。
25. CHARGE 的分项数字（27/42 缺陷、89% 可在 JasperGold 运行、92.2% 非空洞）来自早期抓取的摘要，后续因 arXiv 接口限流未能二次核实。这些数字与论文的会议归属同时记录在 formal-security.md 与数据文件中，但属于”单次抓取、未经复核”，引用时请注明。
26. 同一篇论文在两轮调研中可能导致不同结论，这是本次调研的最大教训：由于 arXiv 接口的限流是间歇性的（连续 6–10 次请求后失效数分钟），同一查询在不同时刻会得出”有结果/无结果”两种截然相反的结论，进而衍生出”某论文不存在””某数字不可核实”等错误判断。本次已识别并更正了两处此类错误（AssertLLM2 存在性、LAsset 召回数字）。任何”未找到”的结论都应视为”在当前限流窗口内未找到”，而非事实。

附录：本次调研的原始数据与子报告

检索方法备注：co: 前缀查询的是 arXiv 的 comment 字段，能高效捞出作者自述的录用信息；但绝大多数 DAC/ICCAD 论文不上 arXiv，因此该方法”高置信度、低召回”。本报告的论文清单是可在线验证的子集，不是完整录用列表。

关于形式验证/安全验证专题：该方向做了两轮独立检索。第一轮因 arXiv 接口限流只完成主体；第二轮在接口可用时（约 1–4 分钟成功一次）补齐了安全资产识别、木马攻防、DATE/ASP-DAC 会议元数据等第一轮无法触达的材料，以 ADDENDUM 形式追加（未覆盖原文件）。本报告 §2.2 / §2.6 已与两轮结果交叉核对。

两轮之间的结论更正（重要，说明”以能否直接读到元数据原文”为裁定标准）：

• LAsset 的 90%/93% 召回 —— 第一轮标记为”不可核实”，第二轮核实为真（来源：DATE 2026 的 DOI 索引会议摘要，逐字为 “up to 90% recall for intra-module asset classification/identification and 93% recall at SoC design level”）。本报告采用第二轮结论。
• ADVERSARIAL 不是 LLM 方法（两轮一致）。
• FVBench 很可能不存在（ti:"FVBench" 在 arXiv 返回 0 条）——不要引用这个名称。
• CHORUS 属于激励生成，不是模型检查/PDR 工作（两轮一致）。

证据等级说明：本报告使用三级标注——**【官方程序】**会议官方页面/DOI 索引会议摘要　**【会议录用】**论文 arXiv 元数据中的录用标注（引述原文）　**【预印本】**仅 arXiv。由于 ACM DL（HTTP 403）、IEEE Xplore、GitHub、dblp 在本环境不可达，本报告绝大多数条目处于后两级，凡标注为”会议录用”的均为作者自述，未与官方录用名单交叉核对（少数经 DOI 索引会议摘要确认的条目已升级为”官方程序”）。

1. 生成公钥和私钥

   Windows

   在桌面，键盘按win键+r键，输入cmd，回车，打开cmd终端输入：

   1	ssh-keygen -t rsa

   一路回车

   Linux

   打开终端，输入：

   1	ssh-keygen -t rsa

   一路回车

2. 复制刚刚生成的公钥

   Windows

   在桌面，键盘按win键+r键，输入cmd，回车，打开cmd终端输入：

   1	notepad %HOMEPATH%/.ssh/id_rsa.pub

   复制这一行, 等后续使用

   • 如果不行，输入：

   1	notepad $HOME/.ssh/id_rsa.pub

   Linux

   打开终端，输入：

   1	cat ~/.ssh/id_rsa.pub

   复制输出的结果, 等后续使用

[!注意]

这一行很长！一定要复制完。格式以ssh-rsa xxxxxxxx开头，以你的用户名@你的系统名结尾，如:

1	ssh-rsa AAAA......xxxx= satan\satan@SatanGT

这个公钥本地只需要生成一次，在不同的服务器上都可以直接进行复制使用。

3. 将本地的公钥复制到服务器上

   • 通用方法

     登录linux后，先检查有没有~/.ssh/authorized_keys文件，如果没有，输入：

     1 2 3 4

     mkdir -p ~/.ssh touch ~/.ssh/authorized_keys chmod 700 ~/.ssh chmod 600 ~/.ssh/authorized_keys

     将刚才复制的公钥粘贴到authorized_keys里。

     或输入:

     1	echo ssh-rsa AAAA......xxxx= user@host（上面复制的公钥） >> ~/.ssh/authorized_keys

   • Linux快捷指令
     打开终端，输入:

     1 2 3 4

     # 将user@remote-server换成你的服务器，可以带端口等选项 ssh-copy-id user@remote-server # 或 ssh-copy-id -i ~/.ssh/work_key.pub -p 2222 user@remote-server

​ 至此，后续的ssh可以免密登录。

4. 常用的指令

   • tab补全忽略大小写

   1	echo 'set completion-ignore-case on' >> ~/.inputrc

   • .bashrc

     1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24

     case $- in *i*) ;; *) return;; esac if [ -f ~/.bash_aliases ]; then . ~/.bash_aliases fi # enable programmable completion features (you don't need to enable # this, if it's already enabled in /etc/bash.bashrc and /etc/profile # sources /etc/bash.bashrc). if ! shopt -oq posix; then if [ -f /usr/share/bash-completion/bash_completion ]; then . /usr/share/bash-completion/bash_completion elif [ -f /etc/bash_completion ]; then . /etc/bash_completion fi fi if [ -e $HOME/.bash_functions ]; then source $HOME/.bash_functions fi

   • .bash_functions

     • cd命令自动输出目录下文件

     1 2 3 4 5 6 7 8 9 10 11

     echo ' function cd() { DIR="$*"; # if no DIR given, go home if [ $# -lt 1 ]; then DIR=$HOME; fi; builtin cd "${DIR}" && \ # use your preferred ls command ls -F --color=auto }' >> ~/.bash_functions

     • 实验室内部服务器，需要科学上网，使用socks5代理，输入lvpn指令切换是否使用代理。

     1 2 3 4 5 6 7 8 9 10 11

     echo ' function lvpn() { # 如果没有设置ALL_PROXY环境变量，则默认使用socks5代理,重复输入取消代理 if [ -z "$ALL_PROXY" ]; then export ALL_PROXY="socks5h://127.0.0.1:10080"; echo "ALL_PROXY set to $ALL_PROXY"; else unset ALL_PROXY; echo "ALL_PROXY unset"; fi; }' >> ~/.bash_functions

     重启终端后测试，如果发现没有生效，原因是.bashrc里没有source .bash_functions，需要输入：
     

     1 2 3 4 5

     echo ' if [ -e $HOME/.bash_functions ]; then source $HOME/.bash_functions fi ' >> ~/.bashrc

     
     

     1 2	#测试效果 curl https://api.openai.com

   • .bash_aliases

     1 2 3 4 5 6 7 8 9 10

     alias gh='history|grep' alias cpv='rsync -ah --info=progress2' alias ..='cd ..' alias ...='cd ../..' alias untar='tar -zxvf ' alias pg='ps -aux|grep ' woc_he() { curl -s "https://ipinfo.io/${1:-}" echo }

   • 检测本机ip

     1 2	curl ipinfo.io curl ifconfig.me

   • 检测他人ip

     1	curl ipinfo.io/[ip]

1. 基本语法:

1
2
3

if [ command ]; then
     符合该条件执行的语句
fi

2. 扩展语法：

1
2
3
4
5
6
7

if [ command ];then
     符合该条件执行的语句
elif [ command ];then
     符合该条件执行的语句
else
     符合该条件执行的语句
fi

3. 语法说明：

​ bash shell会按顺序执行if语句，如果command执行后且它的返回状态是0，则会执行符合该条件执行的语句，否则后面的命令不执行，跳到下一条命令。
当有多个嵌套时，只有第一个返回0退出状态的命令会导致符合该条件执行的语句部分被执行,如果所有的语句的执行状态都不为0，则执行else中语句。
返回状态：最后一个命令的退出状态，或者当没有条件是真的话为0。

注意：

1. [ ]表示条件测试。注意这里的空格很重要。要注意在[后面和]前面都必须要有空格
2. 在shell中，then和fi是分开的语句。如果要在同一行里面输入，则需要用分号将他们隔开。
3. 注意if判断中对于变量的处理，需要加引号，以免一些不必要的错误。没有加双引号会在一些含空格等的字符串变量判断的时候产生错误。比如[ -n "$var" ]如果var为空会出错
4. 判断是不支持浮点值的
5. 如果只单独使用>或者<号，系统会认为是输出或者输入重定向，虽然结果显示正确，但是其实是错误的，因此要对这些符号进行转意
6. 在默认中，运行if语句中的命令所产生的错误信息仍然出现在脚本的输出结果中
7. 使用-z或者-n来检查长度的时候，没有定义的变量也为0
8. 空变量和没有初始化的变量可能会对shell脚本测试产生灾难性的影响，因此在不确定变量的内容的时候，在测试号前使用-n或者-z测试一下
9. ? 变量包含了之前执行命令的退出状态（最近完成的前台进程）（可以用于检测退出状态）

4. 常用参数：

文件/目录判断：

常用的：

1
2
3
4
5
6
7

[ -a FILE ] 如果 FILE 存在则为真。
[ -d FILE ] 如果 FILE 存在且是一个目录则返回为真。
[ -e FILE ] 如果 指定的文件或目录存在时返回为真。
[ -f FILE ] 如果 FILE 存在且是一个普通文件则返回为真。
[ -r FILE ] 如果 FILE 存在且是可读的则返回为真。
[ -w FILE ] 如果 FILE 存在且是可写的则返回为真。（一个目录为了它的内容被访问必然是可执行的）
[ -x FILE ] 如果 FILE 存在且是可执行的则返回为真。

不常用的：

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16

[ -b FILE ] 如果 FILE 存在且是一个块文件则返回为真。
[ -c FILE ] 如果 FILE 存在且是一个字符文件则返回为真。
[ -g FILE ] 如果 FILE 存在且设置了SGID则返回为真。
[ -h FILE ] 如果 FILE 存在且是一个符号符号链接文件则返回为真。（该选项在一些老系统上无效）
[ -k FILE ] 如果 FILE 存在且已经设置了冒险位则返回为真。
[ -p FILE ] 如果 FILE 存并且是命令管道时返回为真。
[ -s FILE ] 如果 FILE 存在且大小非0时为真则返回为真。
[ -u FILE ] 如果 FILE 存在且设置了SUID位时返回为真。
[ -O FILE ] 如果 FILE 存在且属有效用户ID则返回为真。
[ -G FILE ] 如果 FILE 存在且默认组为当前组则返回为真。（只检查系统默认组）
[ -L FILE ] 如果 FILE 存在且是一个符号连接则返回为真。
[ -N FILE ] 如果 FILE 存在 and has been mod如果ied since it was last read则返回为真。
[ -S FILE ] 如果 FILE 存在且是一个套接字则返回为真。
[ FILE1 -nt FILE2 ] 如果 FILE1 比 FILE2 新, 或者 FILE1 存在但是 FILE2 不存在则返回为真。
[ FILE1 -ot FILE2 ] 如果 FILE1 比 FILE2 老, 或者 FILE2 存在但是 FILE1 不存在则返回为真。
[ FILE1 -ef FILE2 ] 如果 FILE1 和 FILE2 指向相同的设备和节点号则返回为真。

字符串判断

1
2
3
4
5
6
7

[ -z STRING ] 如果STRING的长度为零则返回为真，即空是真
[ -n STRING ] 如果STRING的长度非零则返回为真，即非空是真
[ STRING1 ]　 如果字符串不为空则返回为真,与-n类似
[ STRING1 == STRING2 ] 如果两个字符串相同则返回为真
[ STRING1 != STRING2 ] 如果字符串不相同则返回为真
[ STRING1 < STRING2 ] 如果 “STRING1”字典排序在“STRING2”前面则返回为真。
[ STRING1 > STRING2 ] 如果 “STRING1”字典排序在“STRING2”后面则返回为真。

数值判断

1
2
3
4
5
6

[ INT1 -eq INT2 ] INT1和INT2两数相等返回为真 ,=
[ INT1 -ne INT2 ] INT1和INT2两数不等返回为真 ,<>
[ INT1 -gt INT2 ] INT1大于INT2返回为真 ,>
[ INT1 -ge INT2 ] INT1大于等于INT2返回为真,>=
[ INT1 -lt INT2 ] INT1小于INT2返回为真 ,<
[ INT1 -le INT2 ] INT1小于等于INT2返回为真,<=

逻辑判断

1
2
3
4
5

[ ! EXPR ] 逻辑非，如果 EXPR 是false则返回为真。
[ EXPR1 -a EXPR2 ] 逻辑与，如果 EXPR1 and EXPR2 全真则返回为真。
[ EXPR1 -o EXPR2 ] 逻辑或，如果 EXPR1 或者 EXPR2 为真则返回为真。
[ ] || [ ] 用OR来合并两个条件
[ ] && [ ] 用AND来合并两个条件

其他判断

1
2

[ -t FD ] 如果文件描述符 FD （默认值为1）打开且指向一个终端则返回为真
[ -o optionname ] 如果shell选项optionname开启则返回为真

5. IF高级特性：

​ 双圆括号(( ))：表示数学表达式
​ 在判断命令中只允许在比较中进行简单的算术操作，而双圆括号提供更多的数学符号，而且 在双圆括号里面的>，<号不需要转意。

​ 双方括号[[ ]]：表示高级字符串处理函数
​ 双方括号中判断命令使用标准的字符串比较，还可以使用匹配模式，从而定义与字符串相匹配的正则表达式。

6. 双括号的作用：

​ 在shell中，[ $a != 1 || $b = 2 ]是不允许出，要用[ $a != 1 ] || [ $b = 2 ]，而双括号就可以解决这个问题的，[[ $a != 1 || $b = 2 ]]。又比如这个[ "$a" -lt "$b" ]，也可以改成双括号的形式(("$a" < "$b"))

7. Example

1. 判断目录$doiido是否存在，若不存在，则新建一个

1
2
3

if [ ! -d "$doiido"]; then
　　mkdir "$doiido"
fi

2.判断普通文件$doiido是否存在，若不存在，则新建一个

1
2
3

if [ ! -f "$doiido" ]; then
　　touch "$doiido"
fi

3.判断$doiido是否存在并且是否具有可执行权限

1
2
3
4

if [ ! -x "$doiido"]; then
　　mkdir "$doiido"
chmod +x "$doiido"
fi

4.是判断变量$doiido是否有值

1
2
3
4

if [ ! -n "$doiido" ]; then
　　echo "$doiido is empty"
　　exit 0
fi

5.两个变量判断是否相等

1
2
3
4
5

if [ "$var1" = "$var2" ]; then
　　echo '$var1 eq $var2'
else
　　echo '$var1 not eq $var2'
fi

6.测试退出状态：

1
2
3

if [ $? -eq 0 ];then
    echo 'That is ok'
fi

7.数值的比较：

1
2
3

if [ "$num" -gt "150" ];then
   echo "$num is biger than 150"
fi

8.a>b且a<c

1
2
3

(( a > b )) && (( a < c ))
[[ $a > $b ]] && [[ $a < $c ]]
[ $a -gt $b -a $a -lt $c ]

9.a>b或a<c

1
2
3

(( a > b )) || (( a < c ))
[[ $a > $b ]] || [[ $a < $c ]]
[ $a -gt $b -o $a -lt $c ]

10.检测执行脚本的用户

1
2
3
4

if [ "$(whoami)" != 'root' ]; then
   echo  "You  have no permission to run $0 as non-root user."
   exit  1;
fi

上面的语句也可以使用以下的精简语句

1

[ "$(whoami)" != 'root' ] && ( echo "You have no permission to run $0 as non-root user."; exit 1 )

11.正则表达式

1
2
3
4

doiido="hero"
if  [[ "$doiido" == h* ]];then
    echo "hello，hero"
fi

8. ===其他例子===

1. 查看当前操作系统类型

1
2
3
4
5
6
7
8
9
10
11
12
13
14

#!/bin/sh

SYSTEM=`uname  -s`
if [ $SYSTEM = "Linux" ] ; then
   echo "Linux"
elif
    [ $SYSTEM = "FreeBSD" ] ; then
   echo "FreeBSD"
elif
    [ $SYSTEM = "Solaris" ] ; then
    echo "Solaris"
else
    echo  "What?"
fi

2. if利用read传参判断

1
2
3
4
5
6
7
8
9
10
11
12

#!/bin/bash
read -p "please  input a score:"  score
echo  -e "your  score [$score] is judging by sys now"
if [ "$score" -ge "0" ]&&[ "$score" -lt "60" ];then
    echo  "sorry,you  are lost!"
elif [ "$score" -ge "60" ]&&[ "$score" -lt "85" ];then
    echo "just  soso!"
elif [ "$score" -le "100" ]&&[ "$score" -ge "85" ];then
     echo "good  job!"
else
     echo "input  score is wrong , the range is [0-100]!"
fi

3. 判断文件是否存在

1
2
3
4
5
6
7
8
9
10
11

#!/bin/sh
today=`date  -d yesterday +%y%m%d`
file="apache_$today.tar.gz"
cd  /home/chenshuo/shell

if [ -f "$file" ];then
    echo “”OK"
else
    echo "error  $file" >error.log
    mail  -s "fail  backup from test" loveyasxn924@126.com <error.log
fi

4. 这个脚本在每个星期天由cron来执行。如果星期的数是偶数，他就提醒你把垃圾箱清理：

1
2
3
4
5

#!/bin/bash
WEEKOFFSET=$[ $(date +"%V") % 2 ]
if [ $WEEKOFFSET -eq "0" ]; then
   echo "Sunday evening, put out the garbage cans." | mail -s "Garbage cans out"  your@your_domain.org
fi

5. 挂载硬盘脚本(windows下的ntfs格式硬盘)

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28

#! /bin/sh
dir_d=/media/disk_d
dir_e=/media/disk_e
dir_f=/media/disk_f
a=`ls $dir_d | wc -l`
b=`ls $dir_e | wc -l`
c=`ls $dir_f | wc -l`
echo "checking disk_d..."
if [ $a -eq 0 ]; then
    echo "disk_d  is not exsit,now creating..."
    sudo  mount -t ntfs /dev/disk/by-label/software /media/disk_d
else
    echo "disk_d exits"
fi
echo  "checking  disk_e..."
if [ $b -eq 0 ]; then 
    echo "disk_e is not exsit,now creating..."
    sudo mount -t ntfs /dev/disk/by-label/elitor /media/disk_e
else
    echo  "disk_e exits"
fi
echo  "checking  disk_f..."
if [ $c -eq 0 ]; then
    echo  "disk_f  is not exsit,now creating..."
    sudo mount -t ntfs /dev/disk/by-label/work /media/disk_f
else
    echo "disk_f  exits"
fi

1. Introduction:

• Module Name: ahb_sfr

• Module Overview: The ahb_sfr module is designed to interface with a system’s Special Function Registers (SFRs) via the AHB (Advanced High-performance Bus). It primarily handles the reading and writing operations to these registers based on external requests. The module synchronizes these requests and manages data transfer between the external bus and the internal registers, ensuring data integrity and proper timing.

• Timing control:

2. Input/Output Interfaces Descriptions:

• Inputs:

  • sfrclk: The clock signal for the module. All synchronous operations are triggered on the rising edge of this clock.
  • sfrrstz: Active low reset signal. When asserted, it initializes the module’s internal registers and logic.
  • sfrdatai [7:0]: Data input from the SFRs to be sent to the external bus.
  • ADDR [14:0]: Address bus input specifying the SFR address for the current operation.
  • DATA [7:0]: Data bus input specifying the data to be written to the SFRs.
  • REQ: Request signal indicating an active read or write operation.
  • WR: Write enable signal indicating if the current operation is a write (asserted) or read (deasserted).

• Outputs:

  • sfrwe: Write enable output that signals whether a write operation should be performed to the SFRs.
  • sfraddr (output wire [14:0]): Address output that mirrors the input address to the SFRs.
  • sfrdatao [7:0]: Data output holding the data to be written to the SFRs.
  • s2adata [7:0]: Data output that directly mirrors the input sfrdatai, intended for external monitoring or further processing.
  • ACK: Acknowledge signal toggled to indicate the completion of a request processing cycle.

3. Clock and Reset Strategy:

• Clock:

  • Name: sfrclk
  • Active State: The clock signal is active on the rising edge, which is used to synchronize all sequential logic within the module.

• Reset:

  • Name: sfrrstz
  • Active State: The reset signal is active-low. When asserted, it initializes the module’s internal registers and logic.

4-1. Parameters constant:

• None

4-2. Macro constant:

• None

5. Algorithmic Logic

• Reset and Initialization:
  All internal registers (ReqSyncD, SFRWrS, data_i, wr_i, addr_i, sfrwe, sfrdatao, and ACK) are initialized to their default states upon reset (sfrrstz asserted).

• Request Synchronization:
  The module uses a simple synchronization mechanism to detect edges in the REQ signal. This is achieved by comparing the current REQ state with a delayed version (ReqSyncD), stored from the previous clock cycle. The result (ReqToggle) indicates a change in the request state, triggering data and control updates.

• Data and Control Flow:
  Upon detecting a request (ReqToggle asserted), the module captures the address (ADDR), data (DATA), and write enable (WR) from the inputs and stores them in internal registers (addr_i, data_i, wr_i). These values are used to set up the subsequent operations.

  • If a write operation is detected (wr_i asserted), the write enable output (sfrwe) is set based on the SFRWrS status, which tracks the request state to prevent erroneous writes during request transitions.
  • For write operations, the data to be written to the SFR (sfrdatao) is updated with the value from data_i if both wr_i and SFRWrS are asserted.

• Output and Acknowledgement:
  The address output (sfraddr) directly mirrors the internal address register (addr_i). The s2adata output is a direct pass-through of the sfrdatai input, allowing external entities to monitor or process the incoming SFR data. The ACK signal is toggled to indicate the completion of a processing cycle, helping external controllers to manage the timing and sequence of operations.

6 Operational Cycles

The ahb_sfr module is designed to interface with a system bus, handling specific register operations including data transfer and synchronization. The module operates primarily on the rising edge of the system clock (sfrclk) and remains sensitive to the active low reset signal (sfrrstz). The core functionality revolves around capturing and responding to data requests from the bus, managing data write operations, and acknowledging the completion of these operations.

Sequential Logic:

• Reset and Synchronization: The module uses edge-triggered flip-flops to capture and synchronize the request signal (REQ). This synchronization helps in mitigating any metastability issues due to the asynchronous nature of the input request.
• Data and Control Signal Capturing: Upon detecting a change in the request signal (ReqToggle), the module captures the address (ADDR), data (DATA), and write control signal (WR) from the bus. These captured values are stored in internal registers (addr_i, data_i, wr_i) and are used in subsequent operations.
• Write Enable Logic: The write enable signal (sfrwe) is controlled based on the write request (wr_i) and the synchronization status (SFRWrS). This ensures that write operations are only enabled under valid conditions.
• Data Output and Acknowledgment: The module outputs data (sfrdatao) and toggles the acknowledgment signal (ACK) based on the internal state and the synchronization of the request.

Combinational Logic:

• Request Toggle Detection: A simple XOR gate detects changes in the request signal, generating a toggle signal (ReqToggle) that triggers data capturing and acknowledgment logic.
• Data Output to System Bus: The output data to the system bus (s2adata) is directly driven by the input data from another source (sfrdatai), indicating a simple combinational pathway.

7. Data Flow

• ReqSyncD (Request Synchronized Delayed): This signal holds the delayed version of the external request signal (REQ). It is used to detect edges in the request signal by comparing its current state to its previous state.
• data_i (Data Input Register): Captures the data from the bus when a new request is detected. This register temporarily holds the data for processing or forwarding during the write operations.
• SFRWrS (SFR Write Synchronize): Indicates the synchronization status for write operations. It is set when a new request is detected and used to control the write enable signal.
• wr_i (Write Input Register): Captures the write control signal from the bus, indicating whether the current operation involves writing data to the register.
• addr_i (Address Input Register): Holds the address from the bus where data needs to be written or read, captured upon a new request.
• ReqToggle (Request Toggle): A signal generated by XORing the current and delayed request signals. It indicates a change in the request status, used to trigger data capturing and acknowledgment logic.
• sfrwe (SFR Write Enable): Controlled by the write request and synchronization status, this signal enables the data write operation to the internal registers.
• sfrdatao (SFR Data Output): Outputs data based on the internal logic conditions, specifically during write operations when both write request and synchronization are affirmed.
• ACK (Acknowledgment): Toggled in response to a new request detection, signaling the completion of a data read or write operation.

1. Introduction:

• Module Name: ct_pmp_regs

• Module Overview: The ct_pmp_regs module is designed to manage and configure a set of registers related to physical memory protection (PMP) in a processor. The primary objective of this module is to handle the read and write operations to PMP configuration and address registers. It ensures that the PMP settings are correctly updated based on control signals, allowing for secure and controlled access to memory regions. The module supports multiple PMP entries, each with configurable attributes such as read, write, execute permissions, address mode, and lock status.

• Timing control:

2. Input/Output Interfaces Descriptions:

• Inputs:

  • cp0_pmp_wdata [63:0]: A 64-bit data bus used to write data into the PMP configuration and address registers.
  • cpuclk: The clock signal for synchronizing operations within the module.
  • cpurst_b: An active-low reset signal used to initialize the module’s registers to their default states.
  • pmp_csr_sel [17:0]: An 18-bit signal used to select which PMP configuration or address register is being accessed.
  • pmp_csr_wen [17:0]: An 18-bit write enable signal used to control the write operations to the PMP registers.

• Outputs:

  • pmp_cp0_data [63:0]: A 64-bit data bus used to output data from the PMP configuration and address registers.
  • pmpaddr0_value [28:0] to pmpaddr7_value [28:0]: Eight 29-bit signals representing the values of the PMP address registers.
  • pmpcfg0_value [63:0]: A 64-bit signal representing the combined values of the first four PMP configuration registers.
  • pmpcfg2_value [63:0]: A 64-bit signal representing the combined values of the next four PMP configuration registers.

3. Clock and Reset Strategy:

• Clock:

  • Name: cpuclk
  • Active State: The clock signal is active on the rising edge, which is used to synchronize all sequential logic within the module.

• Reset:

  • Name: cpurst_b
  • Active State: The reset signal is active-low. When asserted (logic 0), it initializes all PMP configuration and address registers to their default states, ensuring a known starting condition for the module.

4-1. Parameters constant:

The module contains the following parameter constant:

• parameter ADDR_WIDTH = 29;

4-2. Macro constant:

• None

5. Algorithmic Logic

1. Configuration Registers:

   • The module contains multiple configuration registers (pmpcfg) which store permissions and attributes such as readable, writable, executable, and locked states.
   • Each configuration register manages separate regions or segments of memory, with specific fields determining the operation mode and permissions of each segment.

2. PMP Initialization:

   • Upon reset (cpurst_b signal low), all the configuration and address registers within the module are initialized to a predefined state (0), ensuring a secure and known initial state.

3. Permission and Mode Settings:

   • Each PMP configuration register (pmpcfgX) holds bits that define access rights: readable, writable, and executable, alongside a two-bit mode for address matching.
   • The lock bit in each configuration register indicates whether further writes to the register are possible.

4. Hardware Updates:

   • Configuration registers are updated on the rising edge of the clock (cpuclk) when the corresponding write enable (pmp_csr_wen) signals are valid and no lock conditions are met.
   • Address registers are updated similarly, respecting any lock and match-mode dependencies ensuring secure modification prevention.

5. Chaining Logic:

   • Address matching and permission interpretation rely on the state of the configuration registers, such as mode matching and lock conditions.
   • For chained configurations, the write operations to a PMP address are conditional on already established locks and address mode values.

6. Inter-module Communication:

   • Input cp0_pmp_wdata carries the data for register updates, while pmp_cp0_data serves as an output conveying PMP configurations to other modules.
   • Selection and enable vectors (pmp_csr_sel, pmp_csr_wen) control which registers are accessed for read/write operations.

6 Operational Cycles

• Reset Phase: Registers are reset, meaning they all initialize to zero, ensuring that all regions are initially inaccessible until explicitly configured.

• Configuration Phase: During normal operation post-reset, configuration registers can be updated based on provided data (cp0_pmp_wdata) when writing is enabled via control signals and existing register contents permit the modification (e.g., no active lock bits).

• Normal Operation: During normal runtime, the PMP registers govern access permissions dynamically, allowing secure and managed access to the processor’s memory space per the configuration stored within these registers.
  Algorithm Mechanics:

• Registers: The module contains various configuration registers (pmp0cfg, pmp1cfg, … , pmp7cfg) and address registers (pmpaddr0_value through pmpaddr7_value) to manage PMP regions.

• Configuration Logic:

  • Each pmpcfg# register has fields for address matching mode, permissions (readable, writable, executable), and a lock bit to prevent further modifications.
  • Data from cp0_pmp_wdata is loaded into registers based on write enable signals (pmp_csr_wen[]) provided that the lock bit is not set.

• Address Logic:

  • Address registers are updated based on corresponding enable signals ensuring the previous entry is not locked.

Timing: Updates to the registers are synchronized with the clock signal. On a rising edge of cpuclk, updates occur if the write enable (pmp_csr_wen[]) is set and the reset (cpurst_b) is not asserted.

7. Data Flow

Data Tracing and Processing:

• Input to Register Update: Data from cp0_pmp_wdata is stored into the appropriate configuration (pmpcfg#) or address (pmpaddr#_value) register based on the current state of selection and enable signals, considering lock conditions.
• Configuration to Output: The corresponding configuration or address states can be read out via pmp_cp0_data or pmpcfg0_value, based on pmp_csr_sel[].

Error Handling:

• Lock Protection: If a lock bit within a configuration register is set, further writes to that configuration are blocked regardless of the enable state.

Timing in Data Movement:

• Sequential Updates: Data from cp0_pmp_wdata is sequentially applied across cycles, starting with the first enabled register according to the selection and enable signals.

Concurrency Management:

• Independent Configuration Blocks: Each pmpcfg# and pmpaddr# register set operates independently, allowing updates to different regions concurrently, as long as they adhere to lock and enable conditions.

1 Spec ————A 32-bits Multiplier

Input

Output

2 Design

2.1 testbench.v

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365

`timescale 1ns / 1ps
`define cycles  40
module tb;

	// Inputs
	reg clk;
	reg mult_begin;
	reg [31:0] mult_op1;
	reg [31:0] mult_op2;
	reg [63:0] Data_in_t;
	// Outputs
	wire [63:0] product;
	wire mult_end;

	// Instantiate the Unit Under Test (UUT)
	multiply uut (
		.clk(clk), 
		.mult_begin(mult_begin), 
		.mult_op1(mult_op1), 
		.mult_op2(mult_op2), 
		.product(product), 
		.mult_end(mult_end)
	);
	integer i,errors[0:39],cnt;
	
	integer fd = 0;
	initial begin
		// Initialize Inputs
		clk = 0;
		mult_begin = 0;
		mult_op1 = 0;
		mult_op2 = 0;
		for (i = 0; i < 40; i = i + 1)
			begin
			errors[i] = 0;
			end
		i=0;
		cnt=0;
		$dumpfile("mul.vcd");

		$dumpvars();
		fd = $fopen("./report.txt", "w");
		// if(!fd)
		// 	begin
		// 		$display("Could not open File \r");
		// 		$stop;
		// 	end

		#1000;
		//正数*正数
		mult_begin = 1;
		mult_op1 = 32'H6A98F28D;
		mult_op2 = 32'H7E184AD4;
		Data_in_t = 64'H348164E09FFD9EC4;
		#50;
		mult_begin = 0;
		#1000;
		mult_begin = 1;
		mult_op1 = 32'H2B661ACE;
		mult_op2 = 32'H6AE5B749;
		Data_in_t = 64'H121F3881A38CE6BE;
		#50;
		mult_begin = 0;
		#1000;
		mult_begin = 1;
		mult_op1 = 32'H25BD7BEE;
		mult_op2 = 32'H4ADDFFD9;
		Data_in_t = 64'H0B09801E84861EBE;
		#50;
		mult_begin = 0;
		#1000;
		mult_begin = 1;
		mult_op1 = 32'H0D3A404E;
		mult_op2 = 32'H64B23883;
		Data_in_t = 64'H0533F68AB11BF7EA;
		#50;
		mult_begin = 0;
		#1000;
		mult_begin = 1;
		mult_op1 = 32'H3F64172B;
		mult_op2 = 32'H60CE4AB1;
		Data_in_t = 64'H17F89DB9878072BB;
		#50;
		mult_begin = 0;
		#1000;
		mult_begin = 1;
		mult_op1 = 32'H16761A51;
		mult_op2 = 32'H13462A55;
		Data_in_t = 64'H01B0EBF60AAE06E5;
		#50;
		mult_begin = 0;
		#1000;
		mult_begin = 1;
		mult_op1 = 32'H2026D659;
		mult_op2 = 32'H6D726BE8;
		Data_in_t = 64'H0DBEE81CB76B73A8;
		#50;
		mult_begin = 0;
		#1000;
		mult_begin = 1;
		mult_op1 = 32'H02618586;
		mult_op2 = 32'H1E83A59C;
		Data_in_t = 64'H0048A717560EBBA8;
		#50;
		mult_begin = 0;
		#1000;
		mult_begin = 1;
		mult_op1 = 32'H1B77F796;
		mult_op2 = 32'H5B4B942D;
		Data_in_t = 64'H09CBC10E0A2B3D5E;
		#50;
		mult_begin = 0;
		#1000;
		mult_begin = 1;
		mult_op1 = 32'H5AC08456;
		mult_op2 = 32'H64ED2634;
		Data_in_t = 64'H23C745771E5DA578;
		#50;
		mult_begin = 0;
		#1000;
		//负数*负数
		mult_begin = 1;
		mult_op1 = 32'HDC7F53A9;
		mult_op2 = 32'H9F5CEA89;
		Data_in_t = 64'H0D66DE886A583F71;
		#50;
		mult_begin = 0;
		#1000;
		mult_begin = 1;
		mult_op1 = 32'HB7AC2234;
		mult_op2 = 32'HD3FCAAC7;
		Data_in_t = 64'H0C6F5B2E9CB51E6C;
		#50;
		mult_begin = 0;
		#1000;
		mult_begin = 1;
		mult_op1 = 32'HDAE39537;
		mult_op2 = 32'HD347F65B;
		Data_in_t = 64'H067B902D3789E48D;
		#50;
		mult_begin = 0;
		#1000;
		mult_begin = 1;
		mult_op1 = 32'H9F1D7AEA;
		mult_op2 = 32'HFA3E1FC8;
		Data_in_t = 64'H022DCC3B29965CD0;
		#50;
		mult_begin = 0;
		#1000;
		mult_begin = 1;
		mult_op1 = 32'H9F09D52B;
		mult_op2 = 32'H99A59337;
		Data_in_t = 64'H26C454CFE83B7D3D;
		#50;
		mult_begin = 0;
		#1000;
		mult_begin = 1;
		mult_op1 = 32'H90E87B84;
		mult_op2 = 32'HEAA39889;
		Data_in_t = 64'H09450737E2CC79A4;
		#50;
		mult_begin = 0;
		#1000;
		mult_begin = 1;
		mult_op1 = 32'HEA722216;
		mult_op2 = 32'HF7B63872;
		Data_in_t = 64'H00B2A530D3EBFDCC;
		#50;
		mult_begin = 0;
		#1000;
		mult_begin = 1;
		mult_op1 = 32'HB25BF9E7;
		mult_op2 = 32'H9EAEE22C;
		Data_in_t = 64'H1D83C041476EE1B4;
		#50;
		mult_begin = 0;
		#1000;
		mult_begin = 1;
		mult_op1 = 32'HE23F69BC;
		mult_op2 = 32'H804F5678;
		Data_in_t = 64'H0ED712A6FC42B820;
		#50;
		mult_begin = 0;
		#1000;
		mult_begin = 1;
		mult_op1 = 32'H81A763DE;
		mult_op2 = 32'HE857F5F4;
		Data_in_t = 64'H0BACE522E690A598;
		#50;
		mult_begin = 0;
		#1000;
		//正数*负数
		mult_begin = 1;
		mult_op1 = 32'H117B72B5;
		mult_op2 = 32'HFDE88F42;
		Data_in_t = 64'HFFDB6F504BEEADAA;
		#50;
		mult_begin = 0;
		#1000;
		mult_begin = 1;
		mult_op1 = 32'H2EF80EBF;
		mult_op2 = 32'HDE0A0A5F;
		Data_in_t = 64'HF9C4E5A25416EEE1;
		#50;
		mult_begin = 0;
		#1000;
		mult_begin = 1;
		mult_op1 = 32'H56FA268C;
		mult_op2 = 32'H86F6EBA9;
		Data_in_t = 64'HD6E0AE135F0DF66C;
		#50;
		mult_begin = 0;
		#1000;
		mult_begin = 1;
		mult_op1 = 32'H77A17497;
		mult_op2 = 32'HD367D395;
		Data_in_t = 64'HEB29235711D250E3;
		#50;
		mult_begin = 0;
		#1000;
		mult_begin = 1;
		mult_op1 = 32'H5DE04686;
		mult_op2 = 32'HD29727E2;
		Data_in_t = 64'HEF59213D8FC6AC4C;
		#50;
		mult_begin = 0;
		#1000;
		mult_begin = 1;
		mult_op1 = 32'H0F50B083;
		mult_op2 = 32'H844E2D5D;
		Data_in_t = 64'HF89997CD13412697;
		#50;
		mult_begin = 0;
		#1000;
		mult_begin = 1;
		mult_op1 = 32'H671294E9;
		mult_op2 = 32'HE6CCC285;
		Data_in_t = 64'HF5DA8E00A12BEF0D;
		#50;
		mult_begin = 0;
		#1000;
		mult_begin = 1;
		mult_op1 = 32'H23B50CC7;
		mult_op2 = 32'HCFD68C3B;
		Data_in_t = 64'HF9484575D510C5DD;
		#50;
		mult_begin = 0;
		#1000;
		mult_begin = 1;
		mult_op1 = 32'H60F5B7D8;
		mult_op2 = 32'HFA36D021;
		Data_in_t = 64'HFDCF0059DC9C32D8;
		#50;
		mult_begin = 0;
		#1000;
		mult_begin = 1;
		mult_op1 = 32'H4E520906;
		mult_op2 = 32'HC45F3B23;
		Data_in_t = 64'HEDC1E86B8E859DD2;
		#50;
		mult_begin = 0;
		#1000;
		//0*随机
		mult_begin = 1;
		mult_op1 = 32'H00000000;
		mult_op2 = 32'H51B64CC8;
		Data_in_t = 64'H0000000000000000;
		#50;
		mult_begin = 0;
		#1000;
		mult_begin = 1;
		mult_op1 = 32'H00000000;
		mult_op2 = 32'H7BA49B33;
		Data_in_t = 64'H0000000000000000;
		#50;
		mult_begin = 0;
		#1000;
		mult_begin = 1;
		mult_op1 = 32'H00000000;
		mult_op2 = 32'HF937655D;
		Data_in_t = 64'H0000000000000000;
		#50;
		mult_begin = 0;
		#1000;
		mult_begin = 1;
		mult_op1 = 32'H00000000;
		mult_op2 = 32'H72061A95;
		Data_in_t = 64'H0000000000000000;
		#50;
		mult_begin = 0;
		#1000;
		mult_begin = 1;
		mult_op1 = 32'H00000000;
		mult_op2 = 32'HA31321B7;
		Data_in_t = 64'H0000000000000000;
		#50;
		mult_begin = 0;
		#1000;
		mult_begin = 1;
		mult_op1 = 32'H00000000;
		mult_op2 = 32'H8532E4B1;
		Data_in_t = 64'H0000000000000000;
		#50;
		mult_begin = 0;
		#1000;
		mult_begin = 1;
		mult_op1 = 32'H00000000;
		mult_op2 = 32'HCC480B3E;
		Data_in_t = 64'H0000000000000000;
		#50;
		mult_begin = 0;
		#1000;
		mult_begin = 1;
		mult_op1 = 32'H00000000;
		mult_op2 = 32'HB712E17B;
		Data_in_t = 64'H0000000000000000;
		#50;
		mult_begin = 0;
		#1000;
		mult_begin = 1;
		mult_op1 = 32'H00000000;
		mult_op2 = 32'HFF3BAF67;
		Data_in_t = 64'H0000000000000000;
		#50;
		mult_begin = 0;
		#1000;
		mult_begin = 1;
		mult_op1 = 32'H00000000;
		mult_op2 = 32'H6D0E5A16;
		Data_in_t = 64'H0000000000000000;
		#50;
		mult_begin = 0;

		#500;
		if (cnt == 0)
		begin
			$display("Simulation finished Successfully.");
			$fdisplay(fd, "Simulation finished Successfully.");
		end
		else if (cnt >= 1)
		begin	
			$display("%0d ERROR! See log for details.",cnt);
			$fdisplay(fd, "%0d ERROR! See log above for details.",cnt) ;
		end
		$fclose(fd);

		// $finish;
	end
   always #5 clk = ~clk;

//比较
	always @ (negedge mult_end)
		begin
		if ( product !== Data_in_t || product == 64'Bz )
			begin
			// $display(" ------ERROR. A mismatch has occurred-----,ERROR in ", i);
			$fdisplay(fd," ------ERROR. A mismatch has occurred-----,ERROR in ", i);
			errors[i-1] =  1;
			cnt = cnt + 1;
			end
		i = i + 1; 
		
		end
endmodule

2.2 updated_design_0.v

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94

`timescale 1ns / 1ps   

module multiply(               
    input         clk,        // Clock
    input         mult_begin, // begin multiply signal
    input  [31:0] mult_op1,   // 32bits multiplier
    input  [31:0] mult_op2,   // 32bits multiplier
    output [63:0] product,    // multiply product
    output        mult_end   // end multiply signal
);  
    // Multiplication operation signals
    reg mult_valid;  
    reg  [31:0] multiplier;  

    assign mult_end = mult_valid & ~(|multiplier); // End signal: when multiplier is all zeros
    always @(posedge clk)     
    begin  
        if (multiplier == 32'd0)  
        begin  
            mult_valid <= 1'b0;     // No valid multiplication operation
        end  
        else  
        begin  
            mult_valid <= 1'b1;  
        end  
    end  

    // Absolute values of operands
    wire        op1_sign;      // Sign of operand 1
    wire        op2_sign;      // Sign of operand 2
    wire [31:0] op1_absolute;  // Absolute value of operand 1
    wire [31:0] op2_absolute;  // Absolute value of operand 2
    assign op1_sign = mult_op1[31];  
    assign op2_sign = mult_op2[31];  
    assign op1_absolute = op1_sign ? (~mult_op1+1) : mult_op1;  
    assign op2_absolute = op2_sign ? (~mult_op2+1) : mult_op2;  

    // Loading multiplicand and shifting
    reg  [63:0] multiplicand;  
    always @ (posedge clk)    
    begin  
        if (mult_valid)  
        begin    // Shift multiplicand left by one bit each clock cycle
            multiplicand <= {multiplicand[62:0],1'b0};  
        end  
        else if (mult_begin)   
        begin   // Load multiplicand with absolute value of operand 1
            multiplicand <= {32'd0,op1_absolute};  
        end  
    end  

    // Loading multiplier and shifting
    always @ (posedge clk)   
    begin  
        if(mult_valid)  
        begin       // Shift multiplier right by one bit each clock cycle
            multiplier <= {1'b0,multiplier[31:1]}; 
        end  
        else if(mult_begin)  
        begin   // Load multiplier with absolute value of operand 2
            multiplier <= op2_absolute;  
        end  
    end  

    // Partial product calculation
    wire [63:0] partial_product;  
    assign partial_product = multiplier[0] ? multiplicand : 64'd0;        

    // Accumulator for the product
    reg [63:0] product_temp;		
    always @ (posedge clk)  
    begin  
        if (mult_valid)  
        begin  
            product_temp <= product_temp + partial_product;  
        end        
        else if (mult_begin)  
        begin  
            product_temp <= 64'd0;  
        end  
     end  

    // Product sign and final result
    reg product_sign;	// Sign of the product
    always @ (posedge clk)    
    begin  
        if (mult_valid)  
        begin  
            product_sign <= op1_sign ^ op2_sign; // Calculating sign of the product
        end  
    end   
    assign product = product_sign ? (~product_temp+1) : product_temp; // Adjusting sign of the product
endmodule  

3 Report

3.1 Compile Report

Errors: 0, Warnings: 0

1
2
3
4
5
6
7
8
9
10

Model Technology ModelSim SE-64 vlog 10.7 Compiler 2017.12 Dec  7 2017
Start time: 17:33:09 on Jan 26,2024
vlog -work work ./design/testbench.v ./design/updated_design_0.v -l vcompile.txt 
-- Compiling module tb
-- Compiling module multiply

Top level modules:
	tb
End time: 17:33:09 on Jan 26,2024, Elapsed time: 0:00:00
Errors: 0, Warnings: 0

3.2 Simulation Report

Errors: 0, Warnings: 0

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22

# vsim -voptargs="+acc" work.tb -l ./vsim.txt -wlf ./vsim.wlf 
# Start time: 17:33:09 on Jan 26,2024
# ** Note: (vsim-8009) Loading existing optimized design _opt2
# //  ModelSim SE-64 10.7 Dec  7 2017
# //
# //  Copyright 1991-2017 Mentor Graphics Corporation
# //  All Rights Reserved.
# //
# //  ModelSim SE-64 and its associated documentation contain trade
# //  secrets and commercial or financial information that are the property of
# //  Mentor Graphics Corporation and are privileged, confidential,
# //  and exempt from disclosure under the Freedom of Information Act,
# //  5 U.S.C. Section 552. Furthermore, this information
# //  is prohibited from disclosure under the Trade Secrets Act,
# //  18 U.S.C. Section 1905.
# //
# Loading work.tb(fast)
# Loading work.multiply(fast)
# Simulation finished Successfully.
# quit
# End time: 17:33:10 on Jan 26,2024, Elapsed time: 0:00:01
# Errors: 0, Warnings: 0

3.3 TestBench Report

1

Simulation finished Successfully.

1 Spec

2 Design

2.1 multiply.v

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16

`timescale 1ns / 1ps

module multiply(             
	input         clk,        // 时钟
	input         mult_begin, // 乘法开始信号
	input  [31:0] mult_op1,   // 乘法源操作数1
	input  [31:0] mult_op2,   // 乘法源操作数2
	output [63:0] product,    // 乘积
	output        mult_end   // 乘法结束信号
);
	//乘法正在运算信号和结束信号
	reg mult_valid;
	reg  [31:0] multiplier;

	assign mult_end = mult_valid & ~(|multiplier); //乘法结束信号：乘数全0
endmodule

2.2 testbench.v

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27

`timescale 1ns / 1ps
`define cycles  40
module tb;

	// Inputs
	reg clk;
	reg mult_begin;
	reg [31:0] mult_op1;
	reg [31:0] mult_op2;
	reg [63:0] Data_in_t;
	// Outputs
	wire [63:0] product;
	wire mult_end;

	// Instantiate the Unit Under Test (UUT)
	multiply uut (
		.clk(clk), 
		.mult_begin(mult_begin), 
		.mult_op1(mult_op1), 
		.mult_op2(mult_op2), 
		.product(product), 
		.mult_end(mult_end)
	);
	integer i,errors[0:39],cnt;
	always #5 clk = ~clk;

endmodule

3 Log

3.1 Compile Log

Errors: 0, Warnings: 0

1
2
3
4
5
6
7
8
9
10

Model Technology ModelSim SE-64 vlog 10.7 Compiler 2017.12 Dec  7 2017
Start time: 20:07:49 on Dec 01,2023
vlog -work work ./design/multiply.v ./design/testbench.v -l vcompile.txt 
-- Compiling module multiply
-- Compiling module tb

Top level modules:
	tb
End time: 20:07:49 on Dec 01,2023, Elapsed time: 0:00:00
Errors: 0, Warnings: 0

3.2 Simulation Log

Errors: 0, Warnings: 0

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23

# vsim -voptargs="+acc" work.tb -l ./vsim.txt -wlf ./vsim.wlf 
# Start time: 20:07:49 on Dec 01,2023
# ** Note: (vsim-8009) Loading existing optimized design _opt2
# //  ModelSim SE-64 10.7 Dec  7 2017
# //
# //  Copyright 1991-2017 Mentor Graphics Corporation
# //  All Rights Reserved.
# //
# //  ModelSim SE-64 and its associated documentation contain trade
# //  secrets and commercial or financial information that are the property of
# //  Mentor Graphics Corporation and are privileged, confidential,
# //  and exempt from disclosure under the Freedom of Information Act,
# //  5 U.S.C. Section 552. Furthermore, this information
# //  is prohibited from disclosure under the Trade Secrets Act,
# //  18 U.S.C. Section 1905.
# //
# Loading work.tb(fast)
# Loading work.multiply(fast)
#  ------ERROR. A mismatch has occurred-----,ERROR in          40
# 1 ERROR! See log above for details.
# quit
# End time: 20:07:50 on Dec 01,2023, Elapsed time: 0:00:01
# Errors: 0, Warnings: 0