形式属性验证 FPV：不用测试向量，用数学证明设计属性

更新时间：2026-09-24。验证进阶层。形式方法的总体定位见 形式验证入门，FPV 在项目流程中的切入点与 验证计划 Testplan 和 覆盖率收敛 互为补充：仿真是「用激励抽样试」，FPV（Formal Property Verification，形式属性验证）是「用数学证明」。

本文要回答的问题

• 不写测试向量，形式工具凭什么断言一条属性「永远成立」？
• SVA 里 assert、assume、cover 三个语句各自承担什么语义，写错 assume 为什么会把 bug「假设掉」？
• bounded proof 和 full proof 差在哪，inconclusive 算不算没验证？
• 工具报出 counterexample 之后怎么用？为什么说反例就是最短复现波形？
• 哪类模块上 FPV 性价比最高，状态空间爆炸时怎么办？

一、从「抽样试错」到「数学证明」

仿真的工作方式是抽样：给定一条输入序列，观察这一条路径上的行为。一个 32 位数据通路加上几个控制位，每个周期的输入组合就是天文数字，仿真覆盖率再高也只走了状态空间里极小的一片路径。靠随机碰上空满边界、协议死锁这类深度边角组合，概率往往低到可以忽略。

形式属性验证 FPV 换了一条路。它把 RTL 设计展开成一个有限状态转移模型：所有触发器构成状态向量，所有输入构成每个周期的自由变量，状态之间按组合逻辑转移。你不需要提供任何激励，只需要提供两样东西——用 assume 描述「环境允许给出的合法输入」，用 assert 描述「设计必须保证的结论」。工具从复位状态出发，符号化地遍历所有可达状态、所有输入序列，数学地判定 assert 是否可能被违反。

举个具体的边角例子：一个深度 16 的 FIFO，在「还剩一格、同一拍上游突然背靠背连推两拍、下游恰好停读一拍」的组合下会不会溢出？仿真要撞上这个组合，需要空满计数、上游相位、下游停顿三者恰好对齐，随机回归跑几天也未必覆盖；而对 FPV 来说这只是状态空间里一个普通节点，工具不需要「运气」，只要该节点可达且溢出逻辑有错，就一定能走到它面前。

读图抓住一件事：激励空间被 assume 收窄，结论由 assert 给出，工具穷举的是收窄后的全部可能，而不是某几条波形。三种结论里，proven 表示在给定约束下不存在任何违反序列；counterexample 表示确实存在一条违反路径，工具直接返回从复位出发的最短波形；inconclusive 表示在现有证明深度和算力下既没证出也没找到反例——它不是「没问题」，只是「暂无结论」。

cover 是第三个角色。assert 问「坏事会不会发生」，cover 问「好事到不到得了」：cover property (req && gnt) 命中表示工具确实能构造出 req 与 gnt 同时有效的状态序列。cover 的价值在第三节展开，它是识别「空证明」的探针。

二、assert / assume / cover：三种语义，一份最小范例

以一个简单的 req/gnt 握手模块为例，下面三条 SVA（SystemVerilog Assertions）构成一组完整的形式环境：

// assume：上游合法输入约束。req 一旦拉高必须保持，直到拿到 gnt
assume property (@(posedge clk)
  $rose(req) |=> req throughout gnt[->1]);

// assume：数据在 valid 期间不允许出现 X
assume property (@(posedge clk) valid |-> !$isunknown(data));

