首页/资讯中心/详情

Formality：使用机器学习驱动的分布式处理(DPX)

Formality：使用机器学习驱动的分布式处理(DPX)
📅 发布时间：2026/7/24 22:02:00

相关阅读

Formalityhttps://blog.csdn.net/weixin_45791458/category_12841971.html?spm=1001.2014.3001.5482

DPX流程简介

Formality分布式处理(Distributed Processing, DPX)是Formality在2020版本推出的一个扩展功能。DPX特性基于通用分布式处理库(Common Distributed Processing Library, CDPL)框架，该框架也被Synopsys的许多其他工具所采用，可用的配置选项与其他基于CDPL的工具类似，有关 CDPL的详细说明，请参阅SolvNetPlus提供的 《Common DP Library User Guide》。该技术就像是原本的多核技术（使用set_host_options命令）的进一步拓展，DPX将使用计算集群。

DPX流程通过以下方式缩短等价性检查的运行时间：

  • 将任务进行分布式并行化处理
  • 对每个划分后的任务分区采用多个验证策略(Solver Strategies)并行尝试

这种方式既提高了获得确定性结果（即非 Inconclusive）的概率，也缩短了整体运行时间。

为了使用Formality DPX，需要至少一个Formality-DPX License，用户可以直接购买2024版本推出的Formality Elite产品包，其中包含了Formality、Formality-DPX和Formality-LP三个License。

与标准的Formality等价性检查方案相比，DPX流程能够同时并行验证更多的分区，如图1所示。

图1 Flow资源对比

DPX Manager（即用户直接交互的主Formality进程）会保存一个会话文件，其中包含整个设计空间以及验证上下文。每个工作节点(Worker)都会读取该会话文件，并接受来自DPX Manager的任务。这些任务由一组指令组成，用于采用特定的验证策略对某个分区执行验证，如图2所示。

图2 DPX的分区

策略是求解器设置的一种特定组合，具体介绍可见Formality：验证困难(Inconclusive)的三种解决方法。每个CPU核心可以执行一个任务，因此一个拥有多个CPU核心的工作节点可以并行执行多个任务。当某个任务完成后，它会将验证结果报告给DPX Manager。在某些情况下，任务还会在部分结果可用时，提前将这些部分结果返回给DPX Manager。

DPX流程可应用于Formality的以下两个阶段：

  • Verify阶段：工具在此阶段判断两个设计在逻辑上是否等价。
  • Preverify阶段（即处理SVF时）：用于对检查点(Checkpoints)执行预验证（包括设计类检查点和非设计类检查点）。

要启用分布式处理，可使用set_dpx_options命令。该命令不仅用于启用DPX流程，还用于配置分布式处理环境，包括计算集群类型、任务提交方式以及工作节点的资源分配等。例如：

fm_shell (setup)> set_dpx_options \ -protocol SGE \ -submit_command "qsub -P bnormal -l minslotcpu=4 -l minslotmem=30G" \ -max_workers 8 \ -max_cores 4

set_dpx_options命令各选项的含义如下：

-protocol：用于指定DPX使用的计算集群协议，如SGE、LSF、PBS等。

-submit_command：用于指定访问集群资源所使用的任务提交命令，应使用双引号或花括号括起来。

-max_workers：用于指定启动的工作节点数量（默认值为8），每个工作节点通常运行在一台独立的机器上，工作节点本质上是一个独立的Formality进程。

-max_cores：用于指定每个工作节点可并行执行的任务数量（默认值为1），相当于在工作节进程中使用set_host_options -max_cores命令。DPX Manager将设计划分为多个分区，每个分区的验证对应一个任务，工作节点可同时处理多个任务。

-max_memory（2022版本新增）：用于指定每个工作节点可使用的最大内存(GB)。该值表示节点内所有并行任务占用内存的总和（共享内存仅计算一次）。当内存使用达到上限时，DPX Manager会停止部分任务，并相应减少该工作节点的并行任务数量，使内存消耗恢复到限制范围内。默认值为负数，表示不限制内存使用。

-hosts：用于指定一个兼容CDPL的主机配置文件，可替代-protocol和-submit_command两个选项，用于描述整个分布式处理环境。

