第六章Visualize 波形调试环境

概述

Visualize 是 JasperGold 的集成调试环境，提供波形查看、源码浏览、信号追踪、根因分析等功能，是调试反例和理解设计行为的核心工具。

Visualize 窗口导览

Classic View（经典视图）

Classic Visualize 窗口由标题栏、菜单栏、工具栏、waveforms pane、Source Pane（含 Source Pane 工具栏）以及若干视图标签页组成：

Waveforms pane：信号波形显示区，带 current-range 和 full-range 标尺
Source Pane：RTL 源码显示区，Why / Relevant Loads 等操作的高亮结果显示在这里
View tabs（视图标签页）：Visualize Configurations、Indexed Behaviors、Signal Browser、Task Context

Simplified View（简化视图）

精简界面，聚焦于波形调试和反例分析。

窗口停靠（Docking）

所有面板都可以拖拽停靠、浮动或关闭，自定义布局。

Visualize 波形调试窗口：上方为波形，下方 Source Pane 高亮相关代码，底部显示 Why 结果提示

Visualize 工作流

Property Visualization

双击属性自动加载其波形，显示断言在每个周期的评估结果（pass/fail）。

RTL Exploration with Waveforms

在 Source Pane 中点击信号可以添加到波形中，实时探索 RTL 行为。

Design-Space Tunneling

Design-space tunneling（DST）流程用 Visualize 窗口把目标信号从失败周期回溯到根因。从 Property Table 的右键菜单打开 Visualize 窗口，在 Visualize 对话框中点击 DST 选项即可使用；随后可用 waveforms pane 和 Source Pane 中的菜单项与工具栏按钮（Analyze Conflicts and Boundaries、Suggest Actions on Conflicts and Boundaries、Modify Task Context、Set Local Task Context as AR）进行调试。

State-Space Tunneling

State-space tunneling（SST）是一种推进证明收敛的进阶技术：对状态空间庞大、难以证明的关键属性，通过添加辅助断言（helper assertions）逐步收敛。这个过程是手动的，通常需要花不少时间才能收敛，因此只在目标属性对项目足够关键、值得投入时才使用，一般用在设计已经稳定、项目接近尾声的阶段。

适合 SST 的典型场景包括：存在 token leakage 属性的设计、复杂流水线、cache 一致性问题，或多个状态机之间存在关联的设计。

注意：set_sst_mode 命令及其启用的流程正在被废弃，由基于 Visualize 的新流程取代。

波形配置

# 在 GUI 中（括号内为官方快捷键）：
# 1. 添加信号：Signal pane 中 Add signals            (Alt+A)
# 2. 加扇入/扇出：Add fanin (Ctrl+1) / Add fanout    (Shift+Ctrl+1)
#    传递扇入到输入：Add transitive fanin to inputs   (Ctrl+2)
# 3. 保存信号列表：File → Save Signal List           (Ctrl+S)
#    找回上一次的信号列表：Recover previous signal list (Ctrl+R)
# 4. 保存整体配置：File → Save Visualize Configuration
# 5. Freeze 功能：锁定 trace 中的值，使后续操作不再改变它们

保存 highlight 的默认行为：用 File – Save Signal List 时工具默认会连同高亮一起保存；如果不想保存高亮，改用 Save Signal List As 并取消勾选 Save 高亮的选项。

Building Your Waveform

逐步添加信号构建波形视图。当前窗口布局和波形配置用 File → Save Visualize Configuration 保存。使用 freeze 功能时，工具会锁定 trace 中的值，使所有后续操作都不再改变它们。

QuietTrace 和多 Trace 窗口

QuietTrace 的作用是"让波形安静下来"：减少波形上边界处和内部逻辑中发生翻转的信号数量，让反例里真正相关的活动更容易看出来。

