第3章核心语法（一）

第三章：核心语法（一）——原子命题、布尔表达式、时序操作符

好，咱们正式开始接触 RTLA 的语法核心。说实话，很多初学者一上来就被各种操作符吓住了，觉得形式化验证门槛高。其实没那么玄乎，你把它想象成一种「带时间概念的逻辑电路描述」就行了。

我个人习惯把 RTLA 的语法分成三块来学：原子命题是砖块，布尔表达式是水泥，时序操作符是钢筋。今天咱们先把这三样东西讲透。

原子命题是什么？说白了就是一个不能再拆分的真假判断。比如：

每个原子命题的结果只有两种：真（True）或假（False）。嗯，这里要注意：原子命题里不能有时序操作符，也不能有变量赋值，它就是最纯粹的布尔判断。

核心要点：原子命题是 RTLA 公式的叶子节点。你写的所有复杂断言，最终都要分解成原子命题的组合。

我在项目中遇到过一个问题：有个同事把 req == 1 && ack == 1 写成了一个原子命题，结果调试时死活定位不到是哪个信号出了问题。所以我的建议是——原子命题尽量保持单一信号判断，组合逻辑交给布尔表达式去做。

有了原子命题，接下来就是怎么把它们组合起来。RTLA 支持标准的布尔操作符：

你想想看，这些操作符跟 Verilog 里的逻辑门是不是很像？只不过 RTLA 的布尔表达式是在时间线上做判断，而不是在某个时钟周期里算结果。

个人技巧：写布尔表达式时，我习惯把「蕴含」操作符 -> 读作「承诺」。比如 req -> eventually ack 就是「一旦请求来了，我承诺最终会有应答」。这样理解时序逻辑会顺很多。

我曾经踩过一个坑：在复杂断言里用了三层嵌套的蕴含，结果形式化工具跑了三天没出结果。后来拆成两个独立的断言，半天就验证完了。所以记住——布尔表达式不是越复杂越好，可读性和可验证性才是第一位的。

这才是 RTLA 真正的杀手锏。没有时序操作符，你只能描述「此刻」的状态；有了它们，你就能描述「过去」和「未来」的行为。

always 的意思是「在所有时间点上都成立」。它通常用来描述不变式（invariant），也就是系统在任何时刻都必须满足的属性。

// 示例：复位期间，所有输出必须为0
always (reset -> (data_out == 0 && valid == 0))

// 示例：互斥访问，两个master不能同时拿到grant
always !(grant_master0 && grant_master1)

我个人习惯把 always 放在断言的最外层，因为它定义了「全局约束」。你想想看，如果某个属性不是 always 成立的，那它什么时候成立？这就需要其他操作符来配合了。

注意：不要滥用 always。有些属性只在特定状态下成立，比如「当 fifo 满时不能写入」，这个用 always 就不合适，因为 fifo 不一定总是满的。这时候需要结合条件判断。

eventually 表达的是「在未来的某个时刻一定会发生」。它不承诺具体是哪个周期，只承诺「迟早会来」。

// 示例：一旦收到请求，最终必须给出应答
always (req -> eventually ack)

// 示例：复位释放后，最终状态机进入IDLE
always (reset_release -> eventually (state == IDLE))

我记得有个项目，验证工程师写了一条 eventually 断言，结果工具报错说「无法证明」。查了半天，发现是因为设计里有个死循环分支，导致某些请求永远得不到应答。这就是 eventually 的价值——它能帮你发现活锁和死锁问题。

until 稍微复杂一点，它描述的是「某个条件一直保持，直到另一个条件成立」。语法是 A until B，意思是「A 一直为真，直到 B 变为真的那一刻」。

// 示例：请求信号保持为高，直到收到应答
always (req until ack)

// 示例：忙信号保持，直到传输完成
always (busy until transfer_done)

这里有个容易混淆的点：until 不要求 B 最终一定会发生。如果 B 永远不来，那 A 就得永远保持。所以实际项目中，我通常会把 until 和 eventually 搭配使用：

// 更安全的写法：既保证保持，又保证最终释放
always (req until ack) && always (req -> eventually ack)

避坑指南：我曾经在一个 DMA 控制器项目里，用 until 描述「传输过程中数据保持有效」。结果发现设计里有个异常终止场景，数据在传输完成前就失效了。幸亏 until 断言及时捕获了这个违规，否则流片回来就是一颗废片。

为了让你更直观地理解这三者的关系，我画了一张图：

从这张图你能看到，原子命题在最底层，布尔表达式在中间层，时序操作符在最顶层。写断言的时候，也是这个顺序——先想清楚要判断哪些信号（原子命题），再组合成条件（布尔表达式），最后加上时间约束（时序操作符）。

最后分享几个我在实际项目中总结的经验：

先写 always，再写条件：我习惯先把 always 写出来，再往里填具体条件。这样不容易漏掉全局约束。
eventually 要配合超时使用：纯 eventually 可能让工具跑很久，加上时间上限 eventually[0:10] ack 会更实用。
until 注意边界条件：B 成立的那个时刻，A 是否还需要保持？不同工具的解释可能有细微差别，建议查一下文档。
多用括号：RTLA 的操作符优先级跟 C 语言不太一样，我吃过亏。所以现在一律加括号，宁可多写几个，也不让工具猜我的意图。

一句话总结：原子命题是「什么」，布尔表达式是「怎么组合」，时序操作符是「什么时候」。把这三层理清楚，RTLA 的语法你就掌握了七成。