形式验证入门：assert/assume/cover、bounded proof 与 FIFO/仲裁器验证

更新时间：2026-09-14。本文是「集成电路大类 · 芯片设计 · 数字验证」实操序列第七篇。前面的仿真无论随机多少 seed，本质都是「抽样运行」。形式验证（formal verification）换了条路：不施加任何激励，用数学方法在所有可达状态上判定某条性质是否恒成立。它和仿真互补，工具如 JasperGold、VC Formal、Questa Formal、开源的 SymbiYosys。

本文要回答的问题

形式验证不跑激励，凭什么说「所有情况都对」？
assert/assume/cover 在形式工具里各扮演什么角色？
bounded proof 和 full proof 差别、unroll 深度是什么？
哪类逻辑最值得上形式，哪类纯属浪费？

一、模型检查：在状态空间里证明而非抽样

仿真：给定输入序列，沿一条路径走，检查这条路径上有没有错——哪怕跑一亿条，仍是一亿条具体路径。

形式（模型检查）：把 RTL 展开成状态迁移关系，用约束求解/SAT 引擎在所有合法输入序列、所有可达状态上判断命题：

能证明对所有可达状态成立 → proven（证明通过）；
找到一条使其失败的输入序列 → 给出 counterexample（反例波形），通常很短、直接定位根因；
在资源/深度内证不出来也找不到反例 → inconclusive（未决），要加约束、黑盒或调深度。

这正是 SVA 里同一条性质的两种用法：仿真中 assert 是运行时检查，形式里它是待证明的定理。

二、assert / assume / cover：形式三要素

语句	在形式中的作用
`assert property`	要求工具证明它在所有可达状态成立；给反例即 bug
`assume property`	约束输入环境，告诉工具「外部保证这样」，据此裁剪状态空间
`cover property`	问「这个情形到底到得了吗」，到得了给一条 witness 路径

三者形成闭环：先用 assume 描述合法输入协议（如「valid 拉起后到握手前保持稳定」），再对 DUT 行为写 assert，最后用 cover 确认深状态可达、断言不是空真。assume 写错（过度约束）会把真实 bug 连同非法输入一起排除，造成假 proven——这是形式验证最危险的坑，必须逐条评审假设是否真的是环境契约。

三、bounded proof、full proof 与深度

Bounded（有界）证明：工具把电路展开 N 个周期（unroll depth），证明「复位后 N 拍内性质成立」。N 之外不保证。多数商业工具先跑有界。
Full proof（完整证明）：对所有周期、所有可达状态成立。工具通常先 bounded，再尝试收敛成 full（状态空间可归纳时）。
深度（proof depth）：要覆盖 FIFO 满/空，深度至少要够「连续写满 + 连续读空」。深度不够时 deep bug 看不到；盲目加深又会爆内存和时间。

实务上先让 cover 证明「能写满、能读空、能反压」可达，再信任在此之上的 assert，是判断深度够不够的办法。

四、最适合形式的逻辑：短小、强控制、边角爆炸

形式的优势在控制密集、状态有限、边角组合极多的逻辑，这类逻辑仿真很难随机到所有交错：

适合形式	典型性质
FIFO	不溢出/不下溢；满时写被拒、空时读无效；读写指针与计数一致；不丢数据
仲裁器	每周期至多一个 grant；不 starvation（任一请求者终会被响应）；优先级/轮询规则
握手/总线控制	valid/ready 稳定、不丢 beat、last 与长度一致、 outstanding 不超限
状态机	无非法状态、无死锁、关键迁移必达
CDC/控制胶水	跨时钟域控制标志不丢脉冲
ECC/编码器（小位宽）	decode(encode(x))==x、错误注入可检出

一个轮询仲裁器的性质示例：

systemverilog

// 环境假设：同一时刻请求向量任意组合都合法（不过度约束）
assume property (@(posedge clk) $onehot0(req) or 1); // 允许多请求并存
// 性质1：没有请求时不发 grant
a_no_grant: assert property (@(posedge clk) disable iff(!rst_n)
  (req==0) |-> (gnt==0));
// 性质2：一次最多一个 grant（互斥）
a_mutex: assert property (@(posedge clk) $onehot0(gnt));
// 性质3：持续请求者不会饿死（N 拍内必被服务）
a_no_starve: assert property (@(posedge clk) disable iff(!rst_n)
  req[i] |-> ##[1:N] gnt[i]);

五、不适合 / 需要改造的情况

大数据通路（宽乘法、DSP、复杂流水线运算）：状态空间爆炸，证明「数值算得对」性价比低，留给仿真/参考模型；
存储器阵列：用抽象内存模型替换真实 SRAM，不要让工具展开每个 bit；
巨大整芯片：按模块/单元（unit-level）做形式，把周边逻辑用 assume 抽象或黑盒；
计数器/位宽巨大：合理设参数、缩小证明配置。

黑盒化（black-box） 把不关心的子模块当边界，用 assume 描述其输出契约，把证明范围收敛到本模块——但黑盒边界的假设要在该子模块自己的形式验证里被证明，否则只是「假设它对」。

六、复位、初始化与常见坑

必须约束复位：disable iff(!rst_n) 或在工具里设初始复位序列，否则工具从任意态出发，会报出现实中不可达的假反例；
X 处理：形式默认常把信号当二值，未初始化/X 传播问题要开对应分析或单独约束；
过度 assume：证明全绿但环境从不可能满足那些假设，等于没验；用 cover 验证假设下场景仍可达；
inconclusive 不是失败也不是通过：继续加抽象、调深度、拆性质，不能拿去签核；
反例要能复现到仿真：好的形式反例很短，可转成定向用例回归保留。

七、上线检查清单

[ ] 优先选控制密集、状态有限的模块，而非大数据通路；
[ ] assume 逐条可回溯到接口协议，无过度约束；
[ ] 用 cover 确认关键深状态可达、性质非空真；
[ ] 证明深度足以覆盖满/空/反压等最深场景；
[ ] 存储器/大位宽已抽象或参数缩小；
[ ] 复位与初始化约束正确，排除不可达假反例；
[ ] 结果区分 proven / counterexample / inconclusive，后者不签核；
[ ] 反例转成可复归的定向用例，边界假设在子模块证明中闭合。

总结

形式验证不施加激励，而是把 RTL 当状态迁移系统、用求解器在所有合法输入序列和可达状态上判定 SVA 性质：assume 约束环境契约、assert 是要证明的定理、cover 确认情形可达且断言非空，结果分 proven / counterexample / inconclusive；bounded proof 只保证复位后 N 拍、要靠足够深度和 cover 确认覆盖满空反压，full proof 才覆盖全部周期；它最适合 FIFO、仲裁器、握手、状态机这类控制密集、边角交错爆炸、仿真难以随机周全的模块，对大数据通路和整芯片要用内存抽象、黑盒和单元级收敛——最大风险是过度 assume 造成的假 proven，因此每条假设都必须可回溯到真实接口契约并在边界闭合。

入门

进阶

专家

形式验证入门：assert/assume/cover、bounded proof 与 FIFO/仲裁器验证 ​

本文要回答的问题 ​

一、模型检查：在状态空间里证明而非抽样 ​

二、assert / assume / cover：形式三要素 ​

三、bounded proof、full proof 与深度 ​

四、最适合形式的逻辑：短小、强控制、边角爆炸 ​

五、不适合 / 需要改造的情况 ​

六、复位、初始化与常见坑 ​

七、上线检查清单 ​

相关与延伸 ​

总结 ​