使用 Magellan 对仲裁器进行端到端形式验证

SNUG San Jose 2008 2008 17 页

使用 Magellan 对仲裁器进行端到端形式验证

论文信息

项目	内容
作者	Hari Ganesan、Devin Volpe（Sun Microsystems）
会议	SNUG San Jose 2008
页数	17 页

摘要

本文介绍了用户使用形式验证方法和验证 Sun 公司某款 SPARC 处理器中程序计数器选择（PC Select）逻辑仲裁器的经验。该模块的功能是根据优先级规则，为来自控制转移指令逻辑或陷阱处理逻辑的请求赋予优先级，并选择一个程序计数器（PC）供未来执行跳转使用。请求可以来自核心中的任何线程（strand）。由于核心在不同的执行模式下运行，优先级逻辑变得复杂。

在本文中，我们描述了在不实际查看 RTL 实现的情况下对该模块进行端到端验证所获得的经验。我们概述了被验证的模块、用于为整个逻辑构建属性的分阶段方法，以及使用 Magellan 验证属性的方式。验证过程中遇到的挑战和所采用的解决方案也将被涵盖。本文最后给出一些建议以及我们在设计中获得的结果。

1. 引言

形式验证工具非常擅长在 RTL 中发现深层次的边界情况缺陷。使用形式工具引擎验证 RTL 模块的属性，即使该模块已经历了大量的仿真周期，也能极大地增强对该模块的信心。我们的 PC 仲裁器模块使用 Magellan 进行验证，正是这样的一个模块——它已经经过了无数次仿真周期，但仍希望通过形式验证来确保功能的正确性。

通常，最适合形式验证的逻辑是那些规模较小、具有中到高度复杂性、难以通过仿真编写测试来完全验证的模块。仲裁器正是这类逻辑的典型例子。当一段复杂逻辑被深深嵌入仿真中使用的更高层模型时，验证难度急剧增加。可能很难甚至不可能穷举被验证模块所有可能的合法输入组合。在这种情况下，唯一可用的选择是：a) 编写单元级测试在仿真中验证模块，或 b) 使用形式验证。

在使用单元级仿真的情况下，必须编写诊断程序来为被验证模块生成合法输入。确保所尝试的合法输入与周围逻辑将馈送给模块的输入一致，是一项更加困难的任务。然而对于形式验证方法，通过在仿真周围模块的同时将规范约束转换为断言，问题可以变得更加可控。

最常见的仲裁器类型是轮询（round-robin）或基于优先级的仲裁器。这些是单级仲裁器，其中所有到达仲裁器的输入请求基于轮询或优先级被授予。此外还有多级仲裁器，其中仲裁输入被划分为子集，各子集的获胜者再进行仲裁。在多级仲裁器中，各级之间的仲裁逻辑可能不同。本文涉及的仲裁逻辑是一种自定义类型，不属于上述任何类别。

在本文中，我们讨论了使用 Magellan 验证 Sun UltraSPARC 处理器中程序计数器选择（PCSelect）仲裁器逻辑的经验。我们概述了被验证的模块、模块的接口逻辑和仲裁规则、为该模块构建属性的方法、我们的形式化分阶段方法，以及 Magellan 如何被用于验证属性。

2. PC Select 仲裁器模块概述

以下是与此 PC Select 逻辑接口的模块的简要背景。

2.1 接口模块

与该仲裁器接口的三个主要逻辑模块是：指令获取单元（IFU）、指令执行流水线单元（IEU）和陷阱逻辑单元（TLU）。

PCSelect 逻辑的接口框图如图 1 所示。以 s0_ 和 s1_ 开头的信号名分别来自硬件线程（strand）0 和 1。没有这些前缀的信号由两个线程共享。

指令获取单元（IFU）主要负责从存储器中获取指令以供执行。获取的指令随后被传递给发射单元进行处理。IFU 必须生成待获取指令的地址，同时考虑当前指令流、所有控制转移指令以及需要获取指令的线程。在控制转移指令的情况下，IFU 维护预测结构，用于预测处理器可能执行的指令地址路径，并从那里获取指令。有时，IFU 需要被告知停止并从不同地址获取指令，例如当线程发生陷阱或早期预测不正确时。PC Select 模块正是将这些来自 IEU 和 TLU 的请求传递给 IFU 的通道。这些请求以称为 refetch 的信号形式从 PC Select 仲裁模块发出，并附带相关的 refetch PC 地址。

指令执行单元（IEU）负责执行发射单元提供给它的指令。除了算术指令和其他类别的 Sparc-V9 指令外，IEU 还处理控制转移指令（CTI），这些指令可能要求线程跳转到 CTI 中指定的地址并从那里开始执行。要跳转到的目标地址只有在 IEU 处理 CTI 时才能确定。在该单元中计算出的 CTI 目标地址可能与 IFU 在早期获取过程中预测的"跳转到"地址不同。当发生这种误预测时，IFU 需要开始从正确的目标地址获取指令，并丢弃从预测地址路径获取的指令。为了指示已发生误预测，IEU 通过 PCSelect 逻辑向 IFU 发送一个称为"early-mispredict"的信号以及目标 PC 地址，该信号必须在 PCSelect 逻辑中与来自该核心的 pipe clear 信号和其他线程的 mispredict 信号进行仲裁。当 early-mispredict 请求被 PC Select 仲裁逻辑选中时，refetch 信号被生成并发送给 IFU。

