数字芯片设计中的 Simulation、Formal Verification、Verification、Emulation、Prototype Validation 与 Nightly Regression

本文全部依据 Cadence ASK 技术文档整理。文中的“工作流关系”和“适用场景”是对这些文档的归纳，引用均来自 ask.cadence.com。

一、整体工作流

数字芯片验证可以理解为一个由验证计划驱动、多种执行引擎共同提供证据、再通过回归和覆盖率分析完成收敛的过程。

flowchart TD
    VP["Verification Plan / vPlan<br/>验证目标、功能点、覆盖率目标"]

    VP --> SIM["Simulation<br/>Xcelium"]
    VP --> FV["Formal Verification<br/>Jasper"]
    VP --> EMU["Emulation<br/>Palladium Z3"]
    VP --> PROTO["FPGA Prototyping / Prototype Validation<br/>Protium X3"]

    SIM --> RM["Regression Management<br/>Verisium Manager"]
    FV --> RM
    EMU --> RM
    PROTO --> RM

    RM --> COV["Coverage、失败分析、进度评估"]
    COV --> VP

其中：

Verification 是覆盖整个项目的验证活动，包括验证计划、测试平台、断言、测试用例、覆盖率、回归、失败分析和验证收敛。
Simulation、Formal Verification、Emulation、FPGA Prototyping 是产生验证证据的不同执行方式。
Regression 是批量、重复执行测试并持续判断设计质量的组织方式。
vPlan 与覆盖率 用来判断验证目标是否完成，而不仅是判断某一次测试是否通过。

Cadence 的多引擎覆盖率流程可以把 Xcelium 仿真、Jasper formal 和 Palladium emulation 的覆盖率结果合并，并映射到统一的层次化验证计划中。Cadence ASK：Multi-Engine Coverage

二、六类工作场景对照

工作场景	主要任务	主要输入	主要输出	Cadence 工具
Simulation	按时间和事件执行 RTL 与 testbench	RTL、testbench、激励、seed	日志、波形、断言结果、覆盖率	Xcelium
Formal Verification	数学化证明属性，或寻找反例	RTL、formal property、约束	proven、counterexample、bounded、unknown 等	Jasper
Verification	按验证计划构建激励、检查和覆盖率体系	vPlan、UVM testbench、assertion、testcase	功能结果、覆盖率、缺陷和验证进度	Xcelium、Jasper、vManager 等
Emulation	在专用硬件平台上高速运行大规模设计	可综合 DUT、testbench/软件、外部接口	长时间运行结果、硬件波形、软硬件协同结果	Palladium Z3
Prototype Validation	将设计映射到 FPGA 原型，运行固件、驱动和系统场景	RTL、FPGA 编译结果、软件、物理接口	系统验证结果、软件验证结果、接口测试结果	Protium X3
Nightly Regression	夜间批量运行测试与多个 seed	testlist、配置、seed、资源策略	pass/fail、覆盖率、失败聚类、趋势	Verisium Manager、Xcelium 等

1. Simulation：仿真

1.1 定义

Simulation 是由仿真器按照 HDL 的时间语义和事件调度规则，执行设计模型与 testbench 的过程。

在 Xcelium 流程中，典型阶段包括：

编译 Verilog、SystemVerilog 或 VHDL。
elaboration：建立完整的设计层次、参数和连接关系。
生成可运行的 simulation snapshot。
执行 snapshot。
输出日志、波形、断言和覆盖率数据。

Xcelium 使用统一仿真内核，将编译代码仿真与事件驱动仿真结合。常用入口为 xrun；对应的底层工具包括 xmvlog、xmvhdl、xmelab 和 xmsim。仿真可以生成 SHM、VCD 等波形数据。Cadence ASK：Introduction to the Xcelium Simulator

1.2 Simulation run 是什么

一次 simulation run 通常由以下内容共同决定：

Design版本
+ Testbench版本
+ Testcase
+ 编译/运行参数
+ 配置
+ Random Seed
= 一次可识别、可复现的仿真运行

同一个 testcase 使用不同 seed 执行，会形成不同的随机化激励路径，因此通常被视为不同的 run。

1.3 Simulation 适合的工作

