CN119494301B 分布式数据通路组合等价性验证方法及分布式服务器 （中国科学院软件研究所）

号分布式数据通路组合等价性验证方法及分本发明提供了一种分布式数据通路组合等真获取内部的潜在等价节点并存放于等价节点提取其扇入锥，根据两组扇入锥构造子miter电路；根据子miter电路中异或块的稠密程度选取验证模式并对子miter电路进行验证；若验证成在等价节点验证完成；使用SAT求解器执行最终2S15、根据子miter电路文件中异或块的稠密程度选取用于验证所述子miter电路文件的验证模式并对所述子miter电路文件进行验证，所述验证模式包括格雷排布完备仿真模式和分布式电路可满足性求解模式；所述根据子miter电路文件中异或块的稠密程度选取根据当前分布式求解系统中的总CPU核心数量、子miter电路文件中异或联通块的数,根据当前分布式求解系统中的总CPU核心数量n和影响锥的输入引线数量N计算第二;如果Tar>WTCSS，其中为预设参数，则选取格雷排布完备仿真模式，否则选取分S16、如果验证成功，则合并对应的潜在等价节点和对采用结构哈希技术对存放于不同等价节点队列中的两组潜在等价节点对进行扇入锥获取子miter电路文件的输入节点位宽|PI|，所述输入节点位宽|PI|由格雷位宽wc、获取分布式求解系统中当前可操控的CPU核心数量C，根据当前可操3;根据所述格雷位宽生成用于仿真计算的各个仿真批次的格雷码输入序列并进行潜如果其中有一个CPU核心的仿真轮次中返回的验证结果为验证失败，则潜在等价节点在进行潜在等价节点对的等价验证时，记录每一个节点在上一可支配的从机器节点B…,R,以运行从机器节点B,…,R中的从分布式控制器；通过主分布式控制器将待求解的子miter电路文件分发给从分布式控制器，并实时监每个机器节点启动主线程以同步任务关系树并求解当前机器节点负责的子miter电前机器节点的分布式控制器则会根据同步任务关系树将求解结果反馈给当前机器节点的结果。4在等待空载从线程过程中，若有外部机器节点存在空载从线程并请求7.根据权利要求5所述的方法，其特征在于，所述采用随机采样的方法从子miter电路文件中选择分裂点，将每一分裂点的取值分别赋根据拆分后各子电路的传播锥判断各子电路的求解难易程度，并选对子电路的AIG与非图格式描述文件中的出边无非门个数grr、出边有非门个数gr-、入边无非门个数gsr以及入边有非门个数gs-进行门节点统计；根据门节点统计结果计算分裂点赋值为0时的第一向前传播预估值和第一向后传播预根据门节点统计结果计算分裂点赋值为1时的第二向前传播预估值和第二向后传播预根据第一向前传播预估值、第一向后传播预估值、第二向前传播。器上运行的计算机程序，所述处理器执行所述计算机程序时实现如权利要求1_8任一项所5与上面的SAT问题需要通过上下文区分，表示求解结果时用引号标注）和不可满足SAT_sweeping框架并不能有效解决数据通路组合成的空间里的membershiptesting问题。该问题可以比较快速的验证部分乘法器和加法SAT、BDD（二叉决策树问题）、或者ATPG问题去求解。目前实用性较差，弱于基于SAT_6[0009]精确仿真：通过穷举输入所有的可能性来判断问题是否述问题的分布式数据通路组合等价性验证方法及分[0016]S15、根据子miter电路文件中异或块的稠密程度选取用于验证所述子miter电路文件的验证模式并对所述子miter电路文件进行验证，所述验证模式包括格雷排布完备仿路文件的电路化简，否则返回步骤S14继续验证当前等价节点队列中的其他潜在等价节点[0020]采用结构哈希技术对存放于不同等价节点队列中的两组潜在等价节点对进行扇[0021]进一步地，所述根据子miter电路文件中异或块的稠密程度选取用于验证所述子[0022]根据当前分布式求解系统中的总CPU核心[0024]根据当前分布式求解系统中的总CPU核心数量n和影响锥的输入引线数量N计算7[0028]获取子miter电路文件的输入节点位宽|PI|，所述输入节点位宽|PI|由格雷位宽W和SIMD位宽组成；[0029]获取分布式求解系统中当前可操控的CPU核心数量C，根据当前可操控的CPU核心;[0032]根据所述格雷位宽生成用于仿真计算的各个仿真批次的格雷码输入序列并进[0033]如果其中有一个CPU核心的仿真轮次中返回的验证结果为验证失败，则潜在等价[0035]在进行潜在等价节点对的等价验证时，记录每一个节点在上一仿真批次时的取[0036]进一步地，当采用分布式电路可满足性求解模式对所述子miter电路文件进行验当前可支配的从机器节点B…,R,以运行从机器节点B,…,B中的从分布式控制器；[0038]通过主分布式控制器将待求解的子miter电路文件分发给从分布式控制器，并实[0039]每个机器节点启动主线程以同步任务关系树并求解当前机器节点负责的子miter电路文件中选取分割点以将电路验证任务拆分为两个子任务，并调度相应数量的从8[0042]如果当前机器节点的空载从线程不足以分配拆分后的子任务，则将主线程的挂[0043]在等待空载从线程过程中，若有外部机器节点存在空载[0044]进一步地，所述从待验证的子miter电路文件中选取分割点以将电路验证任务拆[0045]采用随机采样的方法从子miter电路文件中选择分裂点，将每一分裂点的取值分[0048]对子电路的AIG与非图格式描述文件中的出边无非门个数grr、出边有非门个数[0049]根据门节点统计结果计算分裂点赋值为0时的第一向前传播预估值和第一向后传[0052]根据门节点统计结果计算分裂点赋值为1时的第二向前传播预估值和第二向后传[0059]根据分布式机群的总CPU核心数目和电路拆分前后待验证电路中异或块的数量及每一异或块大小计算电路拆分前后待验证电路的预9[0060]很据电路拆分前后待验证电路的预计验证运行时间的变化量ATsar作为打分值A了一种深度结合格雷排布完备仿真模式或分布式电路可满足性求解模式两种算力引擎的CEC验证方法，本发明通过在数据通路组合等价性验证过程中涉及的待验证子电路中异或块的稠密程度来判断应该采用格雷排布完备仿真模式或分布式电路可满足性求解模式进[0063]上述说明仅是本发明技术方案的概述，为了能够更清楚[0068]图4为本发明实施例提供的采用分布式电路可满足性求解模式进行求解验证的流证方法是一种深度结合格雷排布完备仿真模式和分布式电路可满足性求解模式两种算力引擎的CEC验证方法。其中分布式电路可满足性系统是一种基于电路的特征的分治SAT算[0076]图1示意性示出了本发明一个实施例的分布式数据通路组合等价性验证方法的流次从等价节点队列中选择潜在等价节点对也可以随机从等价节点队列中选择潜在等价节[0084]S15、根据子miter电路文件中异或块的稠密程度选取用于验证所述子miter电路文件的验证模式并对所述子miter电路文件进行验证，所述验证模式包括格雷排布完备仿路文件的电路化简，否则返回步骤S14继续验证当前等价节点队列中的其他潜在等价节点还可以在电路化简后重新对新的Miter电路文件进行随机逻辑仿真，以提高后续获取的潜[0088]本实施例中，将归属于同一等价类的潜在等价节点存放于同一等价节点队列之格雷排布完备仿真模式或分布式电路可满足性求解模式两种算力引擎的CEC验证方法。本发明通过数据通路组合等价性验证过程中涉及的待验证子电路中异或块的稠密程度来判采用结构哈希技术对存放于不同等价节点队列中的两组潜在等价节点对进行扇入锥结构则会将处于队列后面的潜在等价节点对从队列中删除，以防止同一结构的多次等价性判[0094]根据当前分布式求解系统中分布式机群的总C异或联通块的数量k以及每一异或联通块大小计算第一预计验证运行时间Tar：[0097]根据当前分布式求解系统中分布式机群的总CPU核心数量和影响锥的输入引线数量N计算第二预计验证运行时间Tces：性求解模式。其中为预设参数，的取值可由同构小电路[0101]图2给出了分布式电路可满足性求解系统的结构示意图。分布式电路可满足性求解系统用于采用分布式电路可满足性求解模式对所述子miter电路文件进行验证。该分布式求解系统会在每一台机器节点上会运行一个并行求解系统，并通过分布式控制器交互。[0102]图3给出了任务管理树的示意图。每一台机器节点的并行引擎的主线程均有一个个线程求解，表示任务在哪一个外部机器节点求解，且该任务为外部机程度衡量，Tar表示根据分布式机群的总CPU核心数目和电路拆分前后待验证电路中异或块的数量及每一异或块大小计算出的电路拆分前后待验证电路的预计验证启动当前可支配的从机器节点B…,R,以运行从机器节点B,…,R中的从分布式控制[0106]S22、通过主分布式控制器将待求解的子miter电路文件[0107]S23、每个机器节点启动主线程以同步任务关系树并求解当前机器节点负责的子miter电路文件中选取分割点以将电路验证任务拆分为两个子任务，并调度相应数量的点存在空载从线程并请求任务求解，则选取对应的一个子任务分配到外部机器节点求解，数目MP;管理内部的并行引擎。首先主线程会立刻启动一个线程T,，直接求解该机器节点[0114]本实施例中，所述从待验证的子miter电路文件中选取分割点以将电路验证任务拆分为两个子任务的具体实现方式如下：采用随机采样的方法从子miter电路文件中选择[0115]图5示出了基于传播锥预测的切割点选择方法的原理示意图。待求解的问题可以[0118]对子电路的AIG与非图格式描述文件中的出边无非门个数grr、出边有非门个数[0119]根据门节点统计结果计算分裂点赋值为0时的第一向前传播预估值和第一向后传[0122]根据门节点统计结果计算分裂点赋值为1时的第二向前传播预估值和第二向后传[0129]根据分布式机群的总CPU核心数目和电路拆分前后待验证电路中异或块的数量及每一异或块大小计算电路拆分前后待验证电路的预[0130]很据电路拆分前后待验证电路的预计验证运行时间的变化量ATsar作为打分值A本发明采用格雷排布完备仿真模式对所述子miter电路文件进行验证，能够进一步提高两[0132]如图6所示，在本发明的一个实施例中，当采用格雷排布完备仿真模式对所述子[0136]S33、获取采用SIMD技术串行求解时的机器指令宽度，根据机器指令宽度计算[0137]S34、根据输入节点位宽|PI|、节点位宽以及SIMD位宽计算格雷位宽WC：。[0140]本实施例中，会根据CPU的核心数目和SIMD的期望压缩指令长度计算节点位宽和该计算机程序被处理器执行时实现如上分布式数据通路组合等价了一种深度结合格雷排布完备仿真模