Formality：设置Automated Setup Mode模式
相关阅读
Formalityhttps://blog.csdn.net/weixin_45791458/category_12841971.html?spm=1001.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命令命令通常包含有关状态优化的非限定信息，如果某些状态编码未被使用，它们在综合时将被视为不关心(don't 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（参考设计中指不关心(don't 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 box |
| set constant |
| set constraint |
| set cutpoint |
| set dont verify points |
| none |
| all |
注意：用户不应在预验证（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"驱动下降沿）和无锁存器时钟门控，其中被门控的时钟会保持在边沿之前的值，例如en&clk驱动上升沿时，!en|clk驱动下降沿）。 |
| high | 考虑无锁存器时钟门控，其中被门控的时钟会保持在边沿之后的值（例如en&clk驱动下降沿时，!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的等价性检查，不应该开启自动设置模式。