4. 命题逻辑与布尔可满足性：核心概念、原理机制、实战要点

形式化验证的核心引擎之一是布尔可满足性（SAT）。在 RTL 代码验证中，我们经常把“设计是否满足属性”转换为一个布尔逻辑公式，然后交给 SAT/SMT 求解器判定。理解命题逻辑与 SAT 的基本原理，是掌握形式化验证流程的关键前提。

4.1 问题背景：为什么验证需要 SAT？

仿真验证在覆盖空间上存在局限性，难以遍历所有输入组合。形式化验证则把设计行为和待验证属性编码为布尔公式，通过求解器自动判断：

  • 是否存在一组输入/状态，使设计行为违反断言？
  • 所有可达状态是否都满足不变式？
  • 两个 RTL 实现（如综合前后）对于所有输入是否等价？

这些问题归根结底都是：给定一个布尔公式 F，是否存在一个变量赋值使 F = TRUE？ 这就是 SAT 问题。

4.2 核心概念

概念 定义/说明 验证中的角色
命题 可判定真假的陈述，如“信号 a 为高” 表示设计中的信号/状态条件
逻辑连接词 与（∧）、或（∨）、非（¬）、蕴含（→）、等价（↔） 组合信号条件，描述属性
布尔公式 由变量、常量（0/1）和连接词构成 将设计约束和属性编码为公式
CNF 合取范式：多个子句的与，每个子句是文字的或 SAT 求解器的标准输入格式
文字（literal） 变量 x 或其否定 ¬x 子句的最小构成单元
赋值 给每个变量指定 0 或 1 对应一组 RTL 输入/状态序列
可满足（SAT） 存在一组赋值使公式为真 找到反例或证明可满足
不可满足（UNSAT） 所有赋值都不能使公式为真 证明属性成立或设计等价

4.3 原理机制：从 RTL 到 SAT

RTL 验证中，SAT 求解器并不直接处理硬件描述语言。我们需要将设计逻辑和断言转换为布尔约束系统，通常经过以下步骤：

  1. 信号编码：将 RTL 中的比特向量、状态寄存器映射为布尔变量。
  2. 逻辑展开：对组合逻辑门（与、或、非、多路选择器等）建立布尔表达式。
  3. 时间边界：在有界模型检验（BMC）中，将时序逻辑展开 k 个时钟周期，形成比特级电路模型。
  4. 属性编码：将断言逻辑（如 PSL/SVA 属性）转换为监视器电路，并与设计逻辑共同构造。
  5. 求反与求解：要证明“属性 P 始终成立”，等价于检查“是否存在反例使 ¬P 为真”。若求解器返回 UNSAT，则属性成立；若 SAT，则给出反例轨迹。
核心等式
验证任务：设计约束 ∧ ¬属性
若求解结果为 UNSAT → 属性成立。
若求解结果为 SAT → 得到一组变量赋值，即反例。
CNF 示例
公式 (a ∨ ¬b) ∧ (¬a ∨ c) ∧ (b ∨ c) 是可满足的，例如赋值 a=1, b=0, c=1 可使公式为真。
公式 (a) ∧ (¬a) 是不可满足的，因为它要求 a 同时为真和假。

现代 SAT 求解器基于 DPLL/CDCL 算法框架：

  • 决策：选择一个未赋值变量，尝试赋值为 0 或 1。
  • 传播：根据子句约束，推导必然赋值，如单元传播。
  • 冲突分析：当发生矛盾时，学习冲突子句，避免重复搜索。
  • 回溯：返回最近的决策点，翻转赋值。
  • 重启：重置决策栈，保留学习子句，提高搜索效率。
RTL 设计 逻辑编码 布尔公式(CNF) SAT 求解器 SAT=可满足 UNSAT=不可满足 输出反例 证明属性成立

4.4 流程步骤

在实际 RTL 形式化验证工具（如 Synopsys VC Formal、Cadence JasperGold、开源工具 Yosys-SMTBMC）中，SAT 求解过程通常被封装为以下标准流程：

  1. 读入设计：解析 RTL、约束文件（SDC）和断言（SVA/PSL）。
  2. 建立模型：将设计映射为门级电路，标注组合/时序逻辑。
  3. 设置求解边界：如 BMC 的 k 周期，或等价性检查的逻辑锥。
  4. 生成 CNF：通过 Tseitin 变换将布尔电路转换为 CNF 公式。
  5. 调用求解器：执行 SAT 求解，可配置决策启发式、随机种子、内存限制等。
  6. 解析结果：
    • 返回 UNSAT：属性在给定边界内成立（或设计等价）。
    • 返回 SAT：提取赋值，生成 VCD/FSDB 等反例波形。
    • 返回 UNKNOWN：超时或资源耗尽，需调整边界/抽象策略。

4.5 案例说明

案例：寄存器写使能断言

假设 RTL 中存在一个写使能信号 wr_en，我们希望验证：

property p_wr_en;
  @(posedge clk)
  !(wr_en && rst_n == 0);
endproperty

其含义是：在时钟上升沿，如果复位有效（rst_n=0），则写使能不能为高。

将该属性转换为布尔约束：

约束 = (rst_n == 0) && (wr_en == 1)
目标 = 约束 为真（即找到反例）

求解器对状态空间搜索后返回 UNSAT，说明在所有可达状态下不存在“复位时写使能拉高”的情况，属性验证通过。

如果设计存在 bug，例如在复位状态写使能由组合逻辑错误拉高，求解器会返回 SAT，并给出一个时钟周期的赋值序列，帮助定位问题。

4.6 表格总结：SAT 结果与验证含义

SAT 结果 验证含义 后续动作
UNSAT 属性在边界内成立，或设计等价 收敛，可扩大边界或完成验证
SAT 存在反例，属性失败 分析波形，修复 RTL 或约束
UNKNOWN / 超时 求解资源不足，无法判定 增加抽象、减小边界、使用 SMT 或混合策略

4.7 误区提醒

  • 混淆 SAT 与 SMT：SAT 处理纯布尔变量；SMT 可处理整数、数组、未解释函数等高层抽象。RTL 验证遇到算术运算时，SMT 往往更高效。
  • 忽视 CNF 转换开销：大型电路转换为 CNF 可能产生数十万子句，编码质量直接影响求解效率。
  • 误将 UNSAT 当作全局正确：有界模型检验中的 UNSAT 仅说明在 k 周期内成立，不等于任意深度的性质成立。
  • 忽略约束合法性：约束过强可能导致设计被迫满足属性；约束过弱则可能导致大量无关反例，浪费调试时间。
  • 盲目增加求解时间：不是所有问题都是越大越好的搜索，合理的化简、抽象和调度策略比单纯加长超时更有意义。

4.8 实战清单

  • 确认验证目标是证明还是找反例，选择对应的公式编码方式。
  • 将时序属性转换为可综合的 assert 或 property，避免未知态（X）传播。
  • 使用 Tseitin 变换时，关注中间变量的数量，避免不必要的子句膨胀。
  • 对大规模设计，先执行 low-resource 快速预检，再决定是否进行深度搜索。
  • 学会阅读求解器统计信息：决策数、冲突数、传播数，判断搜索瓶颈。
  • 利用 增量求解 机制，在多个相似性质之间共享 learned clauses，可显著提高效率。
  • 维护标准断言库，将常用属性（复位、握手、FIFO 满空等）模板化，减少重复编码。
  • 在回归环境中设置合理的超时阈值，推荐使用 多引擎并行（如 SAT + SMT + 仿真）提高总体验证收敛速度。
← 上一章 📖 返回目录 下一章 →