RTL 功能调试。
UVM testbench 开发。
时序和协议行为检查。
assertion 执行。
波形观察。
功能覆盖率和代码覆盖率采集。
针对具体 testcase 和 seed 的问题复现。

2. Formal Verification：形式验证

2.1 定义

Formal Verification 使用数学方法分析设计的全部可能状态和输入组合。验证人员描述需要满足的 property，并为环境建立必要约束；formal engine 随后尝试证明 property，或者生成能够违反 property 的 counterexample。

Jasper 平台包含通用 Formal Property Verification，也包括连接性、寄存器等面向特定问题的自动化应用。部分应用能够自动生成 formal property。Cadence 将其描述为可以进行 exhaustive verification，并且不要求传统仿真 testbench。Cadence ASK：Jasper Platform and Formal Property Verification App User Guide

2.2 Formal 的组成

一个 formal 验证任务通常包含：

DUT：需要验证的 RTL。
Property：需要证明或覆盖的设计性质。
Constraint：对合法输入和环境行为的限制。
Clock/Reset 定义：建立设计运行条件。
Proof configuration：proof engine、深度、资源和运行策略。
Proof result：证明结果及对应证据。

2.3 Jasper 的结果状态

Jasper 将运行状态和 property 的有效性结果分开表示。

运行过程可能处于：

unprocessed
queued
processing
processed

property 结果可能包括：

结果	含义
Proven	property 已完成证明
Covered	cover property 已找到满足路径
Counterexample / CEX	找到违反 property 的执行路径
Unreachable	cover 目标不可达
Bounded Proven	在当前分析边界内成立
Undetermined	当前资源或方法尚未得到最终结论
Unknown	尚无确定结果
Error	分析过程出现错误

Jasper 还提供 vacuity 相关指示，用于识别前提不可达或约束过强等情况。Cadence ASK：Proof Run and Validity Status Indicators

2.4 Formal 适合的工作

控制逻辑和状态机性质证明。
FIFO 不溢出、不下溢等安全属性。
仲裁器互斥、公平性等属性。
连接性和寄存器验证。
低概率、深状态问题分析。
仿真难以覆盖的状态空间分析。

Formal 的重点是 property、环境约束和证明完整性。它通常不以随机 seed 作为探索状态空间的核心机制。

3. Verification：验证体系与 Xcelium/UVM 动态验证

3.1 定义

Verification 是确认设计是否满足功能规格和验证目标的完整工程活动。它覆盖：

Verification Plan。
testbench 架构。
testcase 和 sequence。
constrained-random stimulus。
assertion。
scoreboard 和 checker。
functional coverage。
code coverage。
regression。
failure triage。
coverage closure。

Xcelium 是执行动态验证的重要仿真引擎；UVM 是组织 SystemVerilog 验证环境的标准方法之一。

3.2 UVM 验证环境

Cadence 的 UVM 文档将 UVC 分为 interface、module 和 system 等层级。典型 UVM agent 包含：

Sequencer：调度 sequence 和 transaction。
Driver/BFM：把 transaction 转换为引脚或接口行为。
Monitor：被动采集接口活动。
Coverage collector：统计功能覆盖率。
Checker/Scoreboard：比较实际结果和预期结果。
Virtual sequencer：协调多个 interface agent。

Agent 可以工作在 active 或 passive 模式。System UVC 可以包含 virtual sequencer 和 scoreboard。Sequence 表示一系列 data item，也就是 transaction 流。Cadence ASK：UVC Architecture

3.3 Test、Testcase、Sequence 和 Transaction

术语	作用
Testlist	一批需要执行的 testcase 及其配置
Test/Testcase	某个具体验证目标的运行入口
Sequence	按一定策略产生的一串 transaction
Transaction / Sequence Item	一次抽象协议操作或数据项
Driver	将 transaction 驱动到 DUT 接口
Monitor	观察 DUT 接口行为
Scoreboard	比较实际结果和参考结果
Coverage	统计验证空间中已经到达的部分

4. Seed：随机种子

4.1 Seed 的定义

Seed 是随机数生成器的初始化值。相同的设计、testbench、配置和 seed 通常用于复现相同的随机激励过程。

Xcelium SystemVerilog 随机化支持：