在DPX流程中，DPX Manager负责将待验证设计划分为多个分区，并将这些验证任务分配给各个工作节点执行。DPX Manager与工作节点可以运行在不同的机器上，通过-max_workers选项控制工作节点数量，通过-max_cores选项控制每个工作节点的并行处理能力，从而实现设计验证任务的高效分布式执行。

每个Formality-DPX License（或者说Formality Elite产品包）最多允许同时运行32个并行任务。并行任务总数由工作节点数量与每个工作节点使用的CPU核心数（对应并行任务数）的乘积决定，即：

并行任务数 = DPX max_workers × DPX max_cores

例如，下面几种命令配置都指定了32个并行任务，因此只需要一个Formality-DPX License。

fm_shell (setup)> set_dpx_options -max_workers 8 -max_cores 4 ... fm_shell (setup)> set_dpx_options -max_workers 16 -max_cores 2 ... fm_shell (setup)> set_dpx_options -max_workers 32 -max_cores 1 ...

注意：为了充分利用License资源，建议将并行任务数配置为32的整数倍。

例如，如果配置为6个工作节点、每个工作节点使用4个CPU核心，则总共运行24个并行任务。虽然工具仍然会占用一个完整的Formality-DPX License，但该License最多可以支持32个并行任务，因此还有8个任务容量没有得到利用。相比之下，若配置为8个工作节点、每个工作节点使用4个CPU核心，即可运行32个并行任务，能够充分利用同一License。

再例如，如果配置为10个工作节点、每个工作节点使用4个CPU核心，则共有40个并行任务。由于一个License最多支持32个任务，因此需要占用2个License。然而，第二个License实际上只承担了额外的8个任务，其余24个任务容量处于闲置状态，因此这种配置的License利用率较低。

配置DPX

允许Preverify阶段的DPX

默认情况下，DPX不仅会应用于验证阶段，还会默认应用于SVF文件中guide checkpoints的预验证。如果不希望在非设计类的检查点验证中使用DPX，可将dpx_enable_checkpoint_verification变量设置为false（默认值为true）。

如果希望DPX用于设计类的检查点验证，请将dpx_enable_dbc_verification变量设置为true（默认值为false），该变量于2023版本引入。

上面两个变量的设置必须在预验证阶段开始之前完成。

提交到计算集群或本地机器

对于将任务提交到计算集群或本地机器的情况，可使用-protocol选项和-submit_command选项：

fm_shell (setup)> set_dpx_options \ -protocol SGE \ -submit_command "qsub -P bnormal -l minslotcpu=4 -l minslotmem=30G" \ -max_workers 8 \ -max_cores 4

其中，-protocol选项用于指定计算集群类型，或者在不使用计算集群时用于访问计算主机的方法。CDPL根据-protocol选项的设置，自动选择相应的命令集，用于查询和终止作业。目前支持以下协议：

  • RSH（远程shell）
  • SSH（安全shell）
  • SH（本地主机）
  • SGE（最初为Sun Grid Engine，后来发展为Univa Grid Engine）
  • LSF（Load Sharing Facility，由Platform Computing提供）
  • PBS（Portable Batch System）
  • RTDA（Runtime Design Automation Network Computer）
  • NB（Netbatch Compute Farm）
  • SLURM（Simple Linux Utility for Resource Management）
  • AWSBATCH（AWS Batch）
  • CUSTOM（CDPL未知的用户自定义集群类型）

上述所有协议均受到CDPL的直接支持，其中CUSTOM表示一种CDPL本身不认识的集群类型。CUSTOM协议允许将任务提交到CDPL不支持的其他计算集群。但是如果使用CUSTOM协议，CDPL不会主动查询或终止作业，这依赖计算集群自身在提交进程结束后完成相应的资源清理工作。

-submit_command选项用于指定在目标运行环境中启动进程所使用的命令字符串。当使用计算集群时，该命令字符串通常高度依赖于具体的集群环境。有关如何向计算集群提交作业，请咨询集群管理员。

需要特别注意的是，应使用集群环境所采用的资源描述方式明确指定工作节点所需的CPU核心数和内存。这些资源需求：不会从DPX Manager自动继承，也不会根据-max_cores选项和max_memory选项自动推导。如果没有正确声明资源需求，计算集群管理系统可能会认为当前作业实际占用的资源超过了申请的资源，从而将其标记为资源超额使用。

下面给出了几个使用-protocol选项和-submit_command选项的典型示例：

