第三章SEC 时序等价检查

概述

时序等价检查验证两个设计（或同一设计的两个版本）在时序行为上是否等价。典型应用场景：

• RTL vs Netlist：验证综合后网表与 RTL 等价
• RTL vs RTL：验证 RTL 修改前后功能等价
• 低功耗插入前后：验证 UPF 插入不改变功能

SEC Use Models

• Golden vs Revised 设计比较
• 接口映射（Interface Mapping）
• 约束映射

SEC 工作流程

1. 加载两个设计（Golden 和 Revised）
2. 使用 Setup Wizard 配置映射关系
3. 检查接口一致性
4. 精化映射（Mapping）
5. 生成验证环境
6. 运行等价证明

Setup Wizard

SEC 提供 Setup Wizard 引导用户完成配置：

• 选择 Golden 和 Revised 设计文件
• 自动匹配端口名
• 配置时钟/复位映射
• 指定等价模式（组合/时序）

接口检查（Interface Check）

# 检查 Golden 和 Revised 的接口是否匹配
check_interface

接口检查报告不一致的端口、宽度不匹配等问题。

映射精化

层级别名规则

# 创建层级别名（处理层级名称变化）
add_mapping_alias -golden "/old_name" -revised "/new_name"

# 高级映射选项
set_mapping_option -case_insensitive
set_mapping_option -prefix_match

Expert / Non-Expert View

SEC 提供两种视图模式：

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

证明优化

Proof Cache

# 启用证明缓存加速重跑
set_proof_cache -enable

Failure Extension

提供两种策略：

• Basic Strategy：标准等价证明
• Bug-Hunting Strategy：专注于寻找不等价的反例

set_sec_strategy -basic
set_sec_strategy -bug_hunting

SEC 等价检查界面

SEC 验证方法论

SEC 适用场景

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

• RTL 重构：重写模块以改善时序/面积/功耗，但需要保证功能不变
• ECO 修改：后期手工修改网表，需要确认修改符合预期
• 综合后等价检查：验证综合工具没有改变设计行为（LEC - Logic Equivalence Checking）
• 设计优化验证：插入时钟门控、电源门控后验证等价性

映射策略

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

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

不等价结果分析

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

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