-svseed <number>
-svseed random

如果没有指定 -svseed，默认值为 1。Testbench 可以调用 $get_initial_random_seed() 读取当前仿真使用的初始 seed。-svseed 会覆盖全局 -seed 对 SystemVerilog 随机化的设置。Cadence ASK：Setting Randomization Seeds

4.2 为什么一个 testcase 要运行多个 seed

Constrained-random testcase 描述的是一组约束和生成规则。不同 seed 会让随机求解器产生不同的合法 transaction、时序和组合，因此可以探索更多状态空间。

例如：

testcase = cache_random_test
seed = 1001  → 运行 A
seed = 1002  → 运行 B
seed = 1003  → 运行 C

三个 run 使用同一个 testcase，但可能产生不同的地址、数据、延迟、并发关系和协议交错。

4.3 Seed 与复现

完整复现信息通常包括：

RTL/Testbench版本
Testcase名称
Seed
编译参数
运行参数
配置文件
工具版本
运行环境

失败报告中保存 seed，可以针对同一随机路径重新运行，并打开更详细的日志、断言或波形。

4.4 Verisium Manager 中的 seed

Verisium Manager 的 sv_seed 属性支持：

单个 seed。
seed 列表。
seed 范围。
random。
gen_random。
positive_gen_random。

vManager 会把 seed 导出到 BRUN_SV_SEED。运行脚本需要显式地将其传给 Xcelium，例如：

xrun -svseed $BRUN_SV_SEED ...

sv_seed、count 和 repetitions 会共同影响最终生成的 run 数量。文档同时说明：vManager 属性可以产生 32 位或 64 位 seed，而 Xcelium 的 -svseed 接受 32 位值；传入不符合要求的值时，Xcelium 会给出警告并使用默认 seed 1。Cadence ASK：Test and Group Container Attributes—sv_seed

5. Emulation：Palladium Z3

5.1 定义

Emulation 将可综合设计映射到专用验证硬件平台，在比软件 RTL 仿真更高的执行性能下运行设计。

Palladium Z3 是 Cadence 的 verification computing platform，支持 Software Acceleration 和 In-Circuit Emulation 等工作流。Cadence ASK：Overview of Palladium

5.2 In-Circuit Emulation

在 ICE 流程中：

可综合设计整体运行在 Palladium 上。
可以连接实际或虚拟 target system。
使用 xeCompile 编译设计。
使用 xeDebug 运行和调试。
支持静态和动态 target。
支持 STB、LA、VD 等运行模式。

这类场景适合协议接口、外部设备交互以及长时间系统运行。

5.3 Software Acceleration

在 Software Acceleration 流程中：

可综合 DUT 运行在 Palladium 硬件上。
非综合或行为级 testbench 运行在主机上的 Xcelium 中。
DUT 与 testbench 之间通过加速接口通信。
编译流程可以使用 IXCOM 或 xrun。

这种分工保留了仿真 testbench 的灵活性，同时让 DUT 获得硬件加速。

5.4 调试能力

Palladium 提供：

dynamic probes。
FullVision。
InfiniTrace。
hardware waveform。
触发与信号追踪。
长时间运行中的问题定位。

5.5 典型应用

大规模 SoC 验证。
操作系统启动。
Firmware 和 driver 验证。
长时间协议流量。
软件与硬件协同验证。
仿真运行时间较长的系统级场景。

6. Prototype Validation：Protium X3

6.1 定义

Protium X3 是基于 FPGA 的原型验证平台。设计 RTL 会被编译、分区并映射到一个或多个 FPGA 中，随后以硬件原型的形式运行。

Protium X3 使用 AMD Versal Premium VP1902 FPGA，可用于 SoC/ASIC 硬件验证、固件开发和软件开发。系统由工作站控制，并支持虚拟接口和物理接口。Cadence ASK：Introduction to the Protium X3 System

6.2 原型构建流程

典型流程为：

RTL
  ↓
编译与综合
  ↓
多 FPGA 分区
  ↓
Placement / Routing
  ↓
生成每颗 FPGA 的 bit file
  ↓
下载到 Protium
  ↓
运行固件、驱动、应用软件和系统测试

