形式验证（一）：用数学遍历替代激励去「证明」属性（B3）
设计侧形式基础见 形式验证基础、断言写法见 SVA 实践；本篇讲属性检查工具（Cadence JasperGold、Synopsys VC Formal）内部怎么证、怎么写能收敛的断言。组合等价（LEC）是 B4，本篇讲时序属性的模型检查。
一、核心思想：从「抽样运行」到「穷尽状态」
仿真是在时间上跑某一条具体输入序列，覆盖再高也只是抽样——没跑到的 corner 永远是黑的。属性证明（model checking）换了个问题：
给定设计 D 和一条用时序逻辑（SVA/PSL）写的性质 P，是否存在任意合法输入序列、任意可达状态，使 P 被违反？
工具不显式枚举所有输入（组合爆炸），而是用 SAT/SMT、BDD、符号执行在状态空间上推理：若能推出「违反 P 的状态不可达」，性质被证明（proven）；若找到一条最短路径能到达违反状态，给出反例轨迹（counterexample waveform）——这是一条确定能复现 bug 的具体激励，比仿真偶发失败更好 debug。
三类语句构成一个证明环境：assertion（要证恒真的性质）、assumption（约束合法输入/环境，工具据此剪枝）、cover（证明某状态/序列可达，防止约束把输入限死到「什么都不会发生」的真空证明）。
二、有界、无界与归纳：为什么有「证明深度」
| 方法 | 在做什么 | 局限/用途 |
|---|---|---|
| 有界模型检查 BMC | 在 k 拍以内找反例（把 k 拍展开成 SAT） | k 内无反例不等于全证明；擅长找深 bug |
| 无界模型检查 | 证明任意深度都无反例（BDD/插值） | 状态空间大时不收敛 |
| 归纳（k-induction） | 设「连续 k 拍成立」归纳推出下一拍成立 | 配合 strengthening（加辅助不变量）才收得敛 |
工具常报告 proven、fired（被违反，给反例）、inconclusive/bounded（只证明到深度 k）。bounded 不是 proven——只说明前 k 拍没问题，这是新手最容易误读的结论。
收敛难是属性形式的主旋律：设计越大、状态越多，工具越可能跑到算力上限仍 inconclusive。工程上靠抽象与切分帮它。
三、哪些性质适合形式（投入产出高）
形式不是万能，它最擅长控制密集、状态有限、正确性边界清晰的逻辑：
- 仲裁器/调度器：互斥（两个请求者不会同时拿到授权）、公平性、无死锁；
- FIFO：满不写、空不读、指针不越界、读写后计数正确（FIFO、异步 FIFO）；
- 总线/协议：AXI/AHB/valid-ready 的合法序列（valid/ready、AXI-Lite），常直接用厂商提供的协议 assertion IP；
- 控制 FSM/握手：状态合法跳转、req/ack 不会丢请求、glitch-free 时钟切换（无毛刺时钟 MUX）；
- 访问保护/安全寄存器：越权不可达（与安全属性相关）。
不适合纯形式的：大数据通路的数值正确性（用仿真/参考模型比）、需要真实软件长序列的场景、整颗 SoC（太大）。这类可以形式证控制、仿真证数据，或形式 + Emulation 分工（选择见 仿真/原型/Emulation 选型）。
四、写能收敛的证明环境：关键是切边界
直接对整芯片证明一条顶层断言几乎必然 inconclusive。可收敛性工程：
- 设合理 assume：把上游约束成合法协议（如输入本就经过两级同步、valid 不会在握手中途撤），剪掉不可能输入；但要用 cover 确认主要场景仍可达，避免「假设到永远不会有请求」的假证明；
- 黑盒化无关模块：把大存储器/数据通路当 black box/抽象模型，只留待证控制逻辑；
- 加辅助不变量（strengthening）：归纳证不动时，补充中间性质（如「指针差始终在界内」）作为引理，先证引理再用它证目标；
- 分层证明：先证子模块局部性质，再把它作为上层 assume/引理，逐层抬高；
- 复位与初始状态：明确证明起点（复位后状态），避免工具从任意非法初态推出伪反例。
五、读反例与回归
fired 给出的 CEX 是一条最短违反序列，配合源码像波形一样回放：先确认是真 bug还是 assume 写错（环境约束漏了，允许了不可能输入）——后者在形式里极常见，修假设后重证。属性验证的回归是把 proven 的断言集随 RTL 每次合入重跑：属性不依赖激励，一旦写好，后续改动破坏性质会被立即抓住，这正是它比定向仿真更适合做结构正确性守夜人的原因。
与 LEC/仿真的分工
- vs B4 LEC：LEC 证「两份设计功能等价」（组合/寄存器映射），不需要写性质；B3 证「一份设计满足某条行为属性」，要写 assertion/assume。两者都属形式但问题不同；
- vs 仿真：仿真证「在这些激励下对」，覆盖有限但能跑大数据和真实场景；形式证「在所有合法输入下对」，穷尽但受规模约束。验证收口两者互补（覆盖率 衡量仿真盲区，形式负责把控制类盲区变成 proven）。
相关与延伸
- 静态族：B1 Lint、B2 CDC/RDC、B4 LEC；仿真侧：A1 仿真器、A2 覆盖率。
- 设计/方法：形式验证基础、SVA 断言、Emulation 选型。
总结
属性证明不靠激励抽样，而是用 SAT/BDD/归纳在状态空间上回答「是否存在任意合法输入序列违反这条 SVA」，结果是 proven、给出最短复现反例的 fired，或只到深度 k 的 bounded（不等于证明）；它最适合仲裁、FIFO、总线协议、控制 FSM 这类控制密集且边界清晰的性质，收敛的关键不是堆算力而是切边界——用合理 assume 剪枝、用 cover 防真空证明、黑盒大数据通路、补辅助不变量、分层设引理，并先区分 fired 是真 bug 还是假设写错；它与证等价的 LEC、跑真实数据的仿真互补，一旦断言写好就能在每次合入时穷尽守夜，把控制类盲区从「没覆盖到」变成「已证明」。