VC Formal

常用命令

约束复位期间信号的值，通过fvassume及其配合命令实现的方法：

1. 使用-env参数声明环境全局约束（Environment Constraints）

如果您希望约束在**复位仿真期间（Reset Phase）和正式分析阶段（Formal Analysis Phase）**同时生效，可以使用-env选项。sva中的assume，只作用于Formal Analysis Phase。

• 关键时序：必须在执行sim_run（复位仿真）命令之前发布fvassume -env命令，否则该约束在复位期间不会生效，只会应用于正式分析阶段。
• 对象限制：信号表达式仅限于主输入（primary inputs）、未驱动的网线（undriven nets）、剪切点（snip points）或黑盒输出（black box outputs）。
• 语法限制：表达式必须是常数、等式或简单的组合逻辑蕴含，不能包含复杂的时序操作符，不支持不等式。
• 示例：

  # 必须在 sim_run 之前配置 fvassume -env -expr {vld_status == 1} # 随后进行复位仿真并保存 sim_run 10 sim_save_reset

2. 结合sim_force约束“复位与正式阶段值不同”的信号

在实际验证中，很多信号在复位期间（例如处于复位激活态）需要为特定值，而在正式分析（Functional）阶段需要切换为另一个值。此时推荐将sim_force与fvassume结合使用：

• 工作机制：在复位计算时使用sim_force强行赋予复位值，在保存复位状态（sim_save_reset）后，再用fvassume约束其在正式分析时的值。
• 示例（假设输入SSE在复位期间需为 1，正式分析阶段需为 0）：

  sim_force SSE -apply 1 # ... 进行复位仿真 sim_run sim_save_reset # 复位结束后，使用 fvassume 约束正式分析时的值（此值会覆盖前面的 force） fvassume sse0 -expr {SSE == 0}

3. 使用-depth约束复位后前 N 个周期的值

如果您需要在复位仿真结束、正式分析刚刚开始的前 \(N\) 个时钟周期内对信号进行特定约束（例如约束状态机处于初始态），可以使用-depth选项。

