第六章vManager 集成

概述

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

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

版本兼容

从 2017.09 版本开始，JasperGold 与 UCIS Library 的兼容机制允许它从仿真器安装中动态继承 coverage library——也就是说，JasperGold 端不需要执行任何命令来设置版本。

选择用于动态链接的 libucis 时，按以下优先级设置：

VM Server Web 页面中的 simulator 设置
环境变量 MDV_XLM_HOME 指向的仿真器
环境 path 中的 irun
环境 path 中的 xrun

如果以上都无法定位到 libucis，就选用 JasperGold 包自带的库。最终链接了哪个库会在终端上报告出来。

Server 模式下设置 Coverage Library 版本

要在 vManager 中查看 formal metrics，需要配置兼容的仿真器版本。这件事在 vManager 的 Web 界面里做，不在 JasperGold 里做：

打开浏览器，地址栏输入 https://<server host>:<server port>/vmgr（例如 https://jgperf01:8080/vmgr/）
在认证界面输入用户名和密码，点击 Submit
进入 Web 界面后，点击 Administration 链接进入 vManager 的管理门户，在其中配置仿真器版本

对齐仿真和形式指标

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

Supported Use Models

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

集成流程

Standalone Flow

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

Integrated vManager Flow

vManager 直接调度 JasperGold 运行。

在 vManager 中查看形式验证结果：Assertions 视图按 Formal Average Grade 与 Formal Status Grade 显示各断言

VSIF 文件

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

关键属性

属性	用途
`run_mode`	运行模式，四选一：`batch` / `batch_debug`（默认） / `interactive` / `interactive_debug`。详见下表
`jg_app`	指定启动哪个 App（fpv/cdc/sec...）
`jg_cmd_args`	传递给 JasperGold 的命令行参数
`jg_tasks`	要运行的任务列表
`jg_cov_exclude`	排除的覆盖率项
`jg_data_merge`	决定合并后的 formal 结果取 `stimuli`、`proof`，或两者的组合

run_mode 的四个取值

这个属性在 VSIF 中定义，用于访问 JasperGold Visualize 窗口。默认值是 batch_debug，它允许你用图形和波形视图调试。run 脚本会自动把 run_mode 设置翻译成以 GUI 还是 batch 模式启动 Jasper，并同时设置 database –init_unicov 命令的 coverage 和 waveform 选项。