4、Formality GUI操作：图形界面布局、加载设计、运行比对、查看结果
说实话，很多工程师对Formality的第一印象就是「命令行工具」。但我要告诉你，GUI模式在调试复杂问题时，真的能帮你省下大把时间。我个人习惯是：跑回归用脚本，查问题开GUI。今天我们就来聊聊怎么用好这个图形界面。
4.1 图形界面布局：别被密密麻麻的按钮吓到
第一次打开Formality GUI，你可能会觉得有点懵。别急，我来帮你拆解一下。
启动GUI很简单，在终端输入：
formality -gui或者你已经跑完了batch模式，想直接看结果：
formality -gui -session fm.svf嗯，这里要注意，fm.svf是session文件，保存了你上次比对的所有信息。
界面主要分这么几个区域：
- 菜单栏：在最上面，File、Edit、Run这些，跟其他EDA工具差不多
- 工具栏：常用操作的快捷按钮，比如加载设计、运行比对
- 设计浏览器：左侧的大区域，显示你的设计层次结构
- 控制台：底部，打印log信息，报错也会显示在这里
- 结果面板：右侧，显示比对结果、不匹配点等信息
我记得第一次用的时候，找了半天「开始比对」的按钮。其实就在工具栏上，一个绿色的三角形图标，跟播放键似的。
4.2 加载设计：把两个版本请进来
做形式验证，核心就是比两个设计：一个是参考设计（Reference），一个是实现设计（Implementation）。
在GUI里加载设计的步骤：
- 点击菜单栏 File → Read Design
- 在弹出的对话框里，先选 Reference，加载你的黄金模型（比如RTL综合前的网表）
- 再选 Implementation，加载你要验证的设计（比如综合后的门级网表）
- 指定 Top Module，告诉Formality哪个是顶层模块
这里有个小技巧。我建议你加载设计时，把 SVF文件 也带上。SVF文件记录了综合过程中的优化信息，能帮Formality更准确地理解设计意图。
加载完成后，你会在左侧的设计浏览器里看到层次结构。双击某个模块，可以展开看内部逻辑。这个功能在定位问题时特别有用。
4.3 运行比对：点一下按钮，剩下的交给工具
设计加载好了，接下来就是运行比对。操作很简单：
- 点击工具栏上的 绿色三角形按钮（Run Verification）
- 或者菜单栏 Run → Verification
工具会开始做匹配（Match）和比对（Compare）。匹配阶段，Formality会尝试把Reference和Implementation里的逻辑点对应起来。比对阶段，就是检查这些对应点的逻辑功能是否一致。
你可以在控制台看到实时进度：
// 匹配阶段
Matching: 85% complete...
Matching: 100% complete - 12456 matched points
// 比对阶段
Comparing: 50% complete...
Comparing: 100% complete - 0 failing points为什么会看到「0 failing points」？这说明两个设计完全一致，恭喜你！
但现实往往没那么美好。如果出现不匹配，别慌，我们接着看怎么查。
4.4 查看结果：找到问题，解决问题
比对完成后，结果面板会显示汇总信息：
| 项目 | 说明 |
|---|---|
| Total Compare Points | 总共比对了多少个逻辑点 |
| Matched Points | 成功匹配的点数 |
| Failing Points | 比对失败的点数 |
| Unmatched Points | 未能匹配的点数 |
如果有Failing Points，双击它，工具会打开一个 Schematic Viewer，把两个设计的逻辑路径画出来。红色高亮的就是不匹配的地方。
我个人习惯是这么排查的：
- 先看 Unmatched Points。这些点没对上，后面的比对肯定失败。常见原因是命名规则不同，或者综合时优化掉了某些寄存器。
- 再看 Failing Points。点开Schematic，对比两条路径。有时候是综合插了扫描链，有时候是时钟门控逻辑变了。
- 用 Debug → Analyze Failing Points 功能，工具会给出一些诊断建议。
避坑指南： 我曾经遇到过一个案例，比对失败的点全是加法器。查了半天，发现是综合时用了不同的加法器架构（一个用Carry Lookahead，一个用Ripple Carry）。功能上其实一样，但Formality默认的匹配策略没认出来。解决办法是加一条命令：set verification_clock_gate_hold_mode any，让工具放宽匹配条件。
查看结果时，还有几个实用功能：
- Report → Failing Points：生成一份详细的失败点报告，可以保存成文本
- Report → Unmatched Points：查看未匹配点的列表
- View → Logic Cone：查看某个点的逻辑锥，帮你理解它为什么失败
嗯，基本上GUI操作就这些。说白了，加载设计、点一下运行、看结果，三步走。但真正花时间的，是分析那些不匹配的点。这时候GUI的图形化展示就比命令行好用太多了。
最后提醒一句：GUI适合调试，但回归验证还是建议用脚本。毕竟你不想每次改完代码，都手动点一遍按钮吧？