Protium 支持对 RTL 信号进行观察、调试和追踪，也支持对模型化存储器进行 backdoor read/write。Cadence ASK：Overview of Protium System

6.3 Prototype Validation 的重点

在接近实际硬件的执行环境中运行设计。
提前启动 firmware、driver、bootloader 和操作系统开发。
验证高速接口与外围设备。
运行较长的软件 workload。
进行系统性能和软硬件集成验证。
支持远程软件调试。

Protium X3 SpeedBridge Adapter 支持最多四个 High-Density SpeedBridge 连接，并可提供 UART、JTAG 等 DUT 与外部调试器之间的连接。Cadence ASK：Protium X3 SpeedBridge Adapter Overview

6.4 Palladium Z3 与 Protium X3 的工作关系

维度	Palladium Z3	Protium X3
平台类型	专用 verification computing / emulation 平台	FPGA-based prototyping 平台
主要阶段	硬件验证、软硬件协同验证	原型验证、软件开发、系统验证
调试重点	深度硬件可见性、波形、触发和 trace	FPGA 原型运行、接口连接、软件调试
Testbench	支持 ICE 和 Software Acceleration	侧重在 FPGA 原型上运行系统与软件
典型负载	验证场景、长时间硬件运行、OS boot	firmware、driver、OS、应用 workload
编译结果	Palladium 可执行映射	每颗 FPGA 对应的 bit file

Cadence 文档说明 Protium 与 Palladium Z2/Z3、SpeedBridge 兼容，可以把 emulation 环境进一步迁移到快速 FPGA prototype 环境。Cadence ASK：Overview of Protium System

7. Nightly Regression：夜间回归

7.1 Regression 的定义

Regression 是按照一个 testlist 批量执行 testcase，并汇总 pass/fail、覆盖率和失败信息的过程。

Verisium SimAI 文档把 regression 描述为面向特定目的组织的 testlist，例如：

check-in regression。
nightly regression。
weekly regression。
bug hunting。
coverage closure。

这些 regression 可以包含相同或重叠的 testcase，主要差异之一是每个 testcase 分配的权重，也就是运行多少个 seed。Cadence ASK：Introduction to Verisium SimAI

7.2 Nightly Regression 的典型过程

flowchart LR
    A["准备 nightly testlist"] --> B["展开 testcase、配置和 seed"]
    B --> C["提交到计算资源"]
    C --> D["执行多个 simulation runs"]
    D --> E["收集日志与覆盖率"]
    E --> F["识别 pass / fail"]
    F --> G["失败聚类与 rerun"]
    G --> H["覆盖率和趋势分析"]

7.3 Session、Run 与 Regression

Verisium Manager 的组织关系为：

Regression
└── 一个或多个 Session
    └── 一个或多个 Run
        ├── Passed
        └── Failed

Regression Portal 可以查看 session、run 和相关信息。Cadence ASK：Regression Portal

7.4 Verisium Manager 的作用

Verisium Manager 可以：

管理包含数千个 run 的 session。
通过分布式资源管理系统提交运行。
收集和分析日志。
对失败进行筛选和分组。
重新执行 failed tests。
分析覆盖率和其他验证指标。
通过 GUI、命令行或 batch 模式管理验证任务。
使用 RCL 管理 session 和指标。Cadence ASK：Verisium Manager Overview

7.5 Nightly、Check-in 与 Weekly Regression

类型	典型目标	Test 数量与 seed
Check-in Regression	快速发现新提交引入的基本问题	数量较少、执行时间短、seed 较少
Nightly Regression	每晚检查主要功能和随机场景	更完整的 testlist，每个 testcase 可运行多个 seed
Weekly Regression	更深入的长时间检查和覆盖率增长	更多 testcase、更多 seed、更高资源投入
Bug Hunting	扩大特定问题附近的随机搜索	提高相关 testcase 的 seed 权重
Coverage Closure	填补尚未覆盖的验证目标	根据 coverage hole 调整 testcase 和 seed 分配

表中的组织方式依据 Cadence 对 regression purpose、testlist 和 testcase weight/seed 的定义归纳。Cadence ASK：Introduction to Verisium SimAI

8. Verification Plan：验证计划

8.1 Verification Plan 包含什么