默认的 QuietTrace 生成方法作为独立引擎运行——一旦工具为某个属性找到 trace，引擎 QT 就开始跑（配置方式见 set_separate_engine_qt）。点击 QuietTrace 按钮旁的下拉箭头可打开 QuietTrace Advanced Settings 对话框，为每次 QuietTrace 引擎迭代设置时间限制，默认值 0s（不限）。

给 quiet 尝试设了时间限制后，部分 soft constraint 可能来不及被充分考虑，因而可能不被满足。

多 Trace 窗口则用于管理多个反例波形窗口、比较不同反例（是否弹出新窗口由 Visualize Preferences 的 Replot Setting 控制）。

Local Task Context

用 Modify Task Context 对话框指定新的 property、justify 或 stopat，作为对 AR 的临时修改保留下来，再用 Replot 查看修改的效果。确认无误后用 Set Local Task Context as AR 把这些改动（例如新增的 justify 和 stopat）正式写入 AR——此时改动在数据库中固化，不再列在 Task Context pane 里，但仍可在 Task Context 对话框中追踪。

WaveEdit Mode

WaveEdit 提供一种所见即所得（what-you-see-is-what-you-get）的方式来"指定约束"——这是理解它的关键：你在波形上画出想要的值，工具据此生成约束，而不是像仿真器那样"强制"一个值再看结果。

点击 Visualize WaveEdit Mode 工具栏按钮进入该模式，会出现一个可移动的浮动 palette，包含"应用改动（可选是否 replot）"、清除、切换到 erase 模式等按钮。

进入 WaveEdit 模式后，控制权交给鼠标的 create / erase 操作，其他按钮、菜单和命令都会被禁用。在波形区右键可打开 WaveEdit 上下文菜单，用来关闭 create 模式、清除尚未提交的改动、撤销和重做。

还可以从主窗口实例树、Source Browser 以及 Visualize 的 Source Pane 右键选择 Instance WaveEdit，为所选实例显示一条带主 I/O 的单周期 trace（target 是 Cover {1}），用来探索这个实例"能发生什么"，构造 what-if 场景。

约束强度可调：Visualize Preferences 中的 WaveEdit 选项可让 WaveEdit 改用较弱的 -at_least_once 约束。

WaveEdit 不支持：来自 visualize -load 或 -confirm 的 trace、package、以及 Bits Set radix。

高级调试功能

Indexed Behaviors Pane

Indexed Behaviors pane 显示当前上下文中的属性，帮助你理解设计行为。Visualize 可以分析这张表里的属性，显示 cover 在哪些周期被 exercise、assertion 或 assumption 在哪些周期失败。

这个分析需要触发，有三种方式：

手动对所有属性运行：点表格左上方的分析按钮（tooltip 为 Analyze exercised covers and violated assertions and assumptions）
自动对所有属性运行：点分析按钮旁的下拉箭头选 Analyze Automatically，或在 setup 文件里写 set_visualize_auto_check_props on
手动对选定属性运行：选中一个或多个属性，右键选 Analyze Properties

自动分析会拖慢运行速度，大设计上慎用。

Relevant Logic（相关逻辑高亮）

显示与 trace 中某个事件相关的信号。它做的是高亮，不是隐藏；详见前面 "Relevant Logic：高亮相关逻辑" 一节。

Relevant Differences

和 Relevant Logic 是一对：Relevant Logic 显示与某一条 trace 中某个事件相关的信号，而 Highlight Relevant Differences 显示同一信号在两条不同 trace 之间的差异（例如 CEX 对 witness）。

关键在于它取的是交集：高亮那些既在某一条 trace 中是相关的、又在两条 trace 之间取值不同的信号。这样你就能聚焦地做"根因分析"——比如搞清楚 CEX trace 里到底发生了什么，才使它没能成为一条 witness trace。

两个典型用途：Fairness 调试（高亮 liveness CEX 与 witness trace 之间的 relevant differences）、不可达 cover 调试（高亮两条 not-from-reset trace 之间的差异，其中一条命中 cover 目标、另一条没命中）。

