描述断言在形式验证中的应用
解读
国内大型数字芯片项目（手机 SoC、AI 加速器、车规 MCU）进入 6nm 以下工艺后，流片成本动辄千万人民币，验证签核（sign-off）必须“零逃逸”。形式验证（Formal Verification, FV）因能穷尽所有输入空间，成为继 UVM 动态仿真后的第二道“铁闸”。断言（Assertion）是形式验证的“需求语言”，它把设计规格转化为数学命题，交给形式引擎做穷尽证明。面试时，考官想确认候选人是否真正“写过能收敛的断言”，而不是只会写 assert (a && b)。因此，回答要围绕“为什么写、写什么、怎么写、怎么调、怎么签核”五个层次展开，并给出量化的项目数据，体现工业级经验。
知识点
- 断言分类：立即断言（immediate）用于动态仿真调试；并发断言（concurrent, SVA）才是形式验证主体。
- 形式验证流派：
- 模型检查（Model Checking）—— 证明 “AG (req |-> ##[1:10] ack)” 在所有状态成立；
- 等价性检查（EC）—— 用断言做“关键路径”约减，降低 SEC 复杂度；
- 连接性检查（Connectivity Formal）—— 用断言描述 pin-mux、clock-gating 连接表。
- 断言编码原则：
- 因果链完整：antecedent 必须可触发，consequent 必须可失败；
- 时间窗口闭合：避免 ##[0:$] 导致状态爆炸；
- 约束与断言分离：assume 限定 DUT 环境，assert 限定 DUT 行为；
- 分层粒度：block-level 断言 < 1k 状态量，top-level 断言配 abstraction。
- 形式验证收敛技巧：
- 反例长度（depth）与内存折中，国内云算力平台 256-core 场景下，depth 30 以内 80% 收敛；
- 归纳法（K-induction）（k=10~20）可解决深度环路；
- 覆盖率反馈：assert cover 语句产生“断言覆盖率”，与代码行覆盖交叉验证。
- 签核标准：
- 全部断言 PROVEN + 无 unreachable + 无 vacuous；
- 至少 95% 的 cover 断言被触发；
- 形式验证报告纳入《验证评审清单》，由独立 QA 签字。
答案
“在我参与的 12nm AI 加速器项目中，我们共写了 1.8 万条 SVA 并发断言，其中 1.2 万条用于形式验证。流程分五步：
第一步，规格拆解。以 AXI4 接口为例，我把协议拆成 47 条属性，如写地址通道顺序、写响应唯一性等，每条属性对应一条断言。
第二步，分层编码。模块级断言只关注单通道信号，避免跨时钟；顶层用 hierarchical assertion，通过 bind 语句把子模块断言提升到顶层，再补充跨模块场景。
第三步，约束建模。用 assume 限定 master 的合法顺序，假设 ID 深度 ≤ 16，burst 长度 ≤ 256，这样把状态空间从 10^20 压缩到 10^10，在 128-core 服务器上 6 小时收敛。
第四步，迭代调试。首次运行发现 183 条断言失败，反例长度 11 周期。通过查看波形，发现是 FIFO 指针跨时钟域同步延迟导致，设计在 2 周期后才拉高 ready。我把断言窗口从 ##[1:3] 放宽到 ##[1:5]，同时让设计加一级寄存器，第二次全部 PROVEN。
第五步，签核交付。最终形式验证报告包含 1.2 万条 PROVEN、0 条 vacuous、cover 断言触发率 97%，与 UVM 随机覆盖交叉后，把覆盖率从 92.4% 提升到 99.1%，并在评审会上由 QA 签字确认。流片后硅片 A0 版 AXIM 接口未出现任何协议逃逸，验证了断言在形式验证中的价值。”
拓展思考
- 车规功能安全（ISO 26262）要求“诊断覆盖率 ≥ 99%”。如何用形式断言证明安全机制（ECC、TMR）在单点故障下 1 个周期内报警？需要引入“故障注入断言”：先 assume 故障节点 stuck-at，再 assert 报警信号在指定时间窗口拉高，最终给出 FIT 率计算依据。
- 面对 RISC-V 自定义指令，协议文本往往缺失时序细节。可先用 SystemVerilog 的 let 与 sequence 构造“灰色”断言，再通过形式引擎的“属性细化”功能自动生成最小约束，实现“规格到断言”的半自动化闭环。
- 国内先进工艺出现 3 维堆叠（WoW），跨 die 信号存在 2~5ns 不定延迟。传统 cycle-accurate 断言会假失败，可引入“时间抽象”建模，把信号事件转化为时间标签序列，用 LTL 公式描述“标签顺序”而非“时钟周期”，从而保持形式验证的完备性。