• 示例（在复位后的前三个时钟周期约束state为2'b0）：

  fvassume -expr { state == 2'b0 } -depth 3

• 注意：-depth绑定的表达式必须是纯组合逻辑表达式，且与-env、-stable等参数互斥。

4. 在 SVA 代码中编写initial assume（初始安全假设）

您也可以直接在 SystemVerilog 源代码中编写伴随initial块的并发属性假设。在 VC Formal 中，该假设的评估起点是复位过程完成后的第一个时钟沿。

• 示例（约束复位仿真结束后的前 3 个时钟周期a为 1，之后永远为 0）：

  initial Asm: assume property(@(posedge clk) a #=# always !a);

dump复位阶段波形

在 VC Formal 中，要在使用fvtrace时自动 dump 复位阶段（复位前及复位期间）的波形，或者生成包含复位和正式分析阶段的完整波形（Composite Trace）：

1. 开启复位周期追踪开关

在执行验证（check_fv）之前，必须在 Tcl 中开启允许追踪复位周期的配置：

fv_config -enable_trace_reset_cycles true

该参数默认值为false，开启后工具会在 formal trace 生成时包含复位周期的激励。

2. 确保复位波形记录与混合追踪开启

确保以下变量和仿真配置处于开启状态（默认通常为开启）：

# 开启混合 trace 生成（默认值为 true） set_app_var fml_composite_trace true # 确保复位波形生成未被关闭 sim_config -rst_wave ON

3. 使用fvtrace导出

根据您的调试需求，选择以下一种导出方式：

• 方式 A：仅导出复位阶段的波形

  fvtrace -reset

• 方式 B：导出“复位 + 属性反例”的完整混合波形（Composite Trace）由于默认不直接支持-composite选项，您需要在启动 VC Formal 之前在 Linux Shell 中设置环境变量：

  # 在启动 vcf 前设置环境变量 setenv SNPS_VCST_DISABLE_VF 1

  然后在 vcf 的 Tcl 中运行：

  fvtrace -composite <property_name>

自动 Dump

支持自动dump falsified property波形：

# 1. 开启波形导出模式 set_app_var fml_mode_on true #set_app_var enable_verdi_debug true #set_app_var verdi_export_dir "./my_saved_waves" # 2. 运行验证 check_fv -block # 3. 自动遍历并导出所有失败断言的波形 foreach_in_collection prop [get_props -status falsified] { set prop_name [get_attribute $prop name] ;# 修正：使用 name 属性 fvtrace -property $prop_name }

复位

在 VC Formal 中，不能简单地将软复位和硬复位都一刀切地当作普通复位（即都使用create_reset）来处理。是否需要区分，完全取决于您的验证意图。

这与 VC Formal 对复位信号的底层处理机制密切相关：

1. 核心机制：create_reset会在正式分析中“锁死”信号

当您对一个信号使用create_reset命令时，VC Formal 会自动执行以下双重操作：

1. 在复位仿真阶段（Reset Phase）：将该信号强制驱动为活跃值（Active Value）以建立初始状态。
2. 在正式分析阶段（Formal Analysis Phase）：自动将该信号永久保持在不活跃值（Inactive Value）。

这样做的目的是防止复位信号在正式验证期间随机复位，从而导致断言因前提不满足而发生空成功（Vacuous Pass），或者因设计不断被复位而无法测出深层逻辑。

2. 软复位与硬复位的具体处理方案

根据您的验证目标，建议采取以下不同的建模方式：

方案 A：如果您想验证“软复位被动态触发后的系统恢复行为”

如果您希望 Formal 引擎去探索“在系统运行过程中，突然给一个软复位，系统能否正常清零/恢复工作”的场景：

• 做法：千万不要对软复位信号使用create_reset。
• 原因：一旦使用了create_reset，该软复位在正式分析阶段就会被工具锁死在无效状态，Formal 引擎将永远无法尝试“在运行中拉起软复位”的边界场景。
• 正确配置：
  1. 在复位仿真阶段（sim_run期间），使用sim_force将软复位初始化为无效值（或先有效再无效的顺序序列），然后用sim_save_reset保存初始状态。
  2. 在正式分析阶段，将软复位信号作为普通输入，允许 Formal 引擎自由（随机）驱动它。
  3. 为了防止软复位无限拉起，使用fvassume约束其行为。例如限制它一次最多持续 1 个周期，或者在特定状态下才能拉起：

     // 限制软复位不能连续有效超过 1 个周期 soft_rst_limit: assume property (@(posedge clk) soft_rst |=> !soft_rst);

方案 B：如果您只想让软复位在初始化时生效， functional 阶段不希望它起作用

如果您认为软复位在 functional 验证中不应该被随意触发（或者您目前只想专注于验证常态工作下的业务逻辑）：

• 做法：此时您可以将软复位和硬复位同样对待。
• 正确配置：直接对它们分别声明create_reset：

  create_reset rst_n -sense low ;# 系统硬复位 create_reset soft_rst_n -sense low ;# 软件局部复位

  在复位仿真时，工具会同时将它们拉为有效值以初始化寄存器；进入正式分析后，两者都会被自动锁定在无效值（常态1），确保系统不会发生意外复位。

方案 C：混合使用（硬复位用于初始化，软复位在 functional 阶段用作约束常数）

如果软复位在 functional 阶段需要保持固定的无效值，但您不想用create_reset（例如该信号是内部寄存器，不支持环境约束的要求）：

• 做法：使用sim_force配合set_constant。
• 正确配置：

  # 复位仿真期间强制软复位为 1 参与初始化 sim_force soft_rst -apply 1 sim_run 10 sim_save_reset # 仿真结束后，在正式分析阶段将其锁死为 0 set_constant soft_rst -apply 0

总结

• 硬复位（系统复位）：必须用create_reset。
• 软复位（局部/软件复位）：
  • 如果不希望它在验证中随机乱跳 \(\rightarrow\) 一并用create_reset。
  • 如果需要验证软复位下电恢复/ CDC 行为 \(\rightarrow\)不要用create_reset，改用sim_force进行复位期初始化，并在 functional 阶段用fvassume限制其触发条件。

在 VC Formal 中，sim_run是内置仿真器（Built-in Simulator）的核心命令，用于在正式分析开始前通过模拟时钟和复位激励来建立并确定设计的初始复位状态。

以下是其详细用法以及sim_run -stable与sim_run 10的区别。

1.sim_run的标准用法

在仿真复位流程中，初始化是一个两步法过程：

1. 设置初始值：使用create_clock、create_reset、sim_force（强行约束输入） 或sim_set_state等命令配置复位期间的行为和信号值。
2. 运行仿真并保存：执行sim_run命令驱动仿真器运行，随后必须使用sim_save_reset命令将此时仿真模型的寄存器状态加载并保存为 Formal 模型的初始状态。

常用语法选项：

• 运行固定周期：sim_run <cycles>（例如sim_run 10运行 10 个参考时钟周期）。
• 运行至稳定：sim_run -stable。
• 使用复位向量文件：sim_run -file <reset_seq.txt>（通过读取外部文本文件提供的信号变化序列和延迟来驱动复位仿真）。
• 指定驱动时钟：sim_run <cycles> -clk <clock_name>（显式指定用哪个时钟来驱动，默认使用参考时钟）。

2.sim_run -stable与sim_run 10（即您所指的-10）的区别

sim_run -stable（运行至设计稳定）

• 工作机制：仿真器会一直运行，直到设计中所有时序逻辑/寄存器的值都达到稳定状态（即无论后面再运行多少个时钟周期，它们的值都不会再发生任何改变）。
• 异常处理：如果您的设计中存在组合反馈环路（Combinational Loops）或振荡（Oscillation），导致信号无法稳定，VC Formal 会直接报错并中断运行，报告设计中的振荡情况。
• 适用场景：适用于不知道具体复位链需要多少个时钟周期，或者希望系统在复位激活后完全“静止/稳定”下来的标准初始化场景。

sim_run 10（运行精确的 10 个周期）

• 工作机制：仿真器会精确向前运行 10 个参考时钟周期，然后立即停止，不管此时设计是否已经达到了稳定状态。
• 适用场景：适用于有明确时序步骤要求的复位。例如，复位信号必须保持至少 8 个周期，第 10 个周期释放复位并进行采样。

sim_save_reset可以配合使用fv_sim_report来校验复位仿真结束后，特定控制寄存器是否被正确初始化为了非 X 值。

vacuity

在 VC Formal（vcf）中，当断言（Assertion）或约束（Assumption）的前件（Antecedent，即|->或|=>的左侧条件）永远无法满足时，该属性就会被判定为空成功（Vacuous Proof），其主状态会显示为VACUOUS。

这通常意味着环境存在过约束（Over-constraint）或 RTL 设计、断言定义存在逻辑漏洞。在 VC Formal 中，定位和调试 vacuity 问题通常遵循以下四个核心步骤：

第一步：找出哪些属性发生了空成功（Vacuity）

1. 文本命令行定位： 在运行check_fv之后，使用以下命令过滤出所有空成功的断言：

   vcf> report_fv -status vacuous -verbose

   或者直接生成单行简要报告，查找带(vacuous)标记的属性：

   vcf> report_fv -list -no_summary

2. GUI 界面（GoalList）定位： 打开 Verdi GUI，在VCF:GoalList窗口中，检查vacuity列。
   • 如果该列显示为红色的叉号（X），则表示该属性为VACUOUS，说明前件从未被触发。

第二步：分析是否因环境“过约束”导致空成功（首选排查）

前件无法触发最常见的原因是其他fvassume约束过于严苛，把前件所需的输入空间给堵死了。

1. 使用compute_reduced_constraints命令： 该命令可以自动找出是哪些约束（Assumptions）影响了该属性的前件，并计算出导致其空成功的最小约束子集：

   vcf> compute_reduced_constraints -subtype vacuity -prop <failing_property_name> vcf> report_reduced_constraints -subtype vacuity -property <failing_property_name>

2. GUI 快捷操作： 在 GoalList 窗口中，右键点击状态为VACUOUS的属性，在弹出的右键菜单中选择"Show Reduced Constraints for Vacuity"。
   • 结果解读：
     • 如果工具在终端或 VCF Console 窗口中输出了特定的假设（Assumptions）列表，说明正是这些假设导致了过约束，您需要放宽或修正这些约束。
     • 如果工具报告[Info] No constraints were used...，说明没有任何外部约束影响它，问题出在 RTL 设计内部逻辑或断言自身的定义上。

第三步：分析是否因 RTL 设计或断言定义错误导致空成功

如果排除了外部约束问题，说明在 RTL 硬件逻辑中（或者断言定义中），前件的信号组合在物理上就是不可能实现的。

1. 使用compute_formal_core（Formal Core）分析： 通过计算 Formal Core（形式化核心），可以抓取在证明前件不可达时，到底涉及了 RTL 中的哪些寄存器和输入信号：

   vcf> compute_formal_core -property <property_name> -subtype vacuity -block vcf> report_formal_core -subtype vacuity -property <property_name> -verbose

2. GUI 快捷操作： 在 GoalList 窗口中右键点击该属性，选择"Compute Formal Core"。在弹出的对话框中，将 SubType 勾选为"Vacuity(Selection Only)"，点击 OK。
   • 结果解读： 在弹出的VCF:FormalCore窗口中，展开Complement Formal Core类别，您会清晰地看到涉及的Registers和Inputs（这些寄存器或输入变量的逻辑设计直接导致了前件的“死端状态”）。点击其名字可直接在代码窗口中高亮定位。

第四步：将 Vacuity 显式转换为 Cover 属性进行调试（辅助手段）

如果您觉得隐式的 vacuity 属性不直观，可以通过配置变量，让工具为前件自动生成显式的cover属性：

# 在执行 check_fv 之前，将该变量设为 true vcf> set_fml_var fv_create_vacuity_cover_properties true

• 效果：工具会自动创建名为${original_property_name}_vacuity的显式 cover 属性。
• 调试方法：在跑完验证后，这个属性的状态必然会是uncoverable。由于它变成了标准的 cover 属性，您可以使用针对 cover 属性的所有调试命令（如compute_reduced_constraints来查看哪些约束导致其无法被 cover）来进行无缝定位。