第四章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. 配置和运行检查

配置检查

# 初始化 Superlint
check_superlint -init

# 从规则文件加载检查配置
check_superlint -configure -load_rule_file my_rules.def

# 排除特定层级（-exclude_hierarchies 是 -extract 的选项）
check_superlint -extract -exclude_hierarchies top.testbench

# 保存当前配置到规则文件
check_superlint -configure -save_rule_file config.def

检查规则的启用/禁用在规则文件（superlint.def）中完成，而不是通过 Tcl 命令。在类别定义内用 status 参数控制单条规则：

category <category_name>
{
<tag> <severity> <short_message> {status=off}
}

例如禁用 AUTO_FORMAL_SIGNALS 类别中的 SIG_NO_TGRS 规则；也可以在规则文件末尾用 params <tag> {status=off} 达到同样效果。

运行检查

Design Build Violations

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

Extracting and Proving Checks

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

Superlint 将 Lint 规则转化为形式断言，运行证明。用 check_superlint -list -status 按证明状态筛选结果，状态取值为：

• proven：已证明
• cex：找到反例（counterexample）
• unreachable：不可达
• undetermined：未确定
• unprocessed：未处理

Rule Profiling

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

Noise Filtering

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

导出为 SVA

可以把 Automatic Formal 检查导出为 SVA 属性文件。此操作通过 GUI 完成：点击 Application – Import/Export – Export SVA，在 Export SVA 对话框中选择导出过滤条件。注意部分属性没有可用的 SVA 表达式，这些属性不会出现在导出文件中。

结果分析

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

Persistent Waivers

Waiver 通过 check_superlint -waiver 管理，添加时必须给出 -comment 说明原因：

# 按 message/property ID 添加 waiver
check_superlint -waiver -add -id <message_id_tcl_list> -comment "已确认为假阳性"

# 按条件添加 waiver（可组合 -instance/-expression/-category/-tag 等）
check_superlint -waiver -add -category CODINGSTYLE -comment "项目编码风格例外"

# 查看和删除 waiver
check_superlint -waiver -list
check_superlint -waiver -remove <waiver_id_tcl_list>

定制规则文件

Superlint 支持自定义规则文件（superlint.def），可以用 domain 语句把新类别加入 LINT、DFT 或 AUTO_FORMAL 域，再用 category 语句定义类别内的规则。详细语法参见官方规则定制指南。

Superlint 检查结果界面

静态检查方法论

lint vs formal-lint：质的区别

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

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

两个独立的维度：严重级别 vs 证明状态

分析结果时要分清两个互不相关的属性，初学者最容易把它们混为一谈：

• 严重级别（Severity）是规则本身的静态属性，由规则手册预先规定，与是否跑过形式证明无关。例如 CON_IS_PATH 的 Severity 就固定是 Info。规则手册中实际出现的取值只有三种：Error、Warning、Info（其中 Warning 占绝大多数）。
• 证明状态（Status）才是形式引擎跑出来的结果：proven、cex、unreachable、undetermined、unprocessed。

GUI 中的「分组」是另一回事——它把彼此相关的违规归到一起（用启发式识别不同实例中的相同问题，只在列表里显示主检查项并加一个分组图标；修好主违规，同组的通常一并消失），而不是按严重级分档。用 check_superlint -list 时，-severity 支持 error、warning、info 三档过滤，-status 则按上面的证明状态过滤。

不是所有 warning 都需要修

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

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

Waiver 策略

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

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