常用命令约束复位期间信号的值通过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_reset2. 结合sim_force约束“复位与正式阶段值不同”的信号在实际验证中很多信号在复位期间例如处于复位激活态需要为特定值而在正式分析Functional阶段需要切换为另一个值。此时推荐将sim_force与fvassume结合使用工作机制在复位计算时使用sim_force强行赋予复位值在保存复位状态sim_save_reset后再用fvassume约束其在正式分析时的值。示例假设输入SSE在复位期间需为 1正式分析阶段需为 0sim_force SSE -apply 1 # ... 进行复位仿真 sim_run sim_save_reset # 复位结束后使用 fvassume 约束正式分析时的值此值会覆盖前面的 force fvassume sse0 -expr {SSE 0}3. 使用-depth约束复位后前 N 个周期的值如果您需要在复位仿真结束、正式分析刚刚开始的前 \(N\) 个时钟周期内对信号进行特定约束例如约束状态机处于初始态可以使用-depth选项。示例在复位后的前三个时钟周期约束state为2b0fvassume -expr { state 2b0 } -depth 3注意-depth绑定的表达式必须是纯组合逻辑表达式且与-env、-stable等参数互斥。4. 在 SVA 代码中编写initial assume初始安全假设您也可以直接在 SystemVerilog 源代码中编写伴随initial块的并发属性假设。在 VC Formal 中该假设的评估起点是复位过程完成后的第一个时钟沿。示例约束复位仿真结束后的前 3 个时钟周期a为 1之后永远为 0initial Asm: assume property((posedge clk) a ## always !a);dump复位阶段波形在 VC Formal 中要在使用fvtrace时自动 dump 复位阶段复位前及复位期间的波形或者生成包含复位和正式分析阶段的完整波形Composite Trace1. 开启复位周期追踪开关在执行验证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 ON3. 使用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 会自动执行以下双重操作在复位仿真阶段Reset Phase将该信号强制驱动为活跃值Active Value以建立初始状态。在正式分析阶段Formal Analysis Phase自动将该信号永久保持在不活跃值Inactive Value。这样做的目的是防止复位信号在正式验证期间随机复位从而导致断言因前提不满足而发生空成功Vacuous Pass或者因设计不断被复位而无法测出深层逻辑。2. 软复位与硬复位的具体处理方案根据您的验证目标建议采取以下不同的建模方式方案 A如果您想验证“软复位被动态触发后的系统恢复行为”如果您希望 Formal 引擎去探索“在系统运行过程中突然给一个软复位系统能否正常清零/恢复工作”的场景做法千万不要对软复位信号使用create_reset。原因一旦使用了create_reset该软复位在正式分析阶段就会被工具锁死在无效状态Formal 引擎将永远无法尝试“在运行中拉起软复位”的边界场景。正确配置在复位仿真阶段sim_run期间使用sim_force将软复位初始化为无效值或先有效再无效的顺序序列然后用sim_save_reset保存初始状态。在正式分析阶段将软复位信号作为普通输入允许 Formal 引擎自由随机驱动它。为了防止软复位无限拉起使用fvassume约束其行为。例如限制它一次最多持续 1 个周期或者在特定状态下才能拉起// 限制软复位不能连续有效超过 1 个周期 soft_rst_limit: assume property ((posedge clk) soft_rst | !soft_rst);方案 B如果您只想让软复位在初始化时生效 functional 阶段不希望它起作用如果您认为软复位在 functional 验证中不应该被随意触发或者您目前只想专注于验证常态工作下的业务逻辑做法此时您可以将软复位和硬复位同样对待。正确配置直接对它们分别声明create_resetcreate_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的标准用法在仿真复位流程中初始化是一个两步法过程设置初始值使用create_clock、create_reset、sim_force强行约束输入 或sim_set_state等命令配置复位期间的行为和信号值。运行仿真并保存执行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 Formalvcf中当断言Assertion或约束Assumption的前件Antecedent即|-或|的左侧条件永远无法满足时该属性就会被判定为空成功Vacuous Proof其主状态会显示为VACUOUS。这通常意味着环境存在过约束Over-constraint或 RTL 设计、断言定义存在逻辑漏洞。在 VC Formal 中定位和调试 vacuity 问题通常遵循以下四个核心步骤第一步找出哪些属性发生了空成功Vacuity文本命令行定位 在运行check_fv之后使用以下命令过滤出所有空成功的断言vcf report_fv -status vacuous -verbose或者直接生成单行简要报告查找带(vacuous)标记的属性vcf report_fv -list -no_summaryGUI 界面GoalList定位 打开 Verdi GUI在VCF:GoalList窗口中检查vacuity列。如果该列显示为红色的叉号X则表示该属性为VACUOUS说明前件从未被触发。第二步分析是否因环境“过约束”导致空成功首选排查前件无法触发最常见的原因是其他fvassume约束过于严苛把前件所需的输入空间给堵死了。使用compute_reduced_constraints命令 该命令可以自动找出是哪些约束Assumptions影响了该属性的前件并计算出导致其空成功的最小约束子集vcf compute_reduced_constraints -subtype vacuity -prop failing_property_name vcf report_reduced_constraints -subtype vacuity -property failing_property_nameGUI 快捷操作 在 GoalList 窗口中右键点击状态为VACUOUS的属性在弹出的右键菜单中选择Show Reduced Constraints for Vacuity。结果解读如果工具在终端或 VCF Console 窗口中输出了特定的假设Assumptions列表说明正是这些假设导致了过约束您需要放宽或修正这些约束。如果工具报告[Info] No constraints were used...说明没有任何外部约束影响它问题出在 RTL 设计内部逻辑或断言自身的定义上。第三步分析是否因 RTL 设计或断言定义错误导致空成功如果排除了外部约束问题说明在 RTL 硬件逻辑中或者断言定义中前件的信号组合在物理上就是不可能实现的。使用compute_formal_coreFormal Core分析 通过计算 Formal Core形式化核心可以抓取在证明前件不可达时到底涉及了 RTL 中的哪些寄存器和输入信号vcf compute_formal_core -property property_name -subtype vacuity -block vcf report_formal_core -subtype vacuity -property property_name -verboseGUI 快捷操作 在 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来进行无缝定位。