第2章 形式化验证流程与工具链：核心概念、原理机制、实战要点

1. 问题背景

在 AXI/AHB/APB 总线互连验证中，动态仿真能够在有限激励下发现大量功能错误，但难以回答一个关键问题：协议属性是否在全部可达状态与全部合法输入序列下成立？

• 仿真覆盖率只能量化“已执行的路径”，无法证明“未执行路径”无违例；
• 多主机并发访问、乱序响应、写数据交织等场景，仿真激励很难在有限时间内覆盖完整组合；
• 总线协议本质上是精度到时钟周期的时序命题，适合用数学方法穷举证明。

形式化验证的核心价值：将总线协议规则转化为数学属性，通过穷举状态搜索证明“不存在反例”，从而在仿真之外提供更强的协议合规保证。

2. 核心概念

• 属性（Property）：用形式化语言描述的总线协议规则，例如“当 AWVALID=1 且 AWREADY=1 时，握手在下一拍必须完成”。
• 断言（Assertion）：以 assert property 声明的属性，是验证环境的可执行化表达。
• 约束（Constraint）：限制输入端口行为的环境假设，例如“复位后前 4 拍不允许发送请求”。
• 模型检查（Model Checking）：穷尽可达状态空间的验证算法，回答“该属性在所有状态下是否成立”。
• 反例（Counterexample, CEX）：导致属性失败的时钟精确波形序列，是调试的主要入口。
• 等价性检查（Equivalence Checking）：对比 RTL 与参考模型或网表，证明两者逻辑等价，常用于实现级验证。

3. 原理机制

形式化验证工具将 RTL 设计转换为有限状态机模型，属性转换为时序逻辑公式，然后通过求解器对状态空间进行数学遍历。

• 状态空间由寄存器与输入自由变量共同构成；AXI 通道多、数据位宽大，因此常用抽象缩小状态范围；
• SMT/SAT 求解器支持算术、数组、位向量等理论，适合分析 AXI 的突发长度、字节使能与地址对齐；
• 引擎对可达状态集合进行不动点迭代，直到属性被证明或发现反例；
• 最终结果通常分为四类：proven、fail、bounded、inconclusive。

4. 流程步骤

1. 设计准备：导入 RTL，解析 AXI/AHB/APB 模块，指定顶层和关键信号。
2. 时钟与复位定义：声明主时钟约束，定义复位释放条件和复位后稳定拍数。
3. 属性编码：将协议规则转换为 SVA 或 PSL 属性。
4. 环境建模：为目标接口建立约束，模拟总线主/从行为。
5. 证明运行：选择求解引擎、设置时间边界和证明复杂度上限。
6. 结果分析：对 fail/bounded 结果生成反例并定位违例根因。
7. 收敛签核：补充约束、修正属性，完成所有关键属性证明。

5. 案例说明

以下是一个简化的 AXI 写地址通道握手属性示例：

property p_aw_handshake;
    @(posedge ACLK)
    disable iff (!ARESETn)
    (AWVALID && AWREADY) |=> !AWVALID;
endproperty

assert property (p_aw_handshake);

该属性验证：当 AWVALID 与 AWREADY 同时为高时，下一拍握手完成，AWVALID 必须拉低。

6. 表格总结

工具/引擎	验证维度	主要特点	典型场景
Cadence JasperGold	属性验证、等价性、并发验证	支持 SVA/PSL、多引擎调度、抽象能力	复杂的 AXI 互联仲裁与乱序通道
Synopsys VC Formal	属性验证、等价性、低功耗验证	与仿真回归集成度高，支持大设计	AXI/AHB 桥接 IP 的属性证明
Siemens Questa Formal	属性验证、覆盖率分析	波形集成强，调试验证效率高	单模块 APB slave 属性检查
Yosys + SymbiYosys	开源形式化验证	支持 SMT-BMC、ABC、可脚本化	教学实验、小规模 APB/AHB 模块

7. 误区提醒

8. 实践清单