跳到主要内容

形式验证：先建模环境，再证明设计

形式验证（Formal Verification）把 RTL、环境约束与属性转成逻辑问题，尝试在可达状态空间中证明规则恒成立，或给出一条反例路径。它和随机仿真互补：仿真适合运行真实软件场景，形式验证适合检查难以覆盖的极端状态、异常组合和控制路径。

本文按一次功能形式验证（FPV）的工作顺序说明关键要点。不同 EDA 工具的命令与报告名称会变化，但建模原则相同。

适合先用形式验证的问题​

  • 握手协议、FIFO、仲裁、状态机和权限控制等控制密集逻辑；
  • reset、enable、异常响应、仲裁优先级等极端条件；
  • 需要证明“不可能发生”的安全属性，例如不会溢出、不会两个 grant 同时有效；
  • 修改 RTL 之后希望确认关键行为没有回退的场景；
  • 仿真难以覆盖的深层组合、死锁或不可达状态。

对大规模数据通路、长软件驱动流程或模拟模型，先进行模块切分、抽象和目标排序通常更有效。

正确的起点：定义验证宇宙​

形式引擎默认会探索所有未受约束的输入组合。若不定义时钟、复位和环境协议，得到的反例可能只是“现实中不会出现的输入”；约束太强又会把真实 bug 排除掉。

因此一开始应回答四个问题：

  1. 哪些时钟存在，彼此有什么关系？
  2. 复位的极性、持续时间与释放顺序是什么？
  3. 哪些输入由外部环境控制，它们必须遵守什么接口约定？
  4. 哪些状态在上电后可达，哪些是刻意未初始化的？

环境约束应描述外部真实能保证的最小事实。例如，AXI master 发送地址后应保持地址与 VALID 直到握手；这可以作为 slave 验证的环境假设。相反，“master 永远不会发送某个困难组合”通常不是合理约束。

一条可重复的 FPV 工作流​

1. 建立最小可运行环境​

先加载最小 DUT、必要的接口 wrapper 和断言文件，定义时钟与复位，再跑一个小深度检查。这个阶段的目标不是覆盖全部功能，而是确认顶层、宏、时钟和 reset 处理规则没有错。

伪代码示意：

# 命令名称以实际工具版本为准
read_design -top traffic -f filelist.f
read_sva ../sva/traffic.sva
create_clock clk -period 10
create_reset rst_n -sense low
set_app_mode FPV
check_properties

脚本中的顶层名、文件列表和路径应来自可复现的构建配置，而不是开发机上的绝对路径。真实项目还需要把宏定义、库文件和 black-box 策略纳入版本管理。

2. 先证明小而硬的属性​

优先检查低耦合、高价值的规则：状态机编码、FIFO 空/满状态切换、grant one-hot、请求应答上界、寄存器复位值。小属性的反例更短，也更容易区分设计 bug、断言错误和环境缺失。

assert property (@(posedge clk) disable iff (!rst_n)
  $onehot0(grant));

assert property (@(posedge clk) disable iff (!rst_n)
  pop && empty |-> !pop_accept);

3. 分析每一条失败​

失败并不等同于 RTL 有 bug。通常有三种可能：

现象常见原因下一步
反例违反真实接口协议环境约束不足补上有依据的 assume，并记录依据
反例符合接口协议但违背预期RTL 设计缺陷修复 RTL，保留断言作为回归保护
规则本身没有表达真实意图属性过强、时序偏移或 reset 处理错误重写属性并增加 cover 验证

应先从反例的第一个分叉点观察输入、状态和时钟域，而不是只盯住最终失败周期。

4. 处理超时与难证明目标​

证明超时不表示属性成立或失败，只表示当前引擎与资源尚未得出结论。常用处理顺序是：

  • 检查是否遗漏了不变量、复位约束或合法输入范围；
  • 将长时序目标拆成局部引理（lemma）；
  • 对无关数据通路做抽象，减少状态空间；
  • 按时钟域、子模块或功能阶段分解；
  • 记录证明深度、timeout 和假设，避免“看似通过”的误判。

任何为求通过而添加的约束，都应能回答“这是系统接口保证的吗？”。

覆盖率的作用​

断言证明回答“某规则是否总成立”，形式覆盖回答“某状态或路径是否可达”。两者缺一不可。

cover property (@(posedge clk) disable iff (!rst_n)
  req ##[1:3] ack ##1 done);

如果 cover 无法命中，可能是目标确实不可达，也可能是约束过强、建模有误或请求前件根本不会发生。对不可达目标应给出设计依据后再排除；不要把未理解的 cover 直接从报告中隐藏。

仿真覆盖与形式覆盖也不应简单相加：前者反映测试执行过的路径，后者反映在约束模型下的可达性。两份结果结合，才能更完整地说明验证完成情况。

让结果可信的几个习惯​

  • 将断言、约束、黑盒假设和证明配置与 RTL 一起评审、一起提交。
  • 把关键 assumption 当作设计接口的一部分写下注释或链接到规格。
  • 修改 reset、时钟、CDC 接口或接口定义时，优先回归相关属性。
  • 为关键规则补 cover，避免只证明了 vacuous truth（前件从未发生）。
  • 给每类超时目标保留分解路径，而不是把 timeout 当作绿色结果。

形式验证的产出不只是“通过”或“失败”，还包括可审计的设计约束：环境允许什么、模块保证什么、哪些状态与条件已经被探索过。