IP模块形式化验证流程与案例分析 - 第4节

4.1 本章学习任务：IP 模块验证需求分析

形式化验证不是凭空写断言，而是从“需求”出发，把自然语言规格转变成可验证的数学属性。本章围绕三条主线展开：规格提取、断言映射、验证计划制定。掌握这三步，就能为任意 IP 模块搭建起形式化验证的骨架。

4.2 问题背景：为什么验证需求分析决定形式化效果

实际项目中，形式化验证失败的常见原因并非工具能力不足，而是需求侧出了问题：规格含糊、断言遗漏、验证目标不明确。形式化验证的“穷举”特征决定了它必须首先回答三个问题：

• 证明什么？——属性的精确定义；
• 在什么边界内证明？——输入范围、状态空间约束；
• 证明到什么程度算完成？——覆盖率和属性完备性。

这三个问题全部来自验证需求分析。若跳过该阶段，断言很容易退化为“实现代码的转写”，失去验证意义。

4.3 核心概念：三大关键对象

三者关系：规格提取产生高质量规格；断言映射让规格可执行；验证计划确保验证闭环。下图给出整体流程框架。

4.4 原理机制：三层规格模型

规格提取的质量直接决定断言映射的难度。建议采用三层规格模型逐层收敛：

1. 行为规格（Behavioral Spec）：描述“做什么”，如读操作返回数据、请求必须响应；
2. 时序规格（Temporal Spec）：描述“什么时候做”，如读请求与读数据之间的周期关系；
3. 接口规格（Interface Spec）：描述“怎么交互”，如握手协议、总线仲裁规则、跨时钟域约束。

三层规格分别对应不同的断言类型：行为规格映射为组合断言和功能断言；时序规格映射为蕴含断言和序列断言；接口规格映射为协议断言和同步/异步约束。

4.5 流程步骤：从规格到验证计划

标准流程分为六个步骤，每一步都有明确产出物和检查点。

4.6 案例说明：一个简单的 AXI-Lite 从机模块

以 AXI-Lite 从机接口验证需求分析为例，快速展示三个过程的产物。

4.6.1 规格提取（局部）

原始文档描述：
- 当收到 AWVALID 为高时，从机必须保证 AWREADY 在下一个时钟上升沿之前拉高。
- 写数据 WVALID/WREADY 握手必须在 AWVALID/AWREADY 握手完成后发生。
- 写响应 BVALID 必须在 WVALID/WREADY 握手完成后产生。

4.6.2 断言映射（局部）

// AXI-1：AWREADY 不晚于 AWVALID 后 1 拍拉高
property p_awready_no_later_than_1;
  @(posedge clk)
  $rose(AWVALID) |-> ##[0:1] AWREADY;
endproperty
assert property (p_awready_no_later_than_1);

// AXI-2：写数据通道不能先于地址通道握手
property p_wvalid_after_aw_handshake;
  @(posedge clk)
  $rose(WVALID) |-> !AWVALID || $past(AWREADY);
endproperty
assert property (p_wvalid_after_aw_handshake);

// AXI-3：写响应在写数据握手后 1~8 拍内拉高
property p_bvalid_after_w_handshake;
  int delay;
  @(posedge clk)
  (WVALID && WREADY) |-> ##[1:8] BVALID;
endproperty
assert property (p_bvalid_after_w_handshake);

4.6.3 验证计划制定（局部）

4.7 表格总结：三种能力对比

4.8 误区提醒

• 误区 1：规格提取等于“读文档”。
  实际需要写出来、评出来、形成版本化产物，否则断言无法追溯。
• 误区 2：断言映射越“严”越好。
  过度约束会掩盖真实错误，导致形式化证明通过但不保证功能正确。
• 误区 3：验证计划只关注“断言数量”。
  更重要的是覆盖点的结构分布：不同的输入组合、关键内部状态、连续事务间隔等。
• 误区 4：把仿真中用的断言直接拿来做形式化。
  形式化需要更精确的输入约束和更严谨的时序窗口，否则会出现反例或证明不终止。
• 误区 5：忽略规格变更后的回归。
  版本更新后，要重新检查规格优先级、断言映射和计划覆盖，而不是只重跑工具。

4.9 实践清单：开始 IP 验证需求分析

1. 建立规格追踪矩阵，每条规格有唯一 ID，关联原始文档段落。
2. 为每个功能点标注验证方式：形式化证明 / 仿真 / 二者组合。
3. 列出 P0 属性清单，确认均位于可证明范围（无复杂浮点运算、无未知内部状态）。
4. 编写断言命名规范：p_模块_功能_性质，例如 p_axi_awready_handshake。
5. 明确输入约束：时钟建模、复位建模、输入随机性范围。
6. 定义覆盖点：至少包括关键使能信号翻转、握手完成、FIFO 满/空、异常响应。
7. 设定证明超时阈值：例如单属性 30 分钟内未收敛则拆分或给假设。
8. 安排评审节点：规格评审、断言评审、验证计划评审，分别由设计、验证、架构三方参与。