3.1 本章学习任务：从“动态仿真”走向“形式化证明”
在SoC芯片验证流程中，传统仿真（Simulation）需要在测试向量上反复运行RTL模型，验证覆盖率依赖于激励质量。形式化验证（Formal Verification）则不同：它用数学推理取代激励驱动的动态仿真，对设计空间进行穷尽式证明。等价性检查与模型检查，是形式化验证最核心的两大支柱。
本章聚焦两个问题：
- 如何证明两个设计（RTL vs 网表、RTL vs RTL）在所有输入下行为完全一致？—— 等价性检查（Equivalence Checking）
- 如何证明一个设计在所有可能的状态转换中，永远满足给定的属性（安全、活锁、死锁等）？—— 模型检查（Model Checking）
3.2 核心概念：两种技术到底在“检查”什么
| 维度 | 等价性检查（EC） | 模型检查（MC） |
|---|---|---|
| 验证对象 | 两个设计（逻辑锥）是否功能等价 | 单一设计是否满足一组属性（Assertions） |
| 输入形式 | 参考设计 + 实现设计 + 映射关系 | RTL模型 + 属性（SVA/PSL） |
| 输出 | 等价（Pass）/ 不等价（Fail + 反例波形） | 满足（Proof）/ 违反（Counterexample Trace） |
| 适用阶段 | ECO后、综合后、扫描链插入后、时钟树综合后 | 模块级验证、控制逻辑、总线协议、流水线冲突检测 |
| 复杂度特征 | 可达状态复杂度较低，主要处理组合逻辑锥 | 状态空间爆炸，需要架构抽象、抽象/细化策略 |
站在工程视角，可以把等价性检查理解为“逐对逻辑锥的数学比对”，把模型检查理解为“对状态图的属性遍历”。两者互补：EC保证后端流程没有改变功能；MC保证前端设计本身满足安全/活性的技术规范。
3.3 原理机制：组合逻辑锥与状态空间遍历
（1）等价性检查的数学基础
等价性检查把设计切分为数千个“逻辑锥”（Logic Cone）。每个逻辑锥由一个比较点（Comparison Point）——通常为寄存器输入、输出端口或黑盒边界——回溯其组合逻辑扇入区域。EC引擎对每对对应的逻辑锥进行布尔函数等价性证明。
等价性检查工作流：
参考设计（Golden）：综合前 RTL
实现设计（Revised）：综合后网表 / ECO后网表 / 时钟树综合后网表
1. 映射（Mapping）：识别两个设计中的对应比较点（寄存器、端口、RAM宏单元）
2. 逻辑锥提取：从每个比较点回溯扇入，构建布尔函数
3. 功能等价性验证：使用BDD（二元决策图）或SAT求解器证明两函数是否等价
4. 结果报告：等价类（Equivalent / Non-Equivalent / Aborted）
（2）模型检查的数学基础
模型检查将一个设计建模为有限状态迁移系统（Kripke Structure），然后遍历状态空间验证时态逻辑属性。常用的属性语言是SVA（SystemVerilog Assertions）和PSL。核心算法分为两类：
- BDD-based Symbolic Model Checking：使用二元决策图隐式表达状态集合，适合控制逻辑密集的模块，能一次性证明较宽泛的属性，但容量受BDD变量排序影响。
- SAT-based BMC（Bounded Model Checking）：将“给定长度k内是否存在反例”编码为SAT问题求解。BMC主要用于找反例（Debug），配合无界模型检查（UMC）可完成完整证明。
3.4 实战流程：EC与MC的标准步骤
等价性检查（EC）四步法
- 准备参考设计与实现设计：设置顶层环境，定义常数值（Const）、断开时钟/复位，指定扫描链相关接口（如scan_enable）。
- 运行映射（Match）：工具自动匹配寄存器、锁存器和黑盒。匹配率低于99%时需要人工介入检查匹配失败的比较点。
- 运行验证（Verify）：对每个逻辑锥做等价性证明。对无法直接证明的锥，工具自动调用高层策略（如“分析点”“变换逻辑锥”）。
- 诊断与ECO验证：对Non-Equivalent点生成反例波形，定位差异来源；ECO修改后再验证，确保修复没有引入新问题。
模型检查（MC）实战步骤
- 构建属性集合：将设计规范拆分为安全属性（不允许发生）与活性属性（最终会发生）。例如：总线协议中“grant”信号必须在request置位后最多16个周期拉高。
- 抽象与建模：把复杂RAM/模拟宏替换为透明黑盒；约束时钟和复位，控制状态空间规模。
- 求解与反例分析：运行BMC寻找反例；如果反例存在，检查是真实bug还是属性约束过强（Overconstraint）或环境建模错误。
- 完整证明与收敛：使用无界模型检查、IC3/PDR算法（如Cadence JasperGold、Synopsys VC Formal）完成完整证明。
3.5 案例说明：一个总线仲裁器的EC + MC联合验证
案例背景：一款SoC中的AHB总线仲裁器，包含固定优先级和轮询模式。前端已完成RTL设计，后端完成了综合和扫描链插入。
- MC阶段：用JasperGold验证5条属性。其中“当master0请求且仲裁器处于轮询模式下，每个master（0~3）在不超过16个周期内获得grant”在BMC k=16时发现反例——原因是轮询计数器在复位后初始值为0，导致master0连续两次获权。这是设计真实bug，通过修复计数器复位值解决。
- EC阶段：在综合后网表上运行等价性检查，重点对比扫描链插入后的功能路径。首次运行发现4个Non-Equivalent点，定位到下游工具在扫描链重定时时改变了寄存器边界；修正CLP（Change of Layout Protocol）设置后重新验证，全部等价。
3.6 常见误区：工程中容易踩的坑
| 误区 | 后果 | 正确做法 |
|---|---|---|
| EC只关注RTL vs 网表，忽略ECO后验证 | ECO插入的观察点/测试点可能破坏功能等价性 | ECO后必须重新运行EC，对比ECO前后网表 |
| MC属性过强或过弱 | 过强导致虚假反例（人力浪费）；过弱导致关键缺陷漏报 | 属性由设计规范逐条导出，由验证和设计团队共同评审 |
| 把EC当成“全设计比对” | RAM、模拟宏、时钟域交叉逻辑无法自动匹配，产生大量不相关差异 | 通过黑盒、cutpoint、cx（Constant）进行适当抽象 |
| MC直接对全芯片运行 | 状态空间爆炸，工具长时间不收敛 | 以模块/子系统为单位做MC，全芯片靠等价性检查+仿真 |
| 忽视CLP设置和扫描链映射 | 扫描链相关差异被误报为功能不等价 | 预先声明scan_enable、scan_in/scan_out等扫描端口 |
3.7 本章实践清单
- 能画出EC与MC在SoC验证流程中的角色分工图
- 理解逻辑锥（Logic Cone）与比较点（Comparison Point）的定义
- 掌握BDD、BMC、IC3/PDR的基本算法内核
- 能解读EC报告中的Equivalent / Non-Equivalent / Aborted状态
- 能区分安全属性（Safety）与活性属性（Liveness）
- 能完成一个模块级MC属性集的编写与反例分析
- 了解ECO后EC验证的必要场景和典型步骤
- 在项目中规避表格3.6中列出的五大误区
重要提示：形式化验证不是“验证银弹”，而是需要与动态仿真协同的工程手段。等价性检查保证的是“实现没有偏离参考”，模型检查保证的是“参考设计满足关键属性”。两者结合，才能为SoC签核提供完整的数学级保证。