第六章vManager 集成

概述

vManager 是 Cadence 的验证管理平台，可以管理仿真和形式验证的回归运行。JasperGold 与 vManager 集成，实现：

• 统一的回归管理
• 形式和仿真覆盖率合并
• 验证计划追踪（vPlan）

版本兼容

需要确保 JasperGold 和 vManager 版本兼容，正确设置 Coverage Library 版本。

环境设置

# JasperGold 端设置
set_vmanager_mode -server <vmanager_host>
set_coverage_library_version <version>

# vManager 端配置
# 指定 jg_app, jg_cmd_args, jg_tasks 等

对齐仿真和形式指标

vManager 可以将形式证明结果（proven/failed/covered）与仿真覆盖率数据合并到统一的验证数据库中。

Supported Use Models

• Formal Metrics：纯形式验证指标
• Combined Formal + Simulation Metrics：形式+仿真联合指标

集成流程

Standalone Flow

JasperGold 独立运行，将结果导入 vManager。

Integrated vManager Flow

vManager 直接调度 JasperGold 运行。

VSIF 文件

Verification Session Input Format (VSIF) 文件定义 vManager 如何运行 JasperGold：

关键属性

分析功能

• Analyzing Formal Properties：形式属性状态分析
• Analyzing Metrics：Formal/Simulation/Combined 指标
• Analyzing Verification Plans：vPlan 完成度追踪
• Required Proof Bound：要求的证明边界
• Verification Aspect：验证方面分类

vManager 集成界面

vManager 集成方法论

vManager 在验证流程中的角色

vManager 是 Cadence 的验证管理平台，整合仿真和形式验证的结果：

• 统一管理仿真回归和形式验证的 metrics
• VSIF（Verification Simulation Input Format）描述验证计划
• 追踪验证进度（哪些功能已验证、哪些 pending）
• 覆盖率整合（仿真覆盖率 + 形式覆盖率合并）

JasperGold 与 vManager 集成

• JasperGold 证明结果（proven/failed/covered）自动上传到 vManager
• 形式验证覆盖的功能在 vManager 的 vPlan 中标记为已覆盖
• CI 流程中：JasperGold 批处理脚本 → 结果上传 vManager → metrics 驱动验证 signoff