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 point)，而将实现设计中的无驱动引脚和线网视为x（不确定），如果参考设计中的任何比较点由无驱动信号控制，这种保守的设置会导致验证失败，但确保了参考设计的行为不被任何意外的无驱动信号控制。
• 如果要确保参考设计和实现设计对比点的无驱动信号值一致，需要将该变量设置为BINARY。
• 如果使用自动设置模式，该变量将被设置为SYNTHESIS。

可选值：

X	将无驱动引脚和线网视为x（参考设计中指不关心(don't cares)，实现设计中指不确定，这与仿真保持一致）。
Z	将无驱动引脚和线网视为z（高阻态）。
0	将无驱动引脚和线网视为0。
1	将无驱动引脚和线网视为1。
0:X	将参考设计中的无驱动引脚和线网视为0，而将实现设计中的无驱动引脚和线网视为x（确保中无驱动参考信号在实现中绑定为0）。
BINARY	将每个无驱动引脚或线网视为可匹配的独立自由变量，通过在每个无驱动信号处创建cut point。如果下游比较点被未匹配的无驱动信号控制，这会导致验证失败。
BINARY:X	默认值。将参考设计中的无驱动引脚和线网视为cut point，实现设计中的无驱动引脚和线网视为x。如果任何匹配的参考比较点由无驱动信号控制，则会导致验证失败。
SYNTHESIS	将参考设计中的无驱动引脚和线网视为Design Compiler工具处理的方式，实现设计中的无驱动引脚和线网视为cut point。

        注意： 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 alib

2、支持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，否则工具会忽略此命令（在svf命令处理时，即preverify阶段被rejected）。

guide_set_rounding

        当svf文件中出现此命令时，将为参考设计的乘法器指定初始的舍入信息，用于指定施加到乘法器的内部和外部舍入修正。通过设置舍入位置，可以控制乘法器结果的精度，适用于需要控制计算精度的设计。

guide_set_rounding-design designName-cells cellName-rounding { ExtPos [ IntPos ] }