FPGA 形式验证：属性证明与等价性检查
更新时间：2026-10-01。很多 FPGA 团队的验证闭环是「仿真跑一批定向用例 + 上板看现象」，对数据通路类设计这够用，但握手死锁、仲裁饥饿、综合把关键逻辑优化没这类问题，定向激励很难恰好踩到。形式验证不靠枚举用例，而是对全部可能输入证明性质，恰好补在这个缺口上。本篇按标准篇深度展开 FPGA 形式验证的落地，断言语法基础可先看 SVA 断言实践，方法论背景见 形式验证入门：assert/assume/cover、bounded proof 与 FIFO/仲裁器验证。
本文要回答的问题
- 形式验证和仿真、上板测试的本质差别是什么，为什么它不需要写激励？
- 「设计必须满足的性质」怎么写成 SVA，模型检查又怎样给出证明或反例？
- 综合、HLS、加密 IP 交付之后，为什么要做 LEC 等价性检查，被综合优化掉的逻辑怎么核对？
- 连接性检查查什么，形式检查点应该插在 FPGA 流程的哪几个时机？
- 状态爆炸是什么，靠什么手段让证明收敛？
一、从「跑用例」到「证明性质」
仿真的本质是抽样：给定一组输入序列，观察 DUT（Design Under Test，被测设计）这一条路径上的行为。哪怕随机回归跑几亿拍，覆盖到的状态相对全部可能状态仍近乎零——一个 32 位计数器配几十个控制位，状态空间是天文数字。形式验证换了一条路：把 RTL 和性质都建成数学模型（状态迁移关系加逻辑命题），由模型检查器（model checker）在全部可达状态上判定性质是否恒成立。成立则给出证明，不成立则自动生成一条触发违例的最短反例波形，整条过程不需要任何测试激励，所以也叫无激励验证。
这张图要传达的核心是两种方法的结论强度不同：仿真跑绿了只说明走过的路径没出错，形式证明过了则说明不存在任何合法输入能违例。但注意「合法输入」四个字——形式只在 assume 划定的输入空间里证明，假设写错，证明再漂亮也只是证明了一个现实中不存在的世界。
| 维度 | 仿真 | 形式验证 | 上板测试 |
|---|---|---|---|
| 是否需要激励 | 需要，定向或随机 | 不需要，只写性质与假设 | 需要真实数据流 |
| 覆盖范围 | 抽样的若干路径 | 全部可达状态（收敛时） | 真实工况的子集 |
| 失败交付物 | 波形，靠人复现定位 | 最短反例，自动生成 | 现象，最难复现 |
| 擅长 | 数据正确性、长流量 | 握手/仲裁/状态机/互连 | 系统级、软硬件协同 |
| 主要成本 | 用例与回归时间 | 写假设、调收敛 | 板子与调试时间 |
三者不是替代关系：仿真验数据内容和长流量，形式穷尽控制逻辑边角，上板兜底真实接口与系统协同。仿真加速的整体取舍可回看 仿真加速与覆盖率。
为什么 FPGA 团队过去少用形式？两个现实原因。一是 FPGA 有「反正能上板试」的退路，试错成本远低于流片，团队没有被逼到穷尽验证；二是形式工具长期面向 ASIC 签核，价格与流程都重。但随着单颗 FPGA 承载的设计越来越大、部署到量产现场后无法随时换板（见量产与可靠性约束），「上板试出来」的代价并不低——很多握手死锁要在特定流量配比下连续运行几天才出现，实验室里根本等不到。形式验证在 FPGA 侧的合理定位因此不是 ASIC 式的全套签核，而是挑出那几个「仿真碰不到、上板复现难」的控制模块重点证。另外要分清形式验证与门级仿真/X 传播检查的边界：后者用向量在网表上跑、暴露复位与 X 态问题，前者不依赖向量，两者可以互相印证，方法区别见 门级仿真、SDF 与 X-prop。
二、属性、断言与模型检查
FPGA 形式验证最常用的形态是 FPV（Formal Property Verification，属性形式验证）：用 SVA（SystemVerilog Assertion）写 assert，工具把 DUT 和断言一起交给求解引擎。除了 assert，FPV 里还有三件配套：assume 约束输入环境、cover 检查某状态/序列是否可达、restrict 限定证明空间。四者分工和 bounded/unbounded 证明深度在 形式验证工程应用：FPV、有界/无界证明在控制逻辑上的落地 里有完整论述。
// valid 一旦拉高，在 ready 到来之前必须一直保持
a_valid_hold: assert property (@(posedge clk) disable iff (!rst_n)
$rose(valid) |-> valid throughout (!ready)[->1]);
// FIFO 满时不能再写（安全性质）
a_no_overflow: assert property (@(posedge clk) disable iff (!rst_n)
full |-> !wr_en);
// 请求最终必被响应（活性，证明时使用，仿真中一般加有界窗口）
a_live_resp: assert property (@(posedge clk) disable iff (!rst_n)
req |-> s_eventually gnt);
// 环境假设：ready 不会永远拉低，否则握手本身无意义
m_ready_returns: assume property (@(posedge clk) disable iff (!rst_n)
ready |-> s_eventually ready);
// 可达性：满状态必须能走到，否则「不溢出」可能是空证明
c_reach_full: cover property (@(posedge clk) disable iff (!rst_n) full);性质分两类，写漏一类是形式验证最常见的失误。**安全性质（safety）**声称「坏事永远不发生」：不溢出、不死锁、grant 互斥、握手合法；**活性（liveness）**声称「好事最终发生」：请求最终有响应、出口最终能排空。只证 safety 会漏掉「接口合法但永久卡住」的死锁。
| 性质类型 | 典型句式 | 例子 | 仿真能否判定 |
|---|---|---|---|
| safety | 永不为 / 任何时刻都 | full 时禁写、grant one-hot | 能，逐拍检查 |
| liveness | eventually、最终 | req 最终被 gnt | 无界式不能，需有界窗口 |
| cover | 可达性 | 满/空、反压窗口能走到 | 能统计是否出现 |
模型检查器的工作方式有两种：无界证明（unbounded）给出对任意深度恒真的完整结论；有界证明（bounded，深度 k）只保证 k 拍内不违例，深度逐轮加深直到完整收敛或工程上认为足够。工程实践中大量性质先 bounded 快速抓 bug，再冲 unbounded 签核。
形式环境还有几个 FPGA 特有的设置点。第一是复位与初值：FPGA 配置完成后寄存器初值由比特流决定，很多上电初值并非全零，证明的起始状态要按真实初值约束，否则可能证出一批「复位后几拍内」的假违例。第二是时钟：门控时钟和多时钟域不能简单当单时钟处理，跨时钟信号要么按 CDC 协议抽象成同步后的安全信号，要么用多时钟断言，CDC 背景见 CDC 与亚稳态。第三是 X 态：形式引擎默认信号非 0 即 1，不存在仿真里的 X，依赖 X 传播才能发现的问题要交给门级仿真。这些设置点决定了「同一份 RTL、同一条断言」在仿真环境和形式环境里并不直接通用，接口和假设要分别配置，这也是高级 testbench 与形式环境各自维护一套约束的原因，参考 高级 Testbench。
三、反例：形式验证最值钱的产物
性质证不过时，工具输出的不是一句 fail，而是一条从复位状态走到违例点的最短波形——短到通常只有几拍到几十拍，且每一拍的输入都是工具构造出来的。这类边角序列人脑几乎造不出来：比如「第七拍反压、第九拍另一口插入、第十三拍释放」恰好导致指针错乱。
处理反例先问一个分叉问题：违例路径上的输入是否合法？若输入合法，是设计缺陷，改 RTL；若输入现实中根本不可能出现（比如两个互斥模式同时开启），是 assume 漏写，补约束后重跑。切忌把反例直接 waive——那等于宣告性质放弃。修完还要回归关联性质，因为改动常引出新的违例。
四、等价性检查：核对综合与优化没改行为
LEC（Logical Equivalence Check，逻辑等价检查）是形式方法在 FPGA 流程里的另一大用途。它不跑向量，而是形式化比较两份设计在所有输入下输出是否逐拍一致，工具先自动匹配两份网表的 key point（寄存器、端口、锁存器），再对每个匹配点证明组合锥逻辑等价。详细机理见 逻辑等价检查 LEC/Formality。
FPGA 场景下 LEC 有三个高频落点。一是 RTL 对综合后网表：综合器做常量传播、死逻辑消除、信号合并、跨层次优化，信号可能改名甚至消失，key point 匹配不上时，先去综合报告查该寄存器是被吸收进 BRAM/DSP 原语还是被判定无用——「被优化掉」既可能是正确的死逻辑消除，也可能是复位接法导致寄存器被推断成锁存器或常量，必须逐类核对，不能笼统认为是优化。二是 HLS C 对生成 RTL、生成 RTL 对手写 RTL：HLS 工具的接口综合、数组分割、流水化都会改变微架构，C 仿真过了不等于 RTL 行为一致，HLS 侧的机理见 HLS 深水区。三是加密/第三方 IP 与加密前参考、跨工具（Vivado 与第三方综合）结果的核对，这类只能以黑盒边界做比较。
| LEC 场景 | Golden | Revised | 重点核对 |
|---|---|---|---|
| 综合前后 | RTL | 综合网表 | 被优化掉的寄存器、原语吸收 |
| HLS 流程 | C/C++ 或生成 RTL | 生成 RTL / 手工改写 | 接口协议、II 变化、数组映射 |
| ECO/小改 | 改前网表 | 改后网表 | 改动锥与未动部分 |
| 加密 IP | 交付前 RTL | 加密网表 | 黑盒边界一致性 |
五、连接性检查与形式检查点的插入时机
连接性检查（connectivity check）用形式方法核对「某个端口/寄存器确实连到了期望的目标」：地址解码落到正确 slave、中断源接到正确控制器、AXI ID 通路没有错接、安全模块的隔离信号真正串在通路上。它替代的是人工在原理图里追线——Block Design 里 IP 几十上百个，一根线漏接或接错位，仿真未必走到、上板却必炸。连接性与 lint、CDC 同属「把错误挡在综合之前」的静态门禁，可与 FPGA RTL 质量检查 的 lint/CDC 流程并行组织。
连接性检查的规则写法通常不需要时序语义，而是声明结构化关系：例如「地址落在 0x4000_xxxx 区间时，该 slave 的 cs 必拉高且其余 slave cs 为低」「axi_tx 的 irq_out 必连到中断控制器的第 7 路输入」。工具把全芯片网表展开后沿连线形式化追踪，几秒钟就能给出上百条规则的结论，漏接、错接、多驱动、悬空端口一并报出。Block Design 的自动连线很方便，但越是自动连接，越值得用连接性规则做一次独立核对——自动化消除了手误，却也消除了你对每根线的记忆。
插入时机遵循一个朴素原则：离缺陷引入点越近越好。模块级 FPV 在 RTL 冻结前就能跑，握手、仲裁、状态机各证各的；连接性检查放在集成完成、综合之前；LEC 放在综合之后、布局布线之前，因为此时网表稳定且综合优化的影响已经全部体现；HLS 链路在 C 综合出 RTL 后立刻做等价核对；后续每次 ECO 或优化策略调整，LEC 增量重跑即可，不必全量重来。
六、复杂度、抽象与收敛
形式验证的天花板是状态爆炸：设计状态随寄存器位宽指数增长，100 个触发器理论上有 2^100 个状态。数据通路越宽（乘法器、宽 FIFO、宽总线），求解器的 BDD/SAT 引擎越难收敛，表现为证明长时间停在某个深度不动或直接报内存耗尽。控制密集、状态空间适中的模块——握手、FIFO 控制、仲裁器、状态机、缓存一致性控制——是形式的甜区；巨型数据通路交给仿真和上板更实际。
让证明收敛的手段按成本从低到高排列：
| 手段 | 做法 | 注意点 |
|---|---|---|
| 分块 | 只取模块级 DUT，不一次证全芯片 | 接口协议用 assume 补全 |
| 加假设 | 约束数据内容、模式互斥、有界 burst | 防假设过窄，逐条评审 |
| 黑盒化 | 把存储器/PLL/宽数据通路设为黑盒 | 黑盒边界改由连接性检查守 |
| 抽象 | 用小位宽参数证明，再论证泛化 | 泛化论证要有依据，不能想当然 |
| 换引擎/加深深度 | SAT、BMC、不同证明引擎切换 | bounded 结果不能当 unbounded 签 |
给一个收敛过程的直观感受。一个带 4 路请求的 round-robin 仲裁器，20 条左右性质通常在几分钟内全部 unbounded 证完；同一个模块若把 32 位数据完整性也纳入断言，深度往往爬到几十拍后停滞，因为求解器被迫追踪数据通路的全部位组合。把数据通路黑盒化、只证控制与 ID 顺序后，证明立刻恢复收敛。这说明「证不动」多数时候不是工具不行，而是验证对象选错了——形式要证的是控制决策的性质，数据算没算对属于仿真和参考模型的地盘。判断「假设是否过窄」有个简单动作：每条 assume 都配一条对立的 cover——假设「burst 不超过 16」，就 cover 一次长度 16；若 cover 不可达，说明别的假设把它更早堵死了，约束间存在矛盾。这样既防漏证，也防「证明了一个用不到的世界」。工具层面，FPGA 厂商流程里可选用 Vivado 的形式相关检查与连接性/Xilinx Formal 方案，独立工具则有 Siemens Questa Formal（原 Questa Formal Verification）、Synopsys VC Formal、Cadence JasperGold，LEC 领域常用 Siemens SLEC（含 C-to-RTL）与 Synopsys Formality；多数 FPGA 团队不必买全家桶，按「模块 FPV + 综合后 LEC + 集成连接性」三个点选配即可。
这一篇在知识体系里的位置
- 向上承接：SVA 断言实践 提供断言语法，形式验证入门：assert/assume/cover、bounded proof 与 FIFO/仲裁器验证 提供方法论入门。
- 方法深入：形式验证工程应用：FPV、有界/无界证明在控制逻辑上的落地 讲收敛、假设与签核，逻辑等价检查 LEC/Formality 讲 key point 与网表比较机理。
- 横向相关：FPGA RTL 质量检查 的 lint/CDC 门禁、HLS 深水区 的接口综合，以及 仿真加速与覆盖率 的仿真分工。
总结
FPGA 形式验证用数学证明替代激励枚举：FPV 用 SVA 的 assert/assume/cover 对全部可达状态穷尽握手、仲裁、状态机的安全与活性，证不过即给最短反例；LEC 在综合与 HLS 之后形式化核对 RTL 对网表、C 对 RTL 的逐拍等价，专治「逻辑被优化掉」；连接性检查守集成期的错接漏接；三类检查点分别插在模块冻结、综合前后与 ECO 迭代处，遇到状态爆炸就分块、加假设、黑盒与抽象，与仿真和上板互补而非互相取代。