第四章Superlint 静态检查

概述

Superlint App 将传统 Lint 检查与形式验证结合，不仅检测代码风格和语法问题，还通过形式证明验证 Lint 检查发现的问题是否真的会在设计中触发，大幅降低 false positive（误报）率。

主窗口概览

两种 Setup 流程

JasperGold 流程

1. 在 JasperGold 中加载设计（analyze + elaborate）
2. 配置要运行的检查规则
3. 排除特定实例/层级
4. 运行检查

Xcelium 流程

1. 在 Xcelium 编译流程中启用 Superlint
2. 导入 HAL Design Information Files
3. 配置和运行检查

配置检查

# 启用/禁用检查规则
set_superlint_check -rule {CON_IS_PATH CON_NO_PATH} -enable
set_superlint_check -rule {CODINGSTYLE} -disable

# 排除特定层级
set_superlint_exclude -hierarchy top.testbench

# 保存配置
save_superlint_config config.tcl

运行检查

Design Build Violations

首先检查设计是否能成功编译，编译错误会阻止后续检查。

Extracting and Proving Checks

# 提取并证明检查
run_superlint -extract
run_superlint -prove

Superlint 将 Lint 规则转化为形式断言，运行证明：

• Proven Violation：确认的违规（可达的问题）
• False Positive：误报（形式证明该问题不可达）
• Inconclusive：不确定

Rule Profiling

分析每条规则的运行时间，识别耗时规则。

Noise Filtering

自动过滤低质量/重复的报告。

导出为 SVA

# 将 Lint 检查导出为 SVA 断言
export_superlint_to_sva -output checks.sva

结果分析

• Message Details：每条违规的详细描述和位置
• Related Violations：相关违规分组
• Analysis Browser：按类别/严重程度浏览
• Schematic Viewer：原理图查看问题路径
• FSM Graph Viewer：状态机图分析
• Visualize：查看违规波形

Persistent Waivers

Waiver 可以保存在文件中，在回归中持续生效：

# 保存 waiver
save_waivers waivers.txt

# 加载 waiver
load_waivers waivers.txt

定制规则文件

Superlint 支持自定义 Lint 规则文件，添加项目特定的检查。详细语法参见官方规则定制指南。

Superlint 检查结果界面

静态检查方法论

lint vs formal-lint：质的区别

传统 Lint 工具做的是静态模式匹配——发现代码中"看起来可疑"的模式（如未驱动的信号、可能越界的数组），但不能证明 bug 真正可达。很多 lint warning 是假阳性（实际不可能发生）。

Superlint 的 AUTO_FORMAL 功能用形式引擎证明 bug 可达：它生成断言检查可疑模式是否真能被触发，如果 proven（不可能发生）就放心忽略，如果 failed（能触发）就是真 bug。这大大减少了假阳性。

修复优先级

不是所有 warning 都需要修

AUTO_FORMAL 的优势就是帮助你区分：

• proven 的 warning → 形式引擎证明这个可疑路径不可能触发 → 可以安全忽略（waive）
• failed 的 warning → 形式引擎找到了触发路径 → 这是真 bug，必须修
• undetermined 的 warning → 引擎超时无法确定 → 手动 review 或增加约束

Waiver 策略

对于确认是假阳性的警告，使用 waiver 机制而不是修改代码：

• Waiver 应附带注释说明为什么可以安全忽略
• 条件 waiver（-expression）优于无条件 waiver
• 定期 review waivers，设计变更后需要重新验证