fm_shell (setup)> set_dpx_options \ -protocol SGE \ -submit_command "qsub -P bnormal -l minslotcpu=4 -l minslotmem=30G" \ -max_workers 8 \ -max_cores 4
fm_shell (setup)> set_dpx_options \ -protocol SGE \ -submit_command "qsub -P batch -pe mt 4 -l mem_free=30G" \ -max_workers 8 \ -max_cores 4
fm_shell (setup)> set_dpx_options \ -protocol RTDA \ -submit_command "nc run -e SNAPSHOT -r+ CPUS/4 -r+ RAM/30000" \ -max_workers 8 \ -max_cores 4
fm_shell (setup)> set_dpx_options \ -protocol LSF \ -submit_command {bsub -q batch -n 4 -R "rusage[mem=30G]"} \ -max_workers 8 \ -max_cores 4

注意：工作节点必须继承主Formality进程的全部环境变量和运行环境设置。大多数计算集群默认都会继承这些环境设置，但是对于RTDA集群，需要在nc run命令中添加-e SNAPSHOT选项；对于某些SGE集群，需要在qsub命令中添加-v选项。

如果计算集群支持作业优先级功能，建议设置比普通作业更高的优先级。这样可以减少DPX Manager等待工作节点启动的时间。例如，在SGE集群中，可以在qsub命令中加入-js 100选项，其中100表示在SGE集群中的优先级。

提交到特定机器

若要将作业提交到指定的某个机器或一组机器，可使用-hosts选项，使用该选项可以指定CDPL主机配置文件，如下所示。

fm_shell (setup)> set_dpx_options -hosts my.cdpl -max_workers 8 -max_cores 4

该文件可用于以下场景：

1、多个用户或多个项目共享同一套计算集群配置。所有用户均可指向同一个配置文件，多个Synopsys工具也可以共用同一个配置文件。

2、在使用SSH或RSH协议时，指定具体使用哪些机器，文件中的每一行定义一台可作为计算资源的机器。

主机配置文件采用ASCII文本格式，允许使用单行注释，注释必须以#开头，文件中的每一行均采用如下格式：

<Flag>|<Hostname>|<Slots>|<tmpDir>|<Protocol>|<Command>

各字段的含义如下表所示。

字段类型说明
FLag整数0或10表示该主机不可使用；1表示该主机可作为工作节点使用。
Hostname合法字符串（主机名）对于RSH和SSH协议，填写有效工作节点的主机名；对于其他协议，该字段留空。
Slots整数表示该主机（或集群）可提供的工作节点槽位(Slot)数量。-1表示槽位数量不限，当槽位不限时，CDPL会根据任务需要创建任意数量的工作节点。
tmpDir字符串工作节点上的一个可写临时目录。
Protocol字符串用于连接工作节点的通信协议。
Command字符串实际用于连接工作节点的命令。

下面展示了几个主机配置文件的示例。

// 采用RSH架构、包含两台主机、共提供10个工作节点槽位 // 其中，一台主机提供4个工作节点槽位(slot)，另一台主机提供6个工作节点槽位 # host file for RSH 1|engr_lab-x9|4|/remote/users/tmp |RSH| rsh 1|engr_lab-x2|6|/remote/users/tmp |RSH| rsh
// 采用SSH架构、包含两台主机、共提供12个工作节点槽位 // RSH和SSH环境要求能够免密码登录 # host file for SSH 1|engr_lab-x15|4|/remote/users/tmp |SSH| ssh 1|engr_lab-x21|8|/remote/users/tmp |SSH| ssh
// SGE计算集群 // 对于SGE计算集群，主机名字段为空 # host file for SGE 1| |-1| |SGE| qsub -cwd -V -P bnormal -l mem_free=1G
// 将启动的作业数量限制为3的SGE计算集群 # host file for SGE 1| |3| |SGE| qsub -cwd -V -js 100 -P bnormal arch=glinux

测试和报告DPX配置

要快速测试DPX配置是否正确，请执行以下步骤：

1、启动Formality，此时无需读取任何设计文件。

2、使用set_dpx_options命令配置DPX选项，然后执行check_dpx_options命令。该命令会检查set_dpx_options命令的各项参数是否适用于当前运行环境，从而验证工作节点是否能够成功启动并获取，下面展示了一个例子：