// assert：要证明的结论——请求后 1~3 拍内必须 grant
assert property (@(posedge clk)
  $rose(req) |-> ##[1:3] gnt);

// assert：互斥安全属性——绝不能同时 grant 两个请求方
assert property (@(posedge clk)
  !(gnt[0] && gnt[1]));

// cover：确认握手确实能发生，且背靠背场景可达
cover property (@(posedge clk) req ##1 gnt);
cover property (@(posedge clk) gnt ##1 gnt);

再给一组 FIFO 上几乎是「标准答案」的属性，可以直观感受 FPV 属性怎么从规格直接翻译：

// 空时不能读，满时不能写——指针与标志的不变量
assert property (@(posedge clk) empty |-> !rd_en);
assert property (@(posedge clk) full  |-> !wr_en);

// 读写指针差与计数器恒等：任何一拍都成立的内部不变量
assert property (@(posedge clk)
  fifo_count == ((wr_ptr - rd_ptr) & PTR_MASK));

// 覆盖完整生命周期：空、半满、满、空满同拍穿越都要可达
cover property (@(posedge clk) empty);
cover property (@(posedge clk) full);
cover property (@(posedge clk) wr_en && rd_en);

注意最后两条 assert 描述的是「内部一致性」而非外部可见行为——这类不变量在仿真波形上没人会逐拍核对，却是 FPV 最擅长收割的目标：指针逻辑只要在某一拍算错一拍，属性立刻失败。

三个语句的语义差别必须记牢，FPV 一半的坑都出在把它们混用：

语句	语义	约束对象	写错的后果
assume	条件必须成立，工具据此限制输入	环境/输入端口	过强则把 bug 假设掉，过弱则状态爆炸
assert	条件必须成立，工具去证伪它	设计本身的行为	属性写错会证明一个无意义的结论
cover	条件能否被达到，只需一条路径	可达性探针	不写则无法发现 vacuous（空）证明

SVA 的时序算子也值得点几个最常用的：|-> 是同一拍蕴含，|=> 是延迟一拍蕴含；##[1:3] 表示 1 到 3 拍的区间；$rose/$fell 检测边沿；gnt[->1] 是同步触发点，表示「等到 gnt 第一次出现」；throughout 要求某条件在整段区间持续。写 FPV 属性时优先用这些时序算子表达「事件—响应」关系，而不是手写计数器去数周期——前者工具更容易推理，也更贴近规格语言。

三、bounded proof 与 full proof：证明深度的边界

形式引擎并非总能一次性回答「永远成立」。实践中你会给工具设一个证明深度 N（单位是时钟周期），工具先保证「从复位出发 N 拍以内不存在违反」，这叫 bounded proof（有界证明）。随着 N 增大，如果引擎完成了状态空间的不动点归纳——即证明了任意可达状态出发都不可能违反，不再依赖具体深度——才得到 full proof（完全证明）。

这张图解释了工程里最常见的三种处境。控制逻辑简单、状态位少的模块（仲裁器、FIFO 指针），几十个周期内状态空间就收敛，通常能直接拿到 full proof；带大计数器、深度数据通路的模块，工具只能停在 bounded proof，此时它的含义是「N 拍以内安全」，深度选择要有依据——比如证明深度至少覆盖 FIFO 从空写满、再读空的完整生命周期，而不是随手填一个数；如果连设定深度都跑不完，结果就是 inconclusive。

cover 在深度问题上同时充当判据：如果连 cover property (full)（FIFO 满状态可达）都覆盖不到，说明证明深度或约束根本没有探索到那块区域，此时任何关于「满状态下不溢出」的 assert proven 都值得怀疑——前提状态压根没到达，蕴含式真空成立。

深度怎么取才有说服力？还是拿深度 16 的 FIFO 算：从空开始，只写不读需要 16 拍才满，满后同拍读写、再连续读出清空又是十几拍，证明深度至少要覆盖这样一个完整往返，取 40~50 拍才算把空满边界两侧都走过。仲裁器则换一套账：公平性属性要求「每个请求方在 K 拍内必然被服务一次」，证明深度必须明显大于 K 并留出复位后建立的前置拍数，否则工具只证明了一个谁都来不及饿死的短窗口，结论形同虚设。深度不是越大越好——每加几拍，求解时间可能翻几倍——而是对着属性的最坏合法场景反推出来的。

四、counterexample：反例就是最短复现波形

FPV 最受工程师欢迎的产物，是失败时自动给出的 counterexample（反例波形）。模型检查算法在搜索违反路径时，天然返回从复位状态到违反点的最短序列：哪一拍复位撤销、哪一拍输入取什么值、设计内部每一个触发器如何跳转、在哪一拍 assert 首次失败，全部列在波形里。

这和仿真调试形成鲜明对比。仿真发现一个罕见死锁，你往往先要复现——随机种子、相位、外围时序缺一不可，复现出来的波形前面还裹着成千上万拍无关流量；FPV 的反例通常只有几拍到几十拍，每一拍都是构成违反而不可删减的环节，失败根因几乎直接摊在桌面上。读反例波形的标准顺序是：先定位 assert 失败的末端周期，再沿波形往回看第一个偏离规格预期的内部信号，那个信号通常就是 RTL bug 或错误约束的交汇点。

走一遍典型的读反例过程：假设互斥属性 !(gnt[0] && gnt[1]) 失败，反例一共 7 拍。末拍两个 grant 同时为高；往回倒，第 6 拍仲裁器的 last_winner 指针在某路请求后撤时没有更新，停在了陈旧值；再往前看，第 4 拍复位刚撤销、两路请求恰好同拍拉高——问题就定位到「同拍请求且恰遇复位后首次仲裁」这个初态分支，优先级编码在该分支上漏了一路。整个定位不需要猜，因为最短波形里没有多余动作。

也要提醒：反例可能是设计的错，也可能是你 assume 写错了——比如你忘记约束某个合法输入关系，工具构造出一条「现实中上游永远不会给」的非法序列，assert 当然失败。看到反例先判它是否属于合法输入空间，再决定改 RTL 还是补 assume。

五、FPV 适合什么、不适合什么

FPV 与仿真不是替代关系，分工由问题性质决定：

维度	仿真	FPV
输入空间	激励实际走到的路径	assume 内的全部序列
边角组合	低概率，依赖约束随机	数学穷尽，天然覆盖
失败产物	需复现的长波形	最短反例波形
规模上限	全芯片可跑	中小模块，受状态爆炸限制
数据运算正确性	直观，易参考模型对比	位宽大时难以收敛
典型用途	数据流、性能、整体回归	控制、仲裁、协议、不变量

FPV 性价比最高的模块有共同特征：控制密集、状态空间紧凑、正确性可以表述成几条不变量。

• 仲裁器与调度：互斥 grant、不饿死、轮询公平、req 到 gnt 的时延界；
• 握手与接口协议：AXI/APB/PCIe 的 valid/ready 规则、 outstanding 计数、乱序返回 ID 合法性；
• FIFO 与队列：空满标志与指针关系、不溢出不下溢、同步/异步穿越的不变量；
• 状态机与缓存一致性：非法状态不可达、状态迁移完备、目录/MESI 协议不变量；
• 复位与低层控制：仿真里概率极低、人工很难凑出的深度组合故障。

不适合硬上的场景同样明确：宽数据通路的算术正确性（DSP、浮点、大位宽运算）、含大容量存储的整块设计、没有清晰属性可写的「整体功能正确性」、以及动辄数十万触发器的 SoC 级验证。对这些目标，引擎很快在指数膨胀的状态空间面前返回 inconclusive。

如果是第一次在项目里引入 FPV，选第一个靶子有讲究：挑一个已经在仿真里出过 bug、规模几百行以内、规格能列出三到五条硬规则的控制模块——仲裁器和握手控制几乎是不会失手的起点。几小时拿到全绿证明和若干真实反例，既能校准团队写 assume 的手感，也比在大模块上吃一次 inconclusive 更容易建立信心。等流程跑顺，再按 验证计划 Testplan 把控制类功能点系统地迁到 FPV 轨上。

六、状态空间爆炸与约束建模的纪律

状态空间爆炸是 FPV 唯一的硬约束。状态位每增加一个，潜在状态数翻倍；一个自由的 32 位输入端口意味着每拍 2^32 种选择。工程上的标准对策是一套组合拳：切模块，只验证边界清晰的单元而非整个 SoC；黑盒化，把存储器、大 FIFO、无关子模块替换为抽象模型或约束接口；抽象数据，把宽数据通路缩成若干符号值，只保留与控制相关的位；设证明深度，先用 bounded proof 拿到有界保证，再逐步加深争取收敛。

约束建模则有两个对称的失败方向。over-constrain（过约束）：assume 比真实环境严格，把设计本该处理、现实中也确实会出现的输入排除在外，bug 被「假设掉」，属性 vacuous 成立——报告一片绿色，问题留到硅片上。under-constrain（欠约束）：assume 比真实环境宽松，工具在大量非法输入上证明，要么 inconclusive，要么报出不属于合法空间的假反例。检验纪律只有一条：让 assume 与上游规格逐条对应，并用一组 cover 把关键合法场景全部点亮——关键 cover 不亮，说明约束过强或深度不够；非法 cover 也能亮，说明约束有漏洞。

模块级 FPV 还有一个好用的接口纪律：assume-guarantee 对接。验证上游模块时，它对下游的承诺写成 assert（保证 valid 不会无征兆拉高）；验证下游模块时，同一条接口规则写成 assume（只接收这样的上游）。两边规格文本逐条对齐，模块各自独立证明，拼起来才不会出现「上游证明的东西和下游假设的东西根本不是一回事」。这也是切分大设计时保持正确性闭环的标准做法。

此外还有两个高频坑：复位和初值必须显式建模——复位是同步还是异步、是否所有触发器都被复位覆盖、复位期间输入允许什么状态，都要写清楚，形式引擎的默认起点错了，后面全部证明都不成立；断言本身要评审，证明一条写错的 assert 毫无意义，属性评审应当和 RTL 评审同等严肃，最好由没写这条属性的人对照规格复读一遍。

这一篇在知识体系里的位置

本篇属于芯片设计验证进阶层，回答「不用激励如何获得穷尽式保证」。向前读，形式方法的整体地图见 形式验证入门；横向配套，FPV 属性从哪来、按什么优先级书写，应回到 验证计划 Testplan 里逐条映射功能点，仿真侧的进度度量则见 覆盖率收敛——有经验的团队用 FPV 提前封死控制类边角坑、把仿真算力省给数据流和系统场景；向后读，同一套 SVA 断言也可以挂在仿真里做在线检查，并进一步延伸到等价性检查（LEC）等其他形式分支。

总结

一句话总结：形式属性验证 FPV 不写测试向量，而是用 assume 限定合法输入空间、用 SVA assert 表述必须成立的不变量、用 cover 确认关键状态可达，形式引擎符号遍历全部可达状态，给出 full/bounded proven、最短 counterexample 反例波形或 inconclusive；它在仲裁、握手、FIFO、协议状态机这类控制密集、边角组合多的模块上性价比碾压仿真，对宽数据运算和大设计则受制于状态空间爆炸，需要切模块、黑盒化与数据抽象；成功的关键是精确建模约束、用 cover 防止 vacuous 空证明、按生命周期选择证明深度，并警惕 over-constrain 把真 bug 一起「假设掉」。