用法：点击关注的 signal-cycle 单元格 → 右键 → Highlight Relevant Difference。两个 Visualize 窗口会成组显示相同的相关信号，若某些周期在两窗口间取值不同，这些相关周期会被高亮。

Why / Relevant Loads / Driver / Load

Why：在 Source Pane 中灰色高亮——指定周期直接扇入中影响证明结果的信号
Relevant Loads：同样是灰色高亮，但看的是直接扇出中影响证明结果的信号
Driver：显示给该信号赋值的那段源码
Load：列出该信号作为负载出现的所有 RTL 行

对主输入信号执行 Driver 时，工具会弹窗问你是否改为跳转到该信号的声明处；对话框可以记住你的选择，之后要改回来需编辑配置文件 ~/.config/jasper/jaspergold.conf。若 Driver 或 Load 操作遇到 stopat，工具会问你是否跳转到被 stopat 切掉的那部分原始逻辑。

Source Debugging

Source Pane 支持以下调试特性：

Source Pane with in-line value annotations：显示带高亮、标记和 tooltip 注解的设计代码。默认开启行内值注解配合 Why——跑完 Why 后，被高亮信号的值会以灰色显示在信号名正下方那一行。右键选 Show In-Line Value Annotation 或用 Source Pane 工具栏的组合框在三档之间切换：Off（关闭）、Relevant（只显示与 Why/Relevant Loads/Driver/Load 相关的信号值）、COI（显示目标属性影响锥内所有信号的值）
Navigation pane：含 Hierarchy 和 History 两个标签页。Hierarchy 用于在设计层次中导航，工具会高亮树中当前位置并在相邻 pane 显示对应源码；History 列出你做过的 Why、Relevant Loads、Driver、Load 操作，点击其中一项即可查看对应源码——对 Why/Relevant Loads 它是 Back/Forward 按钮的替代，对 Driver/Load 则为每个 driver 或 load 显示一个节点，是 Previous/Next 按钮的替代
Top-Level Window / Undock：点 Source Pane 右上角的上箭头把它作为独立窗口打开（关闭后恢复为停靠 pane）；点 undock 按钮让它自由浮动

高级时序调试

Liveness Properties 调试

在主 GUI 中对 liveness 断言选择 View Violation Trace 后，Visualize 窗口会给出专门的指示：窗口页脚出现 Looping 标签，表示这条 trace 是无限长且包含一个循环的。波形中，反例由 stem（引导段）和 loop（循环段）两部分组成，loop 用米色背景加上 current-range 标尺（pane 顶部）上的标签标出。

要把循环重复展开若干次：在 current-range 标尺上右键 → Unroll Loop，指定展开次数。展开部分的背景是另一种黄色（与 loop 段的颜色不同），同时 pane 底部的 full-range 标尺会用绿色标示展开部分。

该上下文菜单项仅对 liveness trace 有效。另外在 VNC 中可能需要临时提高客户端显示色深，才能分辨这几种背景色和标尺底纹。

Frozen Cycles（冻结周期）

这和 liveness 无关，是独立特性。使用 freeze 后，工具会锁定 trace 中的值，使今后所有的 Visualize trace 配置在那些"信号/周期"组合上都保持与当前 trace 相同的值。被冻结的周期显示为米色背景。

Freeze 不支持 X-Prop、SPV、cover -path 属性，也不支持 SST 流程。

Comparing Signals

这个功能比较的是两个信号，不是任意多个，而且没有"自动对齐边沿"这回事——需要偏移时由你手动指定周期数。

用法：在波形中选中两个信号名 → 右键 → Compare Signals，弹出的对话框已预填 Signal A 和 Signal B。可选项包括：

Shift cycles：指定正值把 signal B 的比较位置右移，负值左移
Ignore X：比较时忽略 X 值
Ignore value：忽略指定的值