fm_shell (setup)> set_dpx_options \ -protocol SGE \ -submit_command "qsub -P bnormal -l minslotcpu= -l minslotmem=30G" \ -max_workers 4 \ -max_cores 4 fm_shell (setup)> check_dpx_options Info: License check for DPX verification successful. Adding Host "SGE" Info: Starting 1 worker. Each worker can process 4 tasks at a time. Starting DPX worker: /path/FM_DPX_WORK/crew/C2 Checking for live worker... ........ No live worker seen in the past 2 minutes ........ No live worker seen in the past 4 minutes ....... Info: 1 live worker detected. Stopping DPX worker set_dpx_options is working properly in your environment

执行该命令时，工具会按照用户通过set_dpx_options命令指定的配置启动一个工作节点。该工作节点仅向DPX Manager报告自身已成功启动，然后立即退出，不会执行实际的验证任务。

首次在新的计算环境中使用分布式处理时，应使用check_dpx_options命令测试set_dpx_options命令的配置。如果该命令未能成功完成，则不要使用当前set_dpx_options命令中的配置去尝试完整的分布式验证，因为这些配置无法正常工作。此时，应查明失败原因，并调整set_dpx_options命令中指定的选项，或者在不启用分布式处理的情况下运行Formality。

若要查看当前Formality中所有由用户指定并生效的DPX配置，可使用report_dpx_options命令，如下所示：

fm_shell (setup)> report_dpx_options ************************************************** Report : dpx_options Reference : <None> Implementation : <None> Version : S-2021.06 Date : Thu Apr 15 15:23:48 2021 ************************************************** Communication protocol or grid type : SGE Worker submit command : qsub -P bnormal -l minslotcpu= -l minslotmem=30G Max concurrent workers : 8 Max cores available per worker : 4

另一种调试DPX配置的方法是在Formality外部，直接在UNIX Shell中执行提交命令。可以在提交命令末尾添加xterm程序并运行该命令，以验证提交命令本身是否能够正常工作。例如，假设要使用如下set_dpx_options命令：

fm_shell (setup)> set_dpx_options -protocol SGE \ -submit_command "qsub -P bnormal -l minslotcpu= -l minslotmem=30G" \ -max_workers 4 \ -max_cores 4

则可以先在UNIX Shell中执行：

%> qsub -P bnormal -l minslotcpu= -l minslotmem=30G xterm

如果配置正确，该命令应会启动一个xterm窗口。如果无法启动，则说明问题不在Formality，而是在集群环境或作业提交配置上，此时应联系IT部门协助排查集群作业提交环境。

当确认提交命令能够正常工作后，去掉命令末尾的xterm，将其余部分作为set_dpx_options命令的-submit_command选项即可。

使用remove_dpx_options命令可以关闭分布式验证。

管理工作节点

提前启动工作节点

当DPX Manager需要时（例如在verify阶段），会启动工作节点。有时，计算集群从提交工作节点请求到真正的分配之间可能存在一定的延迟。

为了减少这种延迟，可以使用start_dpx_workers命令在真正需要工作节点之前提前申请工作节点，如下所示：

fm_shell (setup)> set_dpx_options -protocol SGE \ -submit_command "qsub -P bnormal -l minslotcpu= -l minslotmem=30G" \ -max_workers 8 -max_cores 4 fm_shell (setup)> start_dpx_workers Info: Starting 8 workers. Each worker can process 4 tasks at a time. Starting DPX workers: /u/testcase_path/FM_DPX_WORK/crew/C1 fm_shell (setup)> match fm_shell (setup)> verify

该命令为非阻塞命令，即向系统发出启动工作节点请求后立即返回，而不会等待工作节点完成启动并进入可接受任务的状态。因此，命令返回时，工作节点可能仍在启动过程中。可以使用get_dpx_workers命令查看当前已经成功启动并可用的工作节点数量。

需要注意的是，提前启动工作节点意味着它们会在真正开始执行任务之前一直处于空闲状态，这可能不符合某些计算集群的资源使用策略，因此应根据实际情况决定是否采用这种方式。

通常，在使用start_dpx_workers命令时，也建议将dpx_keep_workers_alive变量设置为true，使工作节点在整个验证会话期间保持存活，而不会在每个DPX阶段结束后自动释放。工作节点将一直保持运行，直到验证会话结束，或者用户显式执行stop_dpx_workers命令将其释放。

停止工作节点

