相关阅读Formalityhttps://blog.csdn.net/weixin_45791458/category_12841971.html?spm1001.2014.3001.5482DPX流程简介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 minslotcpu4 -l minslotmem30G \ -max_workers 8 \ -max_cores 4set_dpx_options命令各选项的含义如下-protocol用于指定DPX使用的计算集群协议如SGE、LSF、PBS等。-submit_command用于指定访问集群资源所使用的任务提交命令应使用双引号或花括号括起来。-max_workers用于指定启动的工作节点数量默认值为8每个工作节点通常运行在一台独立的机器上工作节点本质上是一个独立的Formality进程。-max_cores用于指定每个工作节点可并行执行的任务数量默认值为1相当于在工作节进程中使用set_host_options -max_cores命令。DPX Manager将设计划分为多个分区每个分区的验证对应一个任务工作节点可同时处理多个任务。-max_memory2022版本新增用于指定每个工作节点可使用的最大内存(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 minslotcpu4 -l minslotmem30G \ -max_workers 8 \ -max_cores 4其中-protocol选项用于指定计算集群类型或者在不使用计算集群时用于访问计算主机的方法。CDPL根据-protocol选项的设置自动选择相应的命令集用于查询和终止作业。目前支持以下协议RSH远程shellSSH安全shellSH本地主机SGE最初为Sun Grid Engine后来发展为Univa Grid EngineLSFLoad Sharing Facility由Platform Computing提供PBSPortable Batch SystemRTDARuntime Design Automation Network ComputerNBNetbatch Compute FarmSLURMSimple Linux Utility for Resource ManagementAWSBATCHAWS BatchCUSTOMCDPL未知的用户自定义集群类型上述所有协议均受到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 minslotcpu4 -l minslotmem30G \ -max_workers 8 \ -max_cores 4fm_shell (setup) set_dpx_options \ -protocol SGE \ -submit_command qsub -P batch -pe mt 4 -l mem_free30G \ -max_workers 8 \ -max_cores 4fm_shell (setup) set_dpx_options \ -protocol RTDA \ -submit_command nc run -e SNAPSHOT -r CPUS/4 -r RAM/30000 \ -max_workers 8 \ -max_cores 4fm_shell (setup) set_dpx_options \ -protocol LSF \ -submit_command {bsub -q batch -n 4 -R rusage[mem30G]} \ -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_free1G// 将启动的作业数量限制为3的SGE计算集群 # host file for SGE 1| |3| |SGE| qsub -cwd -V -js 100 -P bnormal archglinux测试和报告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 minslotmem30G \ -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 minslotmem30G 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 minslotmem30G \ -max_workers 4 \ -max_cores 4则可以先在UNIX Shell中执行% qsub -P bnormal -l minslotcpu -l minslotmem30G 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 minslotmem30G \ -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设置为falseDPX 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小时。控制验证策略一个分布式验证任务由一个待验证的分区和一种要运行的验证策略共同组成。同一个分区可以采用多种不同的验证策略同时进行验证每一种策略或策略组合都对应一个独立的分布式验证任务。当某个任务成功完成该分区的验证后或者说得到确定性结果即非 InconclusiveDPX 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时默认值为falseDPX Manager将针对每个分区使用机器学习预测得到的策略集合而不是默认的静态策略顺序该变量于2024版本引入从而提高验证效率。启用该功能后仅改变DPX选择验证策略的方式其它所有相关的DPX变量仍按照文档说明正常工作。例如工作节点数量、并行方式等配置均不会受到影响。启用该变量还要求系统中已正确安装Synopsys ML Platform。该安装约需8GB磁盘空间并包含支持基于机器学习进行验证策略预测所需的全部软件包。安装Synopsys ML Platform步骤如下登录SolvNetPlus。进入Synopsys ML Platform页面并单击最新版本号。单击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_miscelastic_search_miscrequest_id19a95c9c91b4c5369d63a7c6090dacabbiz_id0utm_mediumdistribute.pc_search_result.none-task-blog-2~all~ElasticSearch~search_v2-1-145133977-null-null.541^v3^controlutm_term%E9%AA%8C%E8%AF%81%E7%82%B9spm1018.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两个子目录。crewcrew目录指的是工作组目录假设用户之前执行了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命令。phasephase目录指的是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)并返回总体验证结果。