相关阅读Formalityhttps://blog.csdn.net/weixin_45791458/category_12841971.html?spm1001.2014.3001.5482要使用自动设置模式在加载/执行SVF文件之前需要将synopsys_auto_setup变量布尔值设置为true或者在GUI界面中选择Use Auto Setup如图1所示。当自动设置模式设置后一组Formality变量会被设置一些设置命令会执行以与Synopsys综合工具例如Design Compiler兼容从而通过使用SVF指导文件提高整体工具的设置性能。图1 选择自动设置模式非默认变量设置启用自动设置模式后以下设置将会发生hdlin_error_on_mismatch_message默认值true该变量将被设置为false这会导致随后设计读入时的仿真综合不匹配错误被降级为警告。注意该变量将被set_mismatch_message_filter -warn命令替代因此最新版的Formality同时会执行set_mismatch_message_filter -warn命令。hdlin_ignore_embedded_configuration默认值false该变量将被设置为true这会导致随后设计读入时忽略VHDL文件中的嵌入式配置(embedded configurations)。hdlin_ignore_full_case默认值true该变量将被设置为false会导致随后设计读入时考虑Verilog文件中的full_case综合指令。hdlin_ignore_parallel_case默认值true该变量将被设置为false会导致随后设计读入时考虑Verilog文件中的parallel_case综合指令。signature_analysis_allow_subset_match默认值true该变量将被设置为false会强制匹配阶段的签名分析(signature analysis)时不使用子集匹配方法。svf_ignore_unqualified_fsm_information默认值true如果在之后加载/执行SVF文件时如果其中存在guide_fsm_reencoding命令该变量将被设置为false当被设置为True时表示忽略SVF文件中的guide_fsm_reencoding命令该设置只影响设置后的SVF文件加载/执行。guide_fsm_reencoding命令命令通常包含有关状态优化的非限定信息如果某些状态编码未被使用它们在综合时将被视为不关心(dont cares)进行优化。注意该变量对仅使用部分状态编码的有限状态机有效。对于使用所有可能状态值的状态机不会受到该变量设置的影响。upf_assume_related_supply_default_primary默认值false该变量控制在分析顶层(top-level)和黑盒(blackbox)端口时如何处理缺少显式相关电源(related supplies)定义的情况。默认情况下会在分析源/汇(source/sink)时遇到没有显式相关电源定义的端口时报错。该变量将被设置为true则会假设该端口的驱动/接收电源设置为本地主要电源(local primary supplies)即使没有显式定义相关电源。upf_use_additional_db_attributes默认值false该变量将被设置为true会导致如果一个单元(cell)被标记为时钟门控单元(clock gating cell)、保持单元(retention cell)或包含时序元素如基于锁存的隔离单元那么该单元将不会被保留不受UPF中set_retention策略的影响。如果工具遇到任何实例化的技术库单元包含celldefine definition定义的寄存器并且该寄存器受set_retention控制且没有可用的DB模型那么会产生错误。对于DB宏单元(is_macro_cell : true)将使用宏单元引脚的related_power和related_ground属性来确定相关电源这在实施UPF中的set_isolation -source/-sink/-diff_supply_only时使用。默认情况下将发出警告并将所有时序单元(sequential cells)转换为保留单元(retention cells)。同时它将忽略宏单元的related_power和related_ground属性在插入隔离时不考虑这些属性。verification_set_undriven_signals默认值BINARY:X该变量用于控制验证过程中如何处理无驱动信号undriven nets和pins。默认情况下将参考设计中的无驱动引脚和线网视为BINARY(即Cut-Net)而将实现设计中的无驱动引脚和线网视为x不确定如果参考设计中的任何比较点由无驱动信号控制这种保守的设置会导致验证失败但确保了参考设计的行为不被任何意外的无驱动信号控制。如果要确保参考设计和实现设计比较点的无驱动信号值一致需要将该变量设置为BINARY。如果使用自动设置模式该变量将被设置为SYNTHESIS。可选值取值含义X将无驱动引脚和线网视为x参考设计中指不关心(dont cares)实现设计中指不确定这与仿真保持一致。Z将无驱动引脚和线网视为z高阻态。0将无驱动引脚和线网视为0。1将无驱动引脚和线网视为1。0:X将参考设计中的无驱动引脚和线网视为0而将实现设计中的无驱动引脚和线网视为x确保中无驱动参考信号在实现中绑定为0。BINARY将每个无驱动引脚或线网视为可匹配的独立自由变量通过在每个无驱动信号处创建Cut-Net。如果下游比较点被未匹配的无驱动信号控制这会导致验证失败。BINARY:X默认值。将参考设计中的无驱动引脚和线网视为Cut-Net实现设计中的无驱动引脚和线网视为x。如果任何匹配的参考比较点由无驱动信号控制则会导致验证失败。SYNTHESIS将参考设计中的无驱动引脚和线网视为Design Compiler工具处理的方式实现设计中的无驱动引脚和线网视为Cut-Net。注意 PI值已弃用并将在未来的版本中移除。对于该值Formality会将无驱动引脚和网线视为BINARY。verification_verify_directly_undriven_output默认值true该变量将被设置为false会导致忽略不验证直接无驱动的输出端口。在综合或验证流程中直接无驱动输出端口通常是为了后续流程中插入扫描测试电路。默认情况下会验证直接无驱动的输出端口但验证通常会失败因为直接无驱动端口可能没有驱动信号。hdlin_enable_verilog_configurations_array_n_block默认值false该变量将被设置为true会允许在Verilog配置中使用实例数组和非LRM语言参考标准的语法1、允许在instance clause中使用方括号[]而不需要前置的转义符这不符合LRM因为转移标识符应该有前置的转义符和末尾的空白如Verilog基础简单标识符和转义标识符一文所述如instance top.genblk[0].a liblist alib2、支持instance clause使用实例数组的单元素实例进行配置如instance top.inst_arr[1] liblist alib instance top.inst_arr[2] liblist blib instance top.inst_arr[3] liblist clib其中arr是一个实例数组通过不同的instance clause对其进行配置。对于整个数组的所有元素基于第一个instance top.inst_arr[1] liblist alib进行配置而后续的instance clause则会被忽略。svf_checkpoint_auto_setup_commands默认值空该变量将被设置为all用于控制在验证过程中哪些用户设置会自动与检查点checkpoint共享。默认情况下不会在进行检查点验证时共享任何用户设置只有在明确指定要共享时用户设置才会被共享。可选值取值set black boxset constantset constraintset cutpointset dont verify pointsnoneall注意用户不应在预验证prevalidation之后更改任何已设置的设置。以上的这些非默认变量设置可以在启动自动设置模式后被用户覆盖或者在进行设置前使用synopsys_auto_setup_filter变量。额外的约束如果synopsys_auto_setup变量设置为true并且随后使用set_svf命令加载/执行SVF文件额外的设置外部约束将通过SVF文件传递给Formality这包括guide_environment {{ clock_gating ... }}其中...可以是none、low、high、any和collapse_all_cg_cells。当SVF文件中出现此guide命令时verification_clock_gate_hold_mode变量默认值为none将被设置为...该变量用于指定应如何识别和处理驱动寄存器时钟引脚的时钟门控。它决定了工具在处理时钟门控时是否应用特定的算法来考虑基于锁存器和无锁存器的时钟门控。默认情况下工具不会应用这些算法可能导致验证结果与预期不符。可选值取值含义none不应用时钟门控算法。low考虑基于锁存器的时钟门控例如latch-and驱动上升沿latch-or驱动下降沿和无锁存器时钟门控其中被门控的时钟会保持在边沿之前的值例如enclk驱动上升沿时!en|clk驱动下降沿。high考虑无锁存器时钟门控其中被门控的时钟会保持在边沿之后的值例如enclk驱动下降沿时!en|clk驱动上升沿。any在同一设计中考虑高(high)和低(low)两种时钟门控方式。collapse_all_cg_cells与low相同但还会考虑所有主输出端口和黑盒输入引脚作为寄存器时钟引脚。guide_environment {{ hdlin_dyn_array_bnd_check ... }}其中...可以是Verilog、VHDL、None和Both。当SVF文件中出现此guide命令时hdlin_dyn_array_bnd_check变量默认值为Verilog将被设置为...该变量指定是否为设计添加逻辑以检查数组索引的有效性这确保在写入数组时如果数组索引超出边界时的行为与仿真器一致。可选值取值含义Verilog仅在Verilog文件中生成超出范围索引的检查逻辑。VHDL仅在VHDL文件中生成超出范围索引的检查逻辑。None不在任何语言中生成超出范围索引的检查逻辑。Both在Verilog和VHDL文件中都生成超出范围索引的检查逻辑。guide_port_constant当SVF文件中出现此命令时代表着参考设计的输入端口将被设置为常量值该命令类似set_constant命令但在guide阶段使用而set_constant命令在setup阶段使用。guide_port_constant -design design_name -value 0 | 1 | X -ports { port_name ... } -pins { pin_name ... }使用该命令将synopsys_auto_setup以及svf_port_constant变量设置为true否则工具会忽略此命令在SVF命令处理时即preverify阶段被rejected。guide_scan_input当SVF文件中出现此命令时代表着参考设计的某些端口将被设置为常量值从而禁用扫描电路通常在扫描电路被插入或扫描链被重新排序时使用。该命令类似set_constant命令但在guide阶段使用而set_constant命令在setup阶段使用。guide_scan_input -design design_name -disable_value 0 | 1 -ports { port_name ... } -pins { pin_name ... }使用该命令需要将synopsys_auto_setup以及svf_scan变量设置为true否则工具会忽略此命令在guide类命令处理时即preverify阶段被rejected。guide_set_rounding当SVF文件中出现此命令时将为参考设计的乘法器指定初始的舍入信息用于指定施加到乘法器的内部和外部舍入修正。通过设置舍入位置可以控制乘法器结果的精度适用于需要控制计算精度的设计。guide_set_rounding -design designName -cells cellName -rounding { ExtPos [ IntPos ] }写在最后自动设置模式是为了RTL与Netlist的等价性检查设计的因此对于Netlist与Netlist的等价性检查不应该开启自动设置模式。