2. 复杂控制逻辑的RTL建模要点

复杂控制逻辑的RTL建模，难点不在语法，而在于把“控制意图”翻译成可综合、可验证、可复用的硬件结构。状态机、流水线控制、仲裁器、握手协议和异常处理逻辑，是五类最常出现也最容易埋下验证隐患的控制结构。本节围绕它们的建模规范与可验证性设计展开，重点说明“怎么写”以及“为什么这样写更容易被形式验证工具收敛”。

一、状态机：把状态语义写清楚

状态机建模的第一条规范是状态编码与状态语义分离。建议用 localparam 或枚举定义状态名，综合工具负责编码，RTL中只出现状态名。第二条规范是三段式或两段式结构统一：组合逻辑算次态，时序逻辑只做状态寄存，输出逻辑单独描述。这样形式验证工具在做状态可达性分析时，能清晰区分“状态转移条件”和“输出函数”，避免把输出毛刺误判为状态错误。

第三条规范是默认转移必须显式。很多设计在 case 中不写 default，综合出锁存器，形式验证会出现大量不可达状态。正确做法是给每个状态一个确定的默认次态，通常回到 IDLE 或 ERROR。第四条是状态可达性约束：在SVA中声明 !$isunknown(state)，并配合 $onehot 或 $stable 断言，让工具快速排除非法编码。

二、流水线控制：让使能与冲刷可证明

流水线控制的核心是valid/ready 沿流水级传播。每一级寄存器都应携带 valid 位，数据位与 valid 位同拍寄存。建模时禁止出现“数据寄存了但 valid 没寄存”或“valid 寄存了但数据被旁路”的不对称写法，否则形式验证无法建立数据与有效性的对应关系。

冲刷（flush）和停顿（stall）是流水线验证的两个重点。建议把冲刷写成优先级最高的同步清零，并在SVA中声明：当 flush 有效时，下一拍所有级 valid 必须为 0。停顿则通过 ready 反压实现，断言“ready 为低时，本级数据与 valid 必须保持稳定”。这两条断言一旦成立，流水线的数据一致性就基本可证。

三、仲裁器：公平性与互斥性

仲裁器建模要同时满足互斥性和公平性。互斥性指同一拍最多只有一个 grant 有效，可用 $onehot0(grant) 断言直接表达。公平性指低优先级请求不会被无限饿死，通常用轮询（round-robin）指针实现。建模时指针更新必须与 grant 同拍，且只在 grant 有效时推进，否则会出现“空转导致公平性丢失”。

对于固定优先级仲裁器，形式验证应重点检查高优先级请求持续有效时低优先级是否永远得不到响应。这不是bug，而是设计意图，因此需要在验证环境中用 assume 约束请求分布，避免工具报出无意义的反例。

四、握手协议：valid/ready 的时序契约

valid/ready 握手有三条不可违反的契约：第一，valid 一旦拉高，在 ready 到来前不得撤销；第二，valid 与 data 必须同拍稳定；第三，ready 可以依赖 valid，但 valid 不得依赖 ready，否则会形成组合环。这三条契约应直接写成SVA断言，作为形式验证的顶层约束。

建模时建议把发送端和接收端分开描述，中间只通过 valid/ready/data 三组信号连接。这样形式验证可以分别对发送端和接收端做局部证明，再通过接口断言完成组合证明，显著降低状态空间。

五、异常处理逻辑：可恢复与不可恢复

异常处理建模要先区分可恢复异常和不可恢复异常。可恢复异常（如握手超时、仲裁冲突）应进入 ERROR 状态并等待软件清除；不可恢复异常（如校验失败、非法状态）应直接锁死并拉高 fatal 标志。两类异常的建模差异在于：可恢复异常需要保留现场寄存器，不可恢复异常只需保证不再产生副作用。

形式验证对异常逻辑的重点是异常触发条件的完备性和异常响应的确定性。建议用 cover 属性证明每个异常都能被触发，用 assert 属性证明异常一旦触发，系统在有限拍内必然进入 ERROR 或 FATAL 状态。

六、可验证性设计的共同原则

把上述五类结构放在一起看，可验证性设计有三条共同原则。第一，接口契约显式化：所有跨模块的握手、仲裁、异常信号都应有明确的SVA断言，而不是靠仿真波形“看着对”。第二，状态空间可收敛：避免组合环、避免锁存器、避免未初始化寄存器，这三者是形式验证状态爆炸的主要来源。第三，约束与断言分离：assume 描述环境允许的输入行为，assert 描述设计必须满足的输出行为，两者混写会导致工具误报或漏报。

下面给出一份可直接参考的建模检查清单，用于在RTL提交形式验证前做自检：

需要强调的是，形式验证不是替代仿真，而是把“穷举输入空间”这件事交给工具。RTL建模阶段把契约写清楚、把状态空间收敛好，形式验证才能真正发挥价值；反之，如果RTL本身存在组合环或未初始化状态，再强的工具也只能报出大量无意义反例。因此，建模规范与可验证性设计应当同步进行，而不是先写完RTL再补断言。