4.1.3 实时逻辑（RTL）：时钟约束（x ≤ 5, y − x > 2）与混合系统验证

文档摘要

4.1.3 实时逻辑（RTL）：时钟约束（x ≤ 5, y − x > 2）与混合系统验证实时系统不是在“时间里运行”的系统，而是在“时间上被定义”的系统。这句话听起来拗口，但恰恰点破了实时逻辑（Real-Time Logic, RTL）的本质：它不关心事件是否“快”，而关心事件是否“准”——准到毫秒级的时序承诺，准到约束条件在每一个可能的执行路径上都不可违背。当我们在形式化方法中写下 $x \leq 5$ 或 $y - x > 2$ 这样的时钟约束时，我们不是在描述一个变量的取值范围，而是在刻写系统的时间契约——就像芯片手册里那几行加粗的时序参数，稍有越界，整个功能链就可能坍缩为未定义行为。本节聚焦于 4.1.