stop_dpx_workers命令用于关闭并释放当前正在使用的所有分布式处理工作节点，同时取消那些尚未被计算集群分配的工作节点请求。

下面的示例展示了stop_dpx_workers命令的使用方法：

fm_shell (setup)> get_dpx_workers chin213:4 rock075:4 white073:4 black104:4 fm_shell (setup)> stop_dpx_workers Stopping DPX workers fm_shell (setup)> get_dpx_workers fm_shell (setup)>

查询工作节点

get_dpx_workers命令返回一个Tcl列表，其中包含已经获取并已准备好接受任务的分布式处理工作节点。

列表中的每个工作节点都采用<hostname>:<cores>的格式表示，其中<hostname>是运行该工作节点的计算主机名称，<cores>是该工作节点使用的CPU核心数。当未获取到任何工作节点时，get_dpx_workers命令返回一个空列表。

在某些情况下，用户可能希望等待至少一定数量的工作节点准备就绪后，再开始执行分布式验证。例如，当计算集群正在分配资源、部分工作节点尚未启动完成时，可以通过该命令周期性地检查工作节点状态，待达到预期数量后再启动验证，以获得更好的并行处理效率。

报告工作节点状态

report_dpx_workers命令用于报告当前工作节点的状态（该命令于2023版本引入）。报告内容包括用户请求、已启动、等待中、运行中以及已终止的工作节点总数。下面的示例说明了report_dpx_workers命令的使用方法：

fm_shell (setup)> report_dpx_workers ************************************************** Report : dpx_workers Reference : r:/WORK/top Implementation : i:/WORK/top Version : V-2023.12 Date : Tue Nov 7 11:00:10 2023 ************************************************** Workers requested by user : 2 Workers started : 2 Workers running : 2 Workers pending : 0 Workers terminated : 0 Workers are running on machines: dccaeg306:1 sofegm122:1

保持工作节点存活

默认情况下，DPX Manager会在一个分布式处理阶段结束后继续保持工作节点存活，而不会立即释放它们，直到验证会话结束或用户显式执行stop_dpx_workers命令。这样可以避免在后续分布式处理阶段重新申请工作节点，从而减少由于计算集群资源分配耗时较长带来的启动延迟，提高整体验证效率。

分布式处理可能会在同一验证会话的多个阶段被使用，例如预验证阶段和正式验证阶段。对于资源分配延迟较大的计算集群，保持工作节点持续存活可以使后续阶段直接复用已有工作节点，而无需重新等待计算资源分配。

dpx_keep_workers_alive变量用于控制工作节点在空闲时是否保持存活（默认值为true）。当该变量保持默认值时，工作节点会在各个分布式处理阶段之间一直保持运行，即使暂时没有任务需要执行，也不会被释放。

另一方面，不同分布式处理阶段之间也可能存在较长时间的非分布式处理过程，此时工作节点将一直处于空闲状态，占用计算集群资源。如果将dpx_keep_workers_alive设置为false，DPX Manager会在每个分布式处理阶段结束后自动释放所有工作节点，使计算资源能够及时归还给计算集群，供其他用户或任务使用。当后续再次进入分布式处理阶段时，DPX Manager会重新申请并启动新的工作节点，因此可能需要再次等待计算资源分配。

管理工作节点获取超时

若要指定preverify、match和verify命令等待第一个工作节点获取成功并准备好接受分布式任务的最长实际经过时间（即wall clock时间），可以使用dpx_worker_acquisition_timeout变量（默认值为0）。执行这些命令时，Formality会等待至少一个工作节点启动并进入可接受分布式任务的状态。如果在dpx_worker_acquisition_timeout变量指定的时间内仍未获取到任何工作节点，则preverify、match和verify命令将停止执行；否则，将继续正常运行直至完成。默认情况下，该变量不限制等待时间，即会无限期等待工作节点。达到指定的时间限制后，工具将中断当前验证过程。小时和分钟必须输入正整数；若不希望设置时间限制，可将该变量设置为none、0或0:0:0。该变量既可以指定为整数，也可以采用hours:minutes:seconds的格式，例如0:0:60表示等待60秒，而单独指定60则表示等待60小时。

控制验证策略

一个分布式验证任务由一个待验证的分区和一种要运行的验证策略共同组成。同一个分区可以采用多种不同的验证策略同时进行验证，每一种策略（或策略组合）都对应一个独立的分布式验证任务。当某个任务成功完成该分区的验证后，或者说得到确定性结果（即非 Inconclusive），DPX Manager会立即终止该分区上采用其他验证策略运行的任务，从而释放对应的工作节点，以便执行其他尚未完成的验证任务。

