第六章Combo Loop Viewer

概述

Combo Loop Viewer 是集中查看和调试组合环（combinational loop）的工具。组合环是指没有寄存器打断的反馈环路，会导致仿真和形式验证中的不确定行为。

GUI 标签页

Loop Exploration Tab：显示一棵可展开的组合环树，展开环节点即可看到该环涉及的信号。它有两个二级标签页：点击某个信号可在 Source Browser pane 中高亮它的 driver；在 Properties pane 中可以查看受环影响的属性列表，据此决定证明时是否要禁用某个属性
Loop Handling Flow Tab：分 Manual Loop Handling Flow 和 Automatic Loop Handling Flow 两个视图。手动视图按三棵树分类展示环并配有调试流程图；自动视图在最右侧提供单选按钮，用于指定证明过程中工具应如何处理所有受环影响的属性
Constraint Table Tab：列出能够禁用每个环的约束，并报告能禁用最多环的最小约束组合（minimal constraint set）——这是这个标签页真正有价值的地方。可以在 Constraint Table 或 minimal constraint set pane 中右键应用选定的约束，或在 minimal constraint set pane 的右键菜单中一次性应用全部约束
Signal Heatmap Tab：用热图显示各信号参与已枚举环的程度。判读方式：白色 = 该信号只参与 1 个环；颜色越深红 = 参与的环越多，最深的红色表示它参与了所有已枚举的环——这种信号是最值得优先调试的切入点

默认只显示 10 个环。如果设计中的环多于 10 个，各一级标签页上会出现警示图标。想看全部环要使用 full enumeration 选项，但要注意官方警告：某些设计的环数量可能是指数级的，完整枚举会严重拖长耗时。也可以在弹出控制框或工具栏上点 + 按钮，从上次因达到上限而停止的地方继续枚举，并用旁边的组合框设定这次要再枚举多少个环。

调试组合环

elaborate 后打开 Combo Loop Viewer
查看检测到的组合环列表
在 Schematic 中追踪环路径
确定环的根因（通常是设计 bug 或缺少复位）
修复 RTL，或用 stopat 切断路径，或选定合适的 loop handling 方式

组合环处理决策

什么是组合环、为什么怕它

组合环是没有寄存器打断的反馈路径：信号 A → 组合逻辑 → 信号 B → 组合逻辑 → 信号 A。在仿真中，组合环会导致 X 值传播（仿真器无法确定稳态）；在形式验证中，组合环会导致状态空间不确定，引擎可能无法收敛或给出不可靠结果。

判断和处理流程

1识别：elaborate 后自动检测

打开 Combo Loop Viewer：Window 菜单、session 标签页的右键菜单，或执行命令 check_loop -viewer。在 Loop Exploration Tab 查看所有检测到的环——这个 pane 显示一棵可展开的组合环树。

注意：这个工具在环境层级（environment level）分析设计，不是 task 层级。另外，UNR App 会忽略你的 loop handling 设置，自动切断它遇到的环。

2分类：判断环的类型

点击一个环，在 Schematic 中查看路径。Manual Loop Handling Flow 把环分成三棵树，先看它落在哪一类：

Potentially Unstable Loops：工具无法确认是否稳定 → 需要你重点判断
Stable Loops：稳定的环
Loops in Clock Logic：环涉及时钟逻辑

每棵树左边列出属于该类的环，右边是辅助调试的流程图；流程图中带 "go-to" 图标的方框可以点击，鼠标悬停时会有蓝色描边和 tooltip 提示。

3处理

修 RTL（真 Bug）：插入寄存器打断环，或修改逻辑消除反馈。
切断路径：用 stopat 命令在指定信号或实例处停止遍历 netlist，从而断开环路。
选择 loop handling 方式：在 Combo Loop Viewer 的菜单里三选一—— Use Assume Stable Approach to Handle Loops（假设设计中所有环都是稳定的）、 Use Break Functional Approach to Handle Loops（先枚举所有组合环，再分析哪些是功能上真实的环，然后用最合适的方式打断）、 Use Break Approach to Handle Loops（直接打断设计中所有环的环路径）。分析结束后仍未被分类的环，用 set_loop_handling_fallback 指定处理方式。

Assume Stable 有风险：官方明确警告——用 Assume Stable 处理不稳定的环，可能导致错误的证明结果。

注意：不要过度使用 stopat！每处切断都会减少形式模型的精度，可能导致假 proven。只在你能确认该路径确实不会被触发时才切断，并且切断后要用 cover 确认关键场景仍然可达。同样地，Assume Stable 用在不稳定的环上会直接导致错误的证明结果。

来源文档

jaspergold_apps_userguide.pdf Ch.5