📚 课程目录第2章命题逻辑与时序逻辑

AI芯片与SoC形式化验证方法 - 第2节

2.1 本章学习任务

在AI芯片与SoC的形式化验证中，命题逻辑与时序逻辑是两大底层推理基石。本章围绕“如何用逻辑语言描述电路行为，并据此选择验证策略”这一任务主线，依次回答以下问题：

命题逻辑如何建模组合电路，并支撑等价性检查？
时序逻辑如何描述状态机与时序属性，并驱动模型检测？
两类逻辑在工程中如何衔接，解决AI芯片中的实际验证问题？

2.2 核心概念

命题逻辑（Propositional Logic）处理真/假值的布尔运算，对应变量为 0/1、true/false。组合逻辑电路的门级网表、布尔表达式、约束条件，本质上都是命题逻辑公式。

时序逻辑（Temporal Logic）在命题逻辑基础上引入时间算子，用于描述系统状态随周期或事件的演化关系。SoC 验证中常用两种时序逻辑：

LTL（Linear Temporal Logic）：沿单条执行路径描述事件，如 FG (req -> ack)；
CTL（Computation Tree Logic）：基于分支时间描述状态空间中的必然与可能路径，如 AG EF ready。

命题逻辑是逻辑代数的基础，时序逻辑是状态与时段推理的扩展，二者共同构成形式化验证的输入语言与语义框架。

  关键提示：在AI芯片验证中，卷积运算单元、矩阵乘累加阵列的等价性依赖命题逻辑求解；而缓存一致性、中断优先级仲裁、DMA状态机等行为依赖时序逻辑属性验证。

2.3 原理机制

2.3.1 命题逻辑与SAT求解

验证一条组合路径是否恒等，可构造 miter 电路：将两个逻辑网络输出异或，再以SAT（可满足性）引擎搜索是否存在令该异或结果为1的输入组合。若不可满足（UNSAT），则证明两个网络功能等价。

AI芯片中的典型场景：

卷积单元重构前后的位宽适配和乘加重排验证；
门控时钟的逻辑替换与低功耗优化验证；
网表与RTL的等价性检查（EC）。

2.3.2 时序逻辑与模型检测

模型检测在有限状态机的状态空间上解释时序逻辑公式。AI芯片中的DMA控制器、中断控制器、片上网络路由状态机，通常建模为一个时钟周期迁移一次的Kripke结构。验证工具通过BMC（Bounded Model Checking）、k-induction、属性覆盖度分析等技术，在多个周期窗口内判定属性是否成立。

LTL属性示例：

assert property (
  @(posedge clk) disable iff (rst_n == 0)
  (req ##[1:5] ack)
);

CTL属性示例：

AG (state != DEADLOCK)
AF (curr_state == IDLE)

2.4 验证流程步骤

属性提取：从AI芯片设计规格中提取功能属性、时序约束、安全不变式；
建模：将设计转换为命题逻辑公式或有限状态机模型；
引擎选择：组合逻辑优先使用SAT/等价性检查引擎，状态相关属性使用模型检测/BMC引擎；
约束注入：配置时钟周期、复位矢量、输入约束、环境假设；
求解与反例分析：分析SAT/UNSAT结果或反例波形，确认是设计缺陷还是约束过强；
收效评估：综合覆盖率、证明轮数、反例数量，判定验证充分性。

2.5 案例说明

  案例A：某AI推理芯片的矩阵乘法单元在低功耗改造后，通过等价性检查验证其布尔逻辑与原乘法器一致。采用SAT引擎在约2小时内完成 32x32 乘法器重构前后的功能等价证明，未发现反例。

案例B：缓存一致性协议的有限状态机中定义如下属性：任何读请求最终都能获得数据或错误响应。使用LTL公式 FG (read_req -> F data_valid) 进行BMC验证，在第4周期展开时发现一条被忽略的仲裁路径，反例驱动设计方补充了优先级修复。

2.6 表格总结：命题逻辑 vs 时序逻辑

对比维度	命题逻辑	时序逻辑
建模对象	组合逻辑网络、布尔约束	状态机、事件时序行为
时间概念	无时间，纯组合函数	含周期、顺序、最终性
核心引擎	SAT、BDD、等价性检查	BMC、LTL/CTL模型检测
典型应用	RTL vs 网表、校位调整、逻辑优化	中断仲裁、DMA状态机、缓存一致性
输出结果	等价/不等价、反例输入	属性成立/不成立、时序反例波形

2.7 误区提醒

误区1：命题逻辑等价并不能保证时序行为一致。组合逻辑相同、状态编码不同，仍然可能产生功能不匹配。
误区2：时序属性验证中遗漏“公平性约束”，容易把理论反例当成真实缺陷。
误区3：将未约束的输入直接参与SAT求解，导致大规模不可满足，误判为功能错误。
误区4：忽略异步接口的时序假设，导致模型检测与实际硬件行为不一致。

2.8 实践清单

合理划分组合等价性和时序属性验证的边界；
为状态机属性定义明确的时钟、复位和输入约束；
对SAT不可满足结果保留求解证据，便于回归分析；
在高风险逻辑上叠加BMC多周期检查，提升验证深度；
每个AI加速器模块至少建立一条核心链路属性，防止功能回归。