dpx_verification_strategies变量的默认值为空。此时，Formality会自动选择一组适用于分布式验证的验证策略及其策略组合（首先是none策略）。用户也可以通过设置dpx_verification_strategies变量，自定义分布式处理过程中使用的验证策略及其组合，例如：

fm_shell (setup)> set_app_var dpx_verification_strategies \ {none s4 {s1 s4} s3 {s3 s8}}

其中，最外层花括号表示整个策略列表，内层花括号表示一个策略组合，即多个验证策略组合后共同执行；特殊策略none表示串行验证使用的默认验证策略。

dpx_verification_strategies变量还控制这些策略的部署顺序。DPX Manager会按照策略列表中的顺序依次尝试各个策略（即创建使用该策略的任务并运行），因此，如果已知某些验证策略对当前设计具有更好的验证效果，建议将这些策略放在列表前面，以便优先执行。如果完成列表中所有指定策略后仍存在未验证点，Formality会继续尝试其他验证策略，以进一步完成验证。

如果将verification_alternate_strategy变量（默认值为none）设置为某个验证策略，则无论dpx_verification_strategies中策略的排列顺序如何，DPX Manager都会将该验证策略作为第二个尝试的策略（这里实测只有dpx_verification_strategies为空才生效，疑似为bug）。

机器学习策略预测

当dpx_enable_ml_strategy_prediction变量设置为true时（默认值为false），DPX Manager将针对每个分区使用机器学习预测得到的策略集合，而不是默认的静态策略顺序（该变量于2024版本引入），从而提高验证效率。启用该功能后，仅改变DPX选择验证策略的方式，其它所有相关的DPX变量仍按照文档说明正常工作。例如，工作节点数量、并行方式等配置均不会受到影响。

启用该变量还要求系统中已正确安装Synopsys ML Platform。该安装约需8GB磁盘空间，并包含支持基于机器学习进行验证策略预测所需的全部软件包。

安装Synopsys ML Platform步骤如下：

  1. 登录SolvNetPlus。
  2. 进入Synopsys ML Platform页面，并单击最新版本号。
  3. 单击Download Here按钮。

在运行Formality DPX时，需要设置如下环境变量，使其指向Synopsys ML Platform的安装目录：

setenv FM_ML_HOME <Synopsys ML Platform 安装目录>

启用机器学习要求DPX Manager至少使用两个CPU核心，可在Formality DPX运行过程中按如下方式设置：

fm_shell (setup)> set_host_options -max_cores 4 fm_shell (setup)> setenv FM_ML_HOME /home/parent/ml_install_dir fm_shell (setup)> set dpx_enable_ml_strategy_prediction true

如果启用了基于机器学习的策略预测，工具将输出如下信息：

Info: DPX utilizing Machine Learning to determine optimal verification strategies

忽略验证策略

dpx_ignored_strategies变量用于控制某些验证策略及策略组合不参与分布式处理（默认值为空）。如果已知某些策略对当前设计的验证效果较差或几乎没有作用，可以通过该变量将其排除，使其不出现在 DPX 的策略执行列表中，从而避免在这些策略上浪费计算资源。例如：

fm_shell (setup)> set dpx_ignored_strategies {l1 q1}

dpx_ignored_strategies的取值格式与dpx_verification_strategies变量相同，既可以指定单个验证策略，也可以指定策略组合。

DPX状态信息

报告DPX状态

report_dpx_status命令用于报告之前各个DPX阶段的状态，并统计哪些任务对验证成功做出了贡献（该命令于2023版本引入）。

下面的示例展示了report_dpx_status命令的使用方法：

fm_shell > report_dpx_status ************************************************** Report : dpx_status Reference : r:/WORK/top Implementation : i:/WORK/top Version : V-2023.12 Date : Thu Sep 21 14:29:38 2023 ************************************************** == DPX Phase 1 == CONTRIBUTING TASKS Count Elapsed Time Strategy 51 0.15 hours none ---------------------------------- 51 0.15 hours IN TOTAL

下面的示例展示了DPX在运行过程中输出的状态更新信息：