验证计划将设计规格转换为可检查、可度量的验证目标。典型内容包括：

Feature 和 sub-feature。
验证目标。
验证方法。
对应 testcase。
对应 assertion/property。
functional coverage。
code coverage。
目标覆盖率。
负责人和计划状态。
完成标准。

8.2 vPlan 与验证指标的映射

Verisium Manager 支持将 coverage metric 映射到 vPlan element，并支持：

一个指标映射到多个计划项。
多个指标映射到一个计划项。
从 session 加载指标数据。
flexible mapping。
logical-instance mapping。
bin filter。

可映射的指标包括：

block coverage。
statement coverage。
expression coverage。
toggle coverage。
FSM coverage。
assertion coverage。
covergroup coverage。
testcase metric。Cadence ASK：Mapping Metrics to vPlan Items

8.3 vPlan Grade

Verisium Manager 可以计算：

overall grade。
goal-relative grade。
completion grade。
planned element 状态。
section 加权结果。

文档列出的 grade 来源包括 block、branch、statement、expression、toggle、FSM、covergroup、assertion 和 testcase 等指标。每个目标可以设置 0 到 100 的 goal，再根据实际结果评估完成程度。Cadence ASK：vPlan Grading

9. Coverage：验证进度的度量

9.1 Code Coverage

Code coverage 描述 RTL 结构的执行情况，例如：

block。
statement。
branch。
expression。
toggle。
FSM state/transition/arc。

它反映设计代码是否被执行或激活。

9.2 Functional Coverage

Functional coverage 描述验证计划定义的功能场景是否到达，常见形式包括：

covergroup。
coverpoint。
cross coverage。
assertion coverage。
testcase metric。

它用于衡量规格定义的功能空间。

9.3 多引擎覆盖率

Cadence 的多引擎覆盖率流程能够把以下结果纳入统一分析：

Xcelium Simulation Coverage
+ Jasper Formal Coverage
+ Palladium Emulation Coverage
= 映射到统一 vPlan 的验证进度

这样可以从验证目标角度观察不同验证引擎共同提供的结果。Cadence ASK：Multi-Engine Coverage

10. 工具选择速查

需要完成的任务	推荐工作方式	Cadence 工具
查看 RTL 在具体激励下的波形	Simulation	Xcelium
运行 UVM testcase	Dynamic Verification / Simulation	Xcelium
使用多个随机 seed 扩大场景覆盖	Regression + Simulation	Verisium Manager + Xcelium
证明 property 对所有合法状态成立	Formal Verification	Jasper
获取违反 property 的反例	Formal Verification	Jasper
运行大规模 SoC 和长时间系统场景	Emulation	Palladium Z3
将行为 testbench 与硬件 DUT 协同运行	Software Acceleration	Xcelium + Palladium
提前启动 firmware、driver 和 OS	FPGA Prototyping	Protium X3
连接 JTAG、UART 或实际外围设备	Prototype Validation	Protium X3 + SpeedBridge
管理 nightly regression	Regression Management	Verisium Manager
统一查看 simulation、formal 和 emulation 覆盖率	Multi-Engine Coverage	Verisium Manager/vPlan
判断验证计划是否完成	vPlan Grading / Coverage Closure	Verisium Manager

11. 术语理解

Simulation：让 RTL 和 testbench 在仿真器中按时间与事件规则运行。
Formal Verification：让证明引擎探索状态空间，对 property 给出证明或反例。
Verification：用计划、激励、检查、覆盖率和回归确认设计符合规格。
Emulation：把大规模设计放到专用验证硬件上高速运行。
Prototype Validation：把设计实现到 FPGA 原型上，运行软件并连接系统接口。
Nightly Regression：每天夜间批量运行 testcase 和多个 seed，持续监控质量与覆盖率。
Seed：决定随机激励生成路径的初始值，也是随机失败复现的重要标识。
Verification Plan：把规格拆解为验证目标，并将 testcase、property 和 coverage 映射到这些目标。
Coverage Closure：根据尚未完成的验证目标，继续补充测试、seed、property 或其他验证活动，直至达到计划目标。

Cadence Simulation、Formal Verification、Verification、Emulation、Prototype Validation 与 Nightly Regression 综述