VC Formal 支持哪些应用模式

Synopsys VC Formal™ 提供了多种 APP（应用模式），针对不同的验证需求进行优化，以提高形式验证的效率和覆盖率。以下是 VC Formal 支持的主要 APPs 及其用途：

1. VC Formal Apps 概览

VC Formal 的 APPs 是预定义的验证策略，针对特定场景优化引擎配置，使形式验证更高效。主要分为以下几类：

APP 名称	主要用途	适用场景
Equivalence (LEC)	RTL-to-RTL 或 RTL-to-netlist 逻辑等价性检查	设计优化、ECO 验证
Safety	硬件安全验证（如信息流跟踪、侧信道攻击检测）	安全关键型芯片（汽车、航天、加密模块）
Connectivity	检查模块间的连接性（如寄存器传输、总线协议）	SoC 集成验证
Control Logic	验证控制逻辑（如状态机、仲裁逻辑）	控制器、FSM 验证
Datapath	数据路径验证（如算术单元、AI 加速器）	乘法器、DSP、AI 硬件验证
Memory	存储器相关验证（如读写一致性、ECC 逻辑）	SRAM/寄存器文件验证
Clock Domain Crossing (CDC)	时钟域交叉验证（同步器逻辑、亚稳态风险）	多时钟域设计
Reset	复位逻辑验证（复位释放顺序、复位毛刺检测）	复杂复位网络验证
Fusion	结合形式验证与仿真（Hybrid Formal-Simulation）	提高覆盖率，验证复杂场景

2. 关键 APPs 详解

(1) Equivalence (LEC)

功能：验证两个设计版本（如 RTL 优化前后、RTL vs. 门级网表）的逻辑等价性。
对比 Formality：
- VC Formal 的 LEC 更灵活（支持 RTL-to-RTL），但 Formality 在门级网表 LEC 上更成熟。
适用场景：
- 算法优化后的 RTL 一致性检查。
- ECO 修改的快速验证。

(2) Safety

功能：验证硬件安全属性（如无非法信息泄漏、权限隔离）。
支持标准：
- ISO 26262（汽车功能安全）、Common Criteria（信息安全）。
典型检查项：
- 敏感数据是否被隔离？
- 是否存在硬件后门？

(3) Datapath

功能：针对算术逻辑（如乘法器、加法器、浮点单元）的自动形式验证。
优势：
- 自动抽象数据位宽，避免状态爆炸。
- 支持符号计算（Symbolic Simulation）。

(4) CDC (Clock Domain Crossing)

功能：验证跨时钟域同步逻辑的正确性。
输出报告：
- 亚稳态风险、同步器缺失、握手协议错误。

(5) Fusion (Hybrid Formal-Simulation)

功能：结合形式验证与仿真，验证复杂场景（如深状态空间问题）。
工作流程：
1. 用仿真生成初始激励。
2. 用形式验证扩展覆盖边界条件。

3. 如何选择 APPs？

RTL 功能验证 → Control Logic + Datapath + Connectivity。
安全芯片 → Safety + Reset + Memory。
多时钟域设计 → CDC + Equivalence。
AI 加速器 → Datapath + Fusion。

4. 与其他工具的协同

与 SpyGlass 结合：用 SpyGlass 做 CDC 静态检查，再用 VC Formal 的 CDC APP 深度验证。
与 Formality 结合：VC Formal 做早期 RTL 等价性检查，Formality 做后端 LEC。
与 VCS 仿真结合：通过 Fusion APP 实现形式化-仿真混合验证。

5. 示例命令（VC Formal 启动 APP）

# 启动 Datapath APP 验证乘法器
read_verilog mult.v
set_app_mode datapath
check_property -expr "a * b == p_out"# 启动 Safety APP 检查信息流
set_app_mode safety
check_security -property "no_unauthorized_access"