第1章 形式化验证概述：核心概念、原理机制、实战要点

在芯片前端设计流程中，仿真（Simulation）长期是 RTL 功能正确性的主要验证手段。然而随着 SoC 规模扩大、接口协议复杂化以及安全等级提升，仿真覆盖率“看似达标、实则漏检”的风险日益突出。形式化验证（Formal Verification）以数学证明替代“激励+比较”，成为补全功能验证闭环的关键一环。

形式化验证 属性规约 数学建模 穷尽证明 工具引擎 收敛策略 图1-1 形式化验证知识框架

1.1 问题背景：验证从哪里打开“缺口”

传统仿真验证的基本方式是“给激励、看结果”。这种方式的弱点在于：激励集合永远只是输入空间的一个子集。流程一端的覆盖率目标又往往停留在“代码行覆盖”或“翻转覆盖”，很难回答“设计行为是否都被验证到”。下列场景尤其容易漏检：

  • 随机激励难以命中长路径的深度时序交互错误；
  • 高维组合条件导致的隐含状态无法被定向激励覆盖；
  • FIFO 溢出、跨时钟域同步、协议乱序返回等边界行为需要穷尽检查；
  • 复用 IP 的接口约束在集成后发生继承性丢失。

形式化验证不依赖测试向量，而是把“设计是否满足某种预期行为”转化为数学命题，对整个空间进行判定。

1.2 核心概念

形式化验证体系中有五个经常遇到的关键术语，也是本课程后续展开的主线：

  • 属性（Property）：设计预期行为的精确描述，通常用 SVA/PSL 时序断言表达。
  • 模型（Model）：RTL 编译后的数学结构，常建模为有限状态机（FSM）或字级转换系统。
  • 穷尽证明（Exhaustive Proof）：对可达状态空间或全部合法输入序列进行分析，不遗漏任何反例。
  • 证明引擎（Engine）：基于 BDD、SAT/SMT 或符号仿真等技术自动判定“模型 |= 属性”。
  • 收敛（Convergence）：证明过程在可接受的时间与内存预算内完成，给出“证明通过”或“反例波形”。

概念速记

属性写清楚 → 模型建正确 → 引擎做穷尽 → 结果判收敛。五个节点串起来就是一条完整的形式化验证知识链。

1.3 原理机制

形式化验证的本质是“用一个数学定理替换一万条测试用例”。其核心推理过程可以概括为三步：

  1. 语义建模：将 RTL 映射到带有迁移关系的数学模型上，状态变量构成有限状态空间。
  2. 属性编译：将断言描述编译成时序逻辑公式，指定在哪些窗口、哪些条件成立时行为必须为真。
  3. 求解判定：由引擎在状态空间中搜索违反属性的路径。若所有路径都被排除，属性成立；若找到一条反例路径，则输出该时序波形。

与传统仿真相比，其根本差异在于“完备性来源不同”：仿真是对有限激励集合的抽样检查，形式化是对状态空间的数学归类与剪枝搜索。

1.4 流程步骤

在工程中落地形式化验证，一般遵循以下六个步骤：

  1. 提取需求属性：从规格说明书中提炼关键行为，写成 SVA/PSL 断言。
  2. 建立环境约束：声明输入有效条件、异步接口忽略范围，防止无关状态触发爆炸。
  3. 选择验证引擎：按设计规模选择模型检验、等价性检查或协议证明专用引擎。
  4. 执行证明：运行工具，让求解器在可达状态空间内证明属性或产生反例。
  5. 分析反例并迭代：将反例波形对应回 RTL，定位根因，修改设计或修正属性后重新证明。
  6. 回归与交付：属性集、约束文件和证明脚本纳入版本管理，供后续 ECO/集成复用。

1.5 案例说明：AXI 乱序返回中的握手丢失

案例提示

某互连模块实现 AXI 读通道乱序返回。随机仿真运行十万轮未出现异常，但形式化团队从协议中提取了一条关键规则：已发出请求的读 ID，在 Data 通道返回时，RVALID 必须保持到 RREADY 有效为止。SVA 断言如下：

property axi_rvalid_hold_until_rready;
  @(posedge aclk) disable iff (!areset_n)
    (rvalid && rready) |-> ##[0:$] rvalid;
endproperty
assert property (axi_rvalid_hold_until_rready);

运行模型检验引擎后，工具在约 47 分钟内生成一条反例：当读 ID=0x3 的返回事务处于 RLAST 窗口时，RVALID 在下一个时钟周期被拉低。设计者在读数据 FIFO 状态机中增加了 ID 匹配保持条件，修复后该断言在全空间证明通过。

这个案例体现了形式化验证的两个实战价值：一是能到达随机仿真覆盖不到的深度时序交点，二是反例波形可直接辅助 R

← 上一章 📖 返回目录 下一章 →