发信号通知 IFU 从误预测地址获取指令仅是处理 CTI 的第一步。控制转移指令通常有延迟槽（delay-slot），在这些 slot 中需要执行一条有效指令后才能转移控制。在 IEU 完成延迟槽指令的执行之前（处理这条指令可能会有显著的延迟），IFU 不应该发射新获取的指令。为了指示 IFU 可以开始从新地址发送指令，IEU 使用另一个称为"late-mispredict"的信号。late-mispredict 信号同样经过 PCSelect 仲裁逻辑，当被授予时生成 refetch_gnt 信号给 IFU。

陷阱逻辑单元（TLU）报告异常并与处理器流水线协调控制转移。其主要职责是检测异常、对这些异常进行优先级排序，并在适用时处理它们。TLU 负责提交流水线的最后阶段，因此在发出请求时比其他流水线具有优先级。每当发生陷阱或异常时，TLU 向其他单元发送 pipe-clear 信号，以基本上停止它们正在做的事情。该 pipe-clear 信号以及相应的 pipe-clear 地址 PC 也被 PC Select 逻辑接收，以进行仲裁并传送给 IFU 进行获取。

2.2 PC Select 仲裁器逻辑

该模块的主要功能是在来自 TLU 的 pipe clear 信号和来自 IEU 的 early/late mispredict 信号之间进行仲裁。仲裁逻辑基于某些仲裁规则生成 refetch 或 refetch_gnt 信号，以及相应的目标 PC（refetch_pc）。

来自 TLU 的输入： 1. 两个线程的 pipe clear 信号：s0_pipe_clear、s1_pipe_clear 2. 两个线程的 64 位目标 PC 总线：s0_pipe_clear_pc[63:0]、s1_pipe_clear_pc[63:0]

来自 IEU 的输入： 1. 两个线程的 early mispredict 信号：s0_early_mispredict、s1_early_mispredict 2. 两个线程的 late mispredict 信号：s0_late_mispredict、s1_late_mispredict 3. 两个线程共享的 64 位目标 PC 总线：target_pc[63:0]

该模块生成的输出： 1. 相应线程的 refetch 信号（s0_refetch、s1_refetch），附带 64 位 refetch_pc[63:0] 2. 相应线程的 refetch_gnt（s0_refetch_gnt、s1_refetch_gnt）

还有其他进入该模块的输入信号，这些信号未在上文中提及，且对本文讨论的形式验证来说不是关键的。

2.3 仲裁规则

PCSelect 逻辑使用各种自定义规则来选择发送给 IFU 进行 refetch 的目标 PC。以下是一些主要的仲裁规则列表，为简洁起见省略了其他规则：

1. 一个线程的 early 或 late mispredict 信号比另一个线程的 pipe clear 具有更高的优先级。 2. 如果 strand0 pipe_clear 和 strand1 pipe_clear 在同一周期发生，strand0 pipe_clear 先于 strand1 pipe_clear 被授予。 3. 如果一个线程的 early 和 late mispredict 在同一周期或在该线程 pipe clear 信号的 3 个周期窗口内发生，则该线程的 early 和 late mispredict 被丢弃。 4. 如果一个线程的 early mispredict 与另一个线程的 late mispredict 同时发生，丢弃 early mispredict。 5. 在 strand0 late mispredict 和 strand1 pipe clear 在同一周期发生、随后 strand0 pipe clear 在下一周期发生的情况下，refetch 授予顺序为：strand0 late mispredict，strand0 pipe clear，strand1 pipe clear。

图 2 描述了规则 5 的时序图。

注意：上述规则适用于同步多线程模式（SMT）。这些规则对于同步单线程模式（SST）略有不同，此处省略。

2.4 自定义仲裁器特性

该仲裁器具有一些有趣的特性使其适合形式验证。该模块支持多种总线输入/输出协议。其输入条件源于 Sparc 核心中各种复杂的控制转移类型。我们需要检查不同的数据包结构、各种优先级方案以及许多边界情况。这些特性的组合使得穷举仿真变得不可行，而形式验证成为必要且有效的替代方案。

3. 分阶段形式验证

3.1 分阶段验证的原因

我们将验证分为多个阶段进行。一次性构建所有属性过于复杂且容易出错。分阶段的方式可以逐步建立对子模块的信心，约束条件可以逐步细化，每个阶段的验证结果可以指导下一阶段的策略。

3.2 验证环境设置

使用 Magellan 建立验证环境，包括：设计读入（RTL）、时钟和复位定义、输入约束（assume 属性）、待证属性（assert 属性）和覆盖属性（cover 属性）。

