第四章：时序逻辑基础——LTL、CTL、CTL*

好，咱们进入形式化验证的核心地带了。

前面聊了组合逻辑和时序电路的基础，现在要聊的，是「怎么用数学语言描述电路的行为」。说白了，就是给芯片写「行为说明书」，而且这个说明书要精确到每个时钟周期、每个状态。

我个人习惯把时序逻辑形式化验证分成三个层次：线性时序逻辑（LTL）、计算树逻辑（CTL）、以及它们的合体CTL*。嗯，咱们一个一个来。

4.1 线性时序逻辑（LTL）

LTL 的核心思想很简单：把时间看成一条直线。从当前时刻开始，往后无限延伸，每个时刻对应一个状态。你想想看，就像看电影，一帧一帧往后放，不能倒带，不能分支。

LTL 的算子不多，但很实用：

• G p（Globally）：从当前时刻开始，所有时刻 p 都成立。
• F p（Finally）：从当前时刻开始，未来某个时刻 p 会成立。
• X p（Next）：下一个时刻 p 成立。
• p U q（Until）：p 一直成立，直到 q 成立的那一刻。

举个例子。你要验证一个复位信号：

// LTL 描述：复位后，输出必须一直保持为0，直到复位撤销
G (reset == 1 -> X (G (output == 0)))

我在项目中遇到过一个问题。有个同事写 LTL 属性时，忘了考虑「复位撤销后第一个时钟沿」的情况。结果仿真通过，但形式化验证报错。为什么？因为 LTL 的「下一个时刻」是严格意义上的下一个时钟沿，不是「过一会儿」。嗯，这里要注意。

4.2 计算树逻辑（CTL）

CTL 和 LTL 最大的区别是：CTL 考虑所有可能的未来路径。说白了，LTL 是一条线，CTL 是一棵树。每个分支代表一个可能的执行路径。

CTL 的算子分两类：路径量词和时序算子。

• A（All）：所有路径。
• E（Exists）：存在某条路径。
• G、F、X、U：和 LTL 一样，但必须和路径量词配对使用。

比如：

// CTL 描述：从任何状态开始，都存在一条路径，最终能到达复位状态
AG (EF (reset == 1))

这个属性在验证「死锁」时特别有用。我曾经用 CTL 验证过一个总线仲裁器，发现某个优先级组合下，低优先级请求永远得不到响应。CTL 的 AG EF 一下子就揪出来了。

4.3 CTL*

CTL* 是 LTL 和 CTL 的合体。它允许你在路径量词内部使用任意的 LTL 公式。说白了，CTL* 更灵活，表达能力更强。

举个例子：

// CTL* 描述：存在一条路径，在这条路径上，p 最终会一直成立
E (F G p)

这个属性在 CTL 里写不出来，在 LTL 里也写不出来。CTL* 把它们揉在一起了。

但说实话，CTL* 的模型检查算法复杂度高，工具支持也不如 LTL 和 CTL 成熟。我个人的建议是：能用 LTL 就用 LTL，能用 CTL 就用 CTL，实在不行再上 CTL*。

逻辑类型	表达能力	复杂度	适用场景
LTL	线性时间	低	协议验证、流水线控制
CTL	分支时间	中	状态机验证、死锁检测
CTL*	两者结合	高	复杂时序属性

4.4 实际应用中的选择

你可能会问：到底用哪个？

我的经验是：

• 验证控制逻辑（比如状态机、仲裁器）：用 CTL。因为你要检查「所有状态」或「存在某个状态」。
• 验证数据通路（比如 FIFO、流水线）：用 LTL。因为你要检查「每个时钟沿的行为」。
• 验证复杂协议（比如 AXI、PCIe）：用 CTL*。因为协议里既有「所有路径」的要求，又有「未来某个时刻」的要求。

我记得有一次验证一个 DDR 控制器，协议要求「写命令发出后，数据必须在 4 个时钟内到达」。用 LTL 写：G (write_cmd -> F (data_valid))。但后来发现，这个属性太弱了，因为「未来某个时刻」可能是 100 个时钟后。最后改成 CTL* 的 AG (write_cmd -> AF (data_valid))，才把问题揪出来。

嗯，今天就聊到这儿。下一章咱们聊聊「模型检查」的具体算法，看看工具是怎么自动验证这些属性的。