4. 断言与属性规格

4.1 问题背景：为什么断言是一切验证的前提

SoC 验证中，设计规模增长使得纯动态仿真很难覆盖到所有状态组合。形式化验证通过数学推理穷举状态空间，回答“某个属性是否恒成立”。因此，属性规格与断言成为验证意图的唯一表达入口。属性建模不准确，形式化结果再漂亮也无法证明设计正确；属性可解性差，证明过程可能长期不收敛。

4.2 核心概念：属性、序列、断言、假设

在形式化验证语境中，以下术语必须严格区分：

• 属性（Property）：描述设计在时间轴上应满足的行为规格，例如“写有效后下一拍 full 不应为真”。
• 序列（Sequence）：构成属性的事件链，表示信号在连续多个时钟周期内的布尔表达式演化。
• 断言（Assertion）：将属性绑定到设计上进行验证，要求属性必须成立；工具会尝试证明或寻找反例。
• 假设（Assume）：对设计输入环境的约束，不是待证明项，而是用于缩小状态空间、排除非法输入。

同时，必须区分两种断言类型：

• 立即断言：在过程块中按执行顺序求值，不依赖时钟边沿，常用于仿真局部检查。
• 并发断言：基于时钟沿采样，具有完整时序语义，是可被形式化工具证明的核心形态。

下图给出断言与属性规格在形式化验证中的完整闭环：

4.3 原理机制：属性如何被证明

属性求值绑定到时钟事件，工具在每个时钟边沿采样信号状态，并依据属性语义遍历状态空间。

以“写有效后下一拍 full 不为真”为例，证明引擎会寻找反例：是否存在一条路径，使得当前周期 fifo_wr && !full 成立，且在下一个时钟沿 full == 1。若在可达状态空间中不存在这样的路径，则报告 pass；若存在，则生成反例波形。

形式化工具主要依赖模型检验与 SAT/SMT 求解，对属性进行穷举推理。结果不是“多轮仿真的统计可靠性”，而是“数学上的确定结论”。

属性求值结果有三种：

• pass：证明成功，属性在所有可达状态中成立。
• fail：找到反例，说明设计存在违反，或属性约束不合理。
• vacuous pass（空成功）：属性前提从未为真，虽然证明通过但没有验证效果。

4.4 流程步骤：断言开发五步法

1. 规格提取：从协议手册、架构文档中提取关键时序关系、不变量与错误场景。
2. 属性编写：使用 SVA/PSL 编写序列与属性，并绑定时钟和复位。
3. 约束建模：通过 assume 约束输入合法值，排除不可达、非法输入。
4. 证明运行：启动形式化验证工具，逐步增加属性复杂度，观察收敛情况。
5. 结果治理：分析 fail/vacuous，修复属性或设计，并将反例转化为仿真回归用例。

4.5 案例说明：FIFO full 信号的时序属性

以 SoC 中常见同步 FIFO 为例，设计接口示意如下：

module fifo (
  input         clk, rst_n,
  input         fifo_wr, fifo_rd,
  input  [7:0]  fifo_wdata,
  output        full, empty
);

目标属性：当写有效且 FIFO 未满时，下一拍 full 不成立。对应的 SVA 断言如下：

property p_wr_not_full_next_cycle;
  @(posedge clk)
  disable iff (rst_n == 0)
  (fifo_wr && !full) |=> !full;
endproperty

a_wr_not_full: assert property (p_wr_not_full_next_cycle)
  else $error("FIFO 在写入有效后下一拍仍为 full");

|=> 表示“下一拍”，右侧 !full 在下一时钟沿被检查。若设计中前件条件成立，但下一拍 full 为 1，则断言失败，工具可给出从写操作到 full 置位的完整反例路径。

为防空成功，补充覆盖属性：

cover property (@(posedge clk) fifo_wr && !full)
  $info("FIFO 可写状态被覆盖");

如果该覆盖属性报告 0 次命中，说明前件从未激活，需要检查环境约束或设计状态空间是否过窄。

4.6 表格总结：断言与属性规格速查

属性构件	语法片段	作用	容易出现的错误
时钟事件	@(posedge clk)	声明采样时钟沿	忘记声明时钟，导致工具无法判定。
序列连接	a ##[1:3] b	a 发生后 1~3 拍内 b 发生	误用 ##0 或 ##1，窗口边界错误。
蕴含操作符	a |-> b	a 发生的同一拍，b 必须成立	前置条件不充分，导致伪反例。
带周期蕴含	a |=> b	a 发生的下一拍 b 成立	与 |-> 混用，相位偏移一拍。
复位控制	disable iff (rst_n == 0)	复位期间不检查属性	忽略复位，产生大量虚假失败。
禁止属性	never a	a 在所有时刻都不允许成立	未约束非法状态时，误报严重。

4.7 误区提醒

4.8 实践清单