Status: Verifying... Info: Start of DPX Distributed Verification. Info: Starting 8 workers. Each worker can process 4 tasks at a time. Info: Distributed Verification directory: /u/testcase_path/FM_RUN7/FM_DPX_WORK/phase/P1. .............................. 0F/0A/107732P/8225U (92% Verification completed) 04/26/21 12:32 7691MB/1524sec (35.4 hrs until timeout) DPX Status: Workers (8 Active, 0 Pending), Tasks (32 Active, 90 Complete)

每当标准验证状态更新时，Formality都会同时输出DPX状态信息。

对于工作节点，Active表示工作节点已与DPX Manager建立通信，并正在执行相应任务；Pending表示工作节点请求已经提交，但尚未由计算集群分配资源。

对于任务，Active表示正在使用某一种验证策略对某个分区执行验证；Complete表示任务已经完成验证，或者已按照工作节点的指示停止执行。

注意：在验证接近结束时，处于Active状态的任务数量可能会少于理论上能够同时运行的最大任务数。这是因为剩余待验证的分区或可尝试的验证策略数量已经不足，无法充分利用全部可用的任务资源。

工作节点延迟

工作节点延迟是指从请求工作节点开始，到工作节点真正可用之间所经历的时间。理想情况下，该延迟应为零，但实际延迟取决于计算集群的响应速度。

下面的信息展示了当前获取工作节点时的延迟情况：

.............................. 0F/0A/129P/564U (18% Verification completed) 07/19/21 21:15 868MB/73sec (32.0 hrs until timeout) DPX Status: Workers (0 Active, 8 Pending), Tasks (0 Active, 0 Complete) ........ Info: 4 of 8 DPX workers are now available. Worker latency is 251 minutes.

自动保存会话

dpx_auto_session_interval变量（默认值为0:0:0，表示禁用自动保存会话）用于指定分布式计算过程中自动保存会话文件的时间间隔。该变量于 2023 版本引入，采用实际经过时间（即wall clock时间）作为计时依据，而非CPU时间。

该变量的时间格式与verification_timeout_limit变量一致，既可以使用正整数表示小时数，也可以采用hours:minutes:seconds格式。例如，0:30:00表示每30分钟自动保存一次会话，而直接指定30则表示30小时，即等价于30:0:0。

该变量仅在verification_auto_session变量设置为on、always或verify时生效。当达到指定的时间间隔后，Formality会自动保存当前会话文件，以便在任务中断或异常退出后恢复验证。但需要注意的是，工具始终只保留最近一次自动保存的会话文件，新的自动保存会覆盖之前生成的自动保存会话文件。

自动导出验证点状态

dpx_auto_status变量（默认值为5000，表示每个文件中最多写出的验证点数量）用于将当前比较点的状态写入FM_INFO目录下的一个Tcl文件。记录的状态包括：passing（验证通过）、failing（验证失败）、aborted（验证中止）、unverified（未验证），将其设置为0表示关闭该功能，该变量于2023版本引入。关于比较点验证状态的更多详细信息可以参考下面的博客。

Formality：比较点的验证状态和整体验证状态https://blog.csdn.net/weixin_45791458/article/details/145133977?ops_request_misc=elastic_search_misc&request_id=19a95c9c91b4c5369d63a7c6090dacab&biz_id=0&utm_medium=distribute.pc_search_result.none-task-blog-2~all~ElasticSearch~search_v2-1-145133977-null-null.541^v3^control&utm_term=%E9%AA%8C%E8%AF%81%E7%82%B9&spm=1018.2226.3001.4450生成的Tcl文件名为dpx_status_C#_P#.tcl，其中：C#表示DPX工作组(Crew)编号，P#表示DPX阶段(Phase)编号，下面给出了一个示例。

# PASSING 8 # FAILING 0 # ABORTED 0 # UNVERIFIED 0 # MEMORY 49.11 GB # CPU 81763.7 sec # PASSING set passing_points { cell://i/WORK/top/m1/b1/bo1_reg cell://i/WORK/top/m1/b2/bo1_reg cell://i/WORK/top/m2/b1/bo1_reg cell://i/WORK/top/m2/b2/bo1_reg port://i/WORK/top/o1 port://i/WORK/top/o2 port://i/WORK/top/o3 port://i/WORK/top/o4 } # FAILING set failing_points {} # ABORTED set aborted_points {} # UNVERIFIED set unverified_points {}