4. 约束条件

验证仲裁器需要仔细定义输入约束，以确保形式验证工具只探索合法的输入空间。约束条件包括输入数据包的格式约束、请求信号的互斥约束以及模式位的合法组合。

4.1 验证约束的正确性

约束条件本身也需要验证。过于宽松的约束会导致工具探索非法状态空间并报告虚假违例；过于严格的约束则可能排除合法的边界情况。我们采用覆盖属性来验证约束的正确性——确保在有约束的情况下，我们关心的所有合法场景都能被探索。

5. 属性

5.1 使用自定义 FIFO 实现属性

仲裁器的行为本质上是顺序逻辑——输出取决于输入的历史序列。为了简洁地表达这些行为，我们使用自定义 FIFO 结构来捕获输入序列并在属性中引用。FIFO 使得我们能够跟踪多个周期内的请求序列，并验证仲裁决策是否符合规则。

5.2 使用 FIFO 检查仲裁规则的示例

下面是一个使用 FIFO 检查优先级规则的简化示例：

property arb_priority_check;
  @(posedge clk) disable iff (!rst_n)
  (req_a && !req_b) |=> (grant == A);
endproperty

复杂仲裁规则（如规则 3-5）需要多周期跟踪和 FIFO 结构来捕捉请求序列和相应的授予顺序。

5.3 属性模块

我们将所有属性组织在一个独立的属性模块中，与设计模块分离。这提高了可维护性，并允许在不修改设计 RTL 的情况下迭代更新属性。当需要修改或添加验证规则时，只需修改属性模块，无需触碰设计代码。

5.4 从 OVA 迁移到 SVA

我们最初使用 OpenVera 断言（OVA）编写属性，后来迁移到 SystemVerilog 断言（SVA）。SVA 提供了更好的语言支持、更广泛的工具兼容性，并且作为 IEEE 标准具有更好的长期可维护性。迁移过程中需要注意两种断言语言在语法和语义上的细微差异。

5.5 提高性能的建议

基于我们的经验，以下建议可以显著提升 Magellan 的验证性能： - 使用合理的约束范围，避免自由变量范围过大 - 避免过于宽松的假设条件——这会扩大搜索空间 - 利用 Magellan 的增量验证功能——修改属性后只重新验证受影响的部分 - 合理使用 $assertoff 和 $asserton 等断言控制语句 - 将大的属性集分解为小的独立属性组

6. 覆盖属性

覆盖属性（cover properties）用于确保验证的完备性——验证我们确实测试了所有关心的合法场景。覆盖属性与断言属性互补：断言确保"坏事不会发生"，覆盖确保"好事确实发生了"。

通过 Magellan 的覆盖分析，我们确认了： - 所有关键仲裁场景都被实际探索 - 每个仲裁规则都有对应的测试案例被触发 - 没有遗漏重要的输入组合

7. 结果

使用 Magellan 进行形式验证的结果：

- 发现了仿真未覆盖的多个边界情况缺陷——包括在特定线程组合和时序条件下的仲裁优先级错误。 - 验证了全部关键仲裁规则的完备性——每个规则都有对应的属性进行了验证。 - 通过覆盖分析确认了验证的充分性。 - 建立了对模块功能正确性的高度信心——即便该模块已通过大量仿真周期，形式验证仍然发现了新的问题。 - 验证周期远小于等效的仿真工作量——形式验证在数小时内完成了仿真需要数周才能覆盖的场景。

8. 结论

形式验证是对复杂控制逻辑进行完备验证的强大补充手段，不应被视为仿真的替代品，而应被视为协作工具。

本文展示的关键经验： 1. 仲裁器是形式验证的理想目标——其行为可被清晰定义为规则，适合属性检查。 2. 分阶段方法有效管理验证复杂度——逐步构建和验证属性，而不是一次性完成。 3. 自定义 FIFO 结构是表达顺序属性的实用技术——能够简洁地捕捉和验证多周期行为。 4. 约束条件的正确性至关重要——不正确的约束可能导致遗漏真实缺陷或报告虚假违例。 5. Magellan 提供了从约束编写到属性验证再到覆盖分析的完整形式验证解决方案。

9. 致谢

（原文提及相关团队支持，详见原文。）

10. 参考文献

（原文包含参考文献列表，详见原文。）

核心概念

概念	说明
形式验证 Formal Verification	使用数学方法穷举证明设计属性是否在所有可能输入下成立
Magellan	Synopsys 形式验证工具，支持属性和覆盖分析
SVA SystemVerilog 断言	用于编写形式验证属性的 IEEE 标准断言语言
仲裁器 Arbiter	多请求源优先级选择逻辑，是形式验证的理想目标
属性验证 Property Checking	检查设计是否满足以属性（assertion）形式表达的规范
约束条件 Constraints	将形式验证的输入空间限制为合法值（assume）

使用 Magellan 对仲裁器进行端到端形式验证