第三章SEC 时序等价检查

概述

时序等价检查是形式化地比较两个 RTL 设计——规格（specification，简称 spec）与实现（implementation，简称 imp）——以验证二者等价。

SEC App Use Models

任何比较活动都可以算作一般意义上的 SEC 用例。以下是文档列出的常见使用模型：

• Clock gating insertion（时钟门控插入）：确保时钟门控不影响功能。spec 中时钟常开，imp 针对动态功耗做了优化。时钟门控的 bug 很关键，因为往往会导致整片区域"熄灯"。
• Re-partitioning and pipeline retiming（重划分与流水线重定时）：修复综合时序违例、缩短路径长度。比较有流水线的 spec 与流水线被改动过的 imp（逻辑在触发器级之间移动、增删流水级、复制触发器等）。
• Code cleanup（代码整理）：让遗留代码变得可读、可维护，这通常是后续增强代码的前提。
• Features addition/removal（功能增删）：保持向后兼容，确保功能等价。
• ECO insertion（ECO 插入）：保持向后兼容，比较 spec 与 imp 中已有的功能，新增功能另行验证。
• Parameterization（参数化）：验证参数化代码。需要把参数化版本的每一种配置都与 spec 设计比较。
• CPU lockstep verification（CPU 锁步验证）：面向功能安全需求，在原始 CPU 核旁放置冗余核。目标是确保在没有故障时两个模型行为完全一致。
• Reset optimization（复位优化）：降低功耗和面积。因为带初始化的触发器比不带初始化的更昂贵，此模型比较"触发器带初始化的 spec"与"触发器不带初始化的 imp"。

SEC 工作流程

1. 加载两个设计（spec 和 imp）
2. 使用 Setup Wizard 配置
3. 检查接口（Interface Check）
4. 精化映射（Mapping）
5. 生成验证环境
6. 运行等价证明
7. 签核（Signoff）

check_sec -setup -spec_top uart_top ...
check_sec -auto_map_reset_x_values on
check_sec -interface
check_sec -map -spec {wb_adr_i[4:0]} -imp {uart_top_imp.wb_address_i[4:0]} \
               -respect_connections_during_reset -global
check_sec -gen
check_sec -prove
check_sec -signoff

Setup Wizard

在 Designs 区域，可以选择 Different spec and imp designs（分别指定 Spec design top name 和 Imp design top name），或 Same spec and imp design（为两者指定同一个 Top）。

Options 区域可接受默认设置，或勾选以下选项：

• No Auto-Mapping：禁用对 spec 和 imp 实例边界目标 COI 内信号的映射
• Auto Map Reset X Values：自动映射不可复位或未初始化的触发器/锁存器对。该功能完全自动——复位变化时会自动增删 init 映射，用户只能开或关
• Map One Side Reset X：进一步自动映射仅在一侧（spec 或 imp）不可复位/未初始化的触发器和锁存器
• Exclude Undriven Mapping：排除 spec 和 imp 中同名的未驱动信号的映射
• Auto-map cover gated clocks toggle：自动创建时钟门控翻转覆盖率的映射，用于检查 imp 与 spec 两个门控时钟之间是否不等价，作为时钟门控用例的合理性检查

另可用 Load global setup file 指定一个 elaborate 之前的 Tcl 设置脚本。

接口检查（Interface Check）

check_sec -interface

# 常用变体
check_sec -interface -mapped
check_sec -interface -imp
check_sec -interface -ignore_user_stopats

接口检查用于评估模型映射的完整性。一对被映射的信号，意味着这两个信号应当被"假定相等"或"验证相等"。例如边界输出映射（Boundary outputs mapping）会检查所有输出和黑盒输入是否都已映射。

映射精化

层级别名规则（Hierarchy Aliasing Rules）

层级别名不是通过独立命令创建的，而是在 GUI 中定义后由命令应用：使用 Spec expression 和 Imp expression 字段定义要映射的 spec/imp 层级名或子名，点击 Add Rule，然后运行命令应用该规则：

check_sec -map -auto

高级映射选项

高级映射选项对话框提供的是时序与功能上下文相关的选项，包括 clocking_event、disable_cond_expression、spec_cond_expr、imp_cond_expr、spec_cond_delay_value、imp_cond_delay_value，以及 RegExp / Inverse / Init / Bit blast / Speculative 等复选框。

Expert / Non-Expert View

SEC 提供两种视图模式：

• Non-Expert View：简化的界面，自动配置大部分参数
• Expert View：完整控制映射、约束和证明选项

证明优化

Proof Cache

# Proof cache 默认是关闭的，需显式启用
set_sec_autoprove_use_proof_cache true

# 可选：指定缓存路径
set_sec_autoprove_proof_cache_path <path>

AutoProve 策略

SEC 的证明策略通过 check_sec -prove -strategy 指定，共有四种：

check_sec -prove -strategy basic
check_sec -prove -strategy proof
check_sec -prove -strategy bug_hunting
check_sec -prove -strategy design_style

也可以用变量 set_sec_autoprove_strategy 设置。

Failure Extension

Failure Extension 是一项能力，而不是一组策略。SEC App 在 basic 和 bug-hunting 两种 AutoProve 策略下都支持它：

• 使用 bug-hunting 策略时，Failure Extension 默认开启
• 要在 basic 策略下使用，需在命令中额外加 -failure_extension 开关

check_sec -prove -strategy basic -failure_extension

SEC 等价检查界面

SEC 验证方法论

SEC 适用场景

时序等价检查（SEC）在以下场景中不可或缺：

• 代码整理 / RTL 重构：重写模块以改善可读性或时序/面积/功耗，但需要保证功能不变
• ECO 插入：后期修改，需要确认已有功能保持向后兼容
• 流水线重定时：为修复综合时序违例而移动逻辑、增删流水级后验证等价性
• 设计优化验证：插入时钟门控后验证等价性

映射策略

SEC 的核心是建立 spec（原始）和 imp（修改后）之间的信号映射：

• 自动映射：工具根据层次名和信号名自动匹配（同名、同端口位宽）
• 手动映射：自动匹配失败的信号需要手动 map（如重命名的信号、位宽变化的端口）
• 黑盒映射：不重要的模块可以黑盒化，工具只比较黑盒接口的等价性

不等价结果分析

当 SEC 报告不等价时，按以下顺序排查：

1. 映射错误：检查自动映射是否正确配了信号（最常见原因）
2. 接口不匹配：spec 和 imp 的端口列表是否一致？用 check_sec -interface
3. 复位/X 值差异：未初始化寄存器处理不同？用 -auto_map_reset_x_values on
4. 真的不等价：映射确认正确后，看反例波形找到差异点——这是真正的修改 bug