DPX的目录结构（以SH协议为例）

Formality将在当前工作目录下创建FM_DPX_WORK目录，其中有crew和phase两个子目录。

crew

crew目录指的是工作组目录，假设用户之前执行了check_dpx_options命令进行测试，则会在其中新建C1子目录，内含W1目录，即一个工作节点；假设用户之前使用-max_workers选项设置的工作节点数量为4，则验证开始时会在其中新建C2子目录，内含W1、W2、W3、W4目录，即4个工作节点。

W*目录中包含FM_RUN目录，其中包含了FM_INFO、FM_WORK等默认创建的子目录以及fm_shell_command.log文件（该文件会记录工作节点的日志文件，可能包含多个任务的记录），如Formality：工具生成的文件一文中所说。

W*目录中还包含run.log文件（即工作节点运行Formality的日志文件，记录直到任务开始执行）、run.sh文件（即Shell执行的脚本，包含了fm_shell命令，其中-max_cores选项为用户之前使用-max_cores选项设置）、start.tcl文件（即fm_shell执行的脚本，通过-f选项指定，其中包含start_dpx_worker_control_loop命令）。

phase

phase目录指的是DPX验证阶段目录，验证开始时会在其中新建P1子目录，以此类推（标号代表验证阶段或者说一次verify命令执行的先后顺序）。

P*目录中包含crew目录，链接到一个工作组目录C*。

P*目录中还包含tasks目录，task目录下包含T1、T2、T3、T4目录，即4个任务（标号代表任务创建的先后顺序），以及setup.tcl文件（任务通用设置文件）。

T*目录中包含init.tcl文件（即任务的初始化脚本，用于设置任务参数、验证策略以及当前分区的验证点）、process.tcl文件（即任务的执行脚本，用于调用verify命令完成当前分区的验证，并在出现超时以外的异常时终止任务并返回错误信息）、task.log文件（即工作节点执行当前验证任务时生成的日志文件，从任务开始执行记录）、task.summary文件（即任务的运行总结，包含开始时间、结束时间、内存消耗、计算主机名称、任务状态（完成SUCCESS或未完成NO_LONGER_NEEDED）、验证策略等信息）、task.result文件（即任务的验证结果，包含当前分区的比较点及其验证结果，如果任务状态为NO_LONGER_NEEDED，则不会生成该文件，且此时task.log文件因被提前终止而内容不完整，也就是看不到最后的“*** DONE PROCESSING TASK ***字段”）。

P*目录中还包含workers目录，workers目录包含init.fss（初始会话文件）、setup.tcl文件（即工作节点通用设置文件，包含restore_session命令）。

P*目录中还包含summary.txt文件，包含DPX配置信息、工作节点等待时长（最大、最小、平均）、工作节点内存消耗（最大、最小、平均）、任务运行时间（最大、最小、平均）、任务内存消耗（最大、最小、平均）、任务CPU利用率（最大、最小、平均）和总体DPX验证阶段分配的任务数量、提前终止的任务数量、比较点状态、总运行时间。

DPX执行流程

1、启动Formality工作节点。fm_shell执行用户启动脚本start.tcl，完成基础运行环境初始化。

2、进入工作节点控制循环。执行start_dpx_worker_control_loop命令，切换至 FM_DPX_WORK/phase/.../workers目录，等待DPX Manager分配验证任务。

3、恢复Worker会话。执行工作节点通用设置文件(setup.tcl)，恢复init.fss会话，配置工作节点运行环境，并关闭无关的显示和功能。run.log文件的记录到此为止。

4、初始化当前任务。切换至对应任务目录，执行任务的初始化脚本(init.tcl)，设置任务编号、分区编号、验证策略，收集当前分区的比较点，并将其设置为本次验证对象。task.log文件的记录从这里开始。

5、执行分区验证。执行任务通用设置文件(setup.tcl)和执行脚本(process.tcl)，调用verify命令开始当前分区验证，并持续输出验证进度、内存占用、CPU时间等运行状态。

6、等待下一任务。当前任务完成（或被终止）后，工作节点输出任务的运行总结(task.summary)和任务的验证结果(task.result)。随后返回控制循环，等待DPX Manager分配新的分区任务或结束运行。

7、当在DPX验证阶段结束后，DPX Manager将会输出DPX验证阶段总结(summary.txt)，并返回总体验证结果。