比较结果的呈现方式：不匹配的周期上会出现 tooltip 显示两个信号各自的值，例如 4'h02 <> 4'hF3；item 列表中信号名上的 tooltip 则报告本次比较的信息（信号名和你指定的选项）。

支持的类型：单 bit 信号、一维向量、transaction。

Appendix: Keyboard Shortcuts

Visualize 提供丰富的键盘快捷键加速调试操作，包括：波形缩放/平移、信号导航、时间光标移动等。

Visualize 波形调试

波形调试方法论

Visualize 不是"看看波形"的工具，它是你定位和理解反例的核心武器。证明失败只是告诉你"属性被违反了"，但波形告诉你"怎么违反的、为什么违反"。

反例阅读思路

从末尾倒推：找到断言失败的时钟周期（红色标记 Current 位置），先看那个周期的信号值，再向前追溯
先看输入再看内部：确认输入信号是否合法（如果输入本身就不合法，说明约束不够）
关注异常值：对可疑的 signal-cycle 单元格执行 Highlight Relevant Logic，被高亮出来的信号就是与之相关的逻辑（默认 Auto 配色下，第一次 relevant logic 操作用红色高亮）
用时间游标定位：将游标移到关键变化沿，逐周期分析信号关系

Why 分析：看直接驱动来源

右键信号 → Why 是最高效的调试功能之一。它在 Source Pane 中用灰色高亮标出：在指定周期，直接扇入（immediate fanin）中哪些信号影响了所选信号（或 Tcl 表达式属性）的证明结果。

Why 只看一层：Why 分析的是 immediate fanin，不会自己递归展开。要沿 RTL 一路传递地追下去，用下面的 Highlight Relevant Logic——它执行的才是传递性（transitive）的 Why 操作。

相关的三个配套操作：Relevant Loads（灰色高亮直接扇出中影响证明结果的信号）、Driver（显示给该信号赋值的那段源码）、Load（列出该信号作为负载出现的所有 RTL 行）。Source Pane 工具栏会显示你最近一次的操作；如果上一次是 Why 或 Relevant Loads，之后双击会重复同样的操作，其他情况下双击执行 Driver。操作历史可以在 History 标签页中查看。

Relevant Logic：高亮相关逻辑

在波形中右键某个 signal-cycle 单元格，用上下文菜单指定希望工具高亮哪一类相关逻辑：

Highlight Relevant Logic：执行传递性的 Why 操作，替你遍历 RTL，高亮某信号 buffer cloud 的两端
Add Relevant Module Instance Port Signals：只显示 target 所在实例的 module port
Add Relevant Input/Undriven Signals：只显示主输入和未驱动信号

它是"高亮"不是"过滤"：Relevant Logic 只做颜色高亮，不会隐藏或筛掉任何信号。配置项是 Relevant logic configuration（all / data path / control path）和 Color scheme（Auto，或 Temperature——按 Why 的迭代层数用红、橙、黄、蓝、绿依次着色）。

Tunneling：两种完全不同的 Tunneling

名字相近，用途完全不同，别混淆：

DST（Design-Space Tunneling）：调试用。把目标信号从失败周期回溯到根因，在 Visualize 对话框里选 DST 选项进入。
SST（State-Space Tunneling）：收敛用。靠手工添加 helper assertion 推进难证明属性的收敛，跟看波形没关系。

WaveEdit：What-if 分析

WaveEdit 允许手动修改波形中的信号值（将某个信号从 0 改为 1），然后观察波形如何变化。这可以用来验证"如果信号 A 是正确的，后面的行为是否正确"——帮助区分设计 bug 和属性错误。

高效调试流程：打开反例波形 → Why 看失败信号的直接扇入 → Highlight Relevant Logic 沿 RTL 传递地高亮相关逻辑 → 在 WaveEdit 中修正值验证假设 → 用 Driver 回到源码定位 bug 行。

来源文档

jaspergold_visualize_gui.pdf
jaspergold_apps_userguide.pdf Ch.7