Formality：匹配(match)是如何进行的？

相关阅读Formalityhttps://blog.csdn.net/weixin_45791458/category_12841971.html?spm1001.2014.3001.5482匹配点、比较点和逻辑锥匹配指的是Formality工具尝试将参考设计中的每个匹配点与实现设计中的相应匹配点进行配对这里的匹配点包括比较点(Compare Points)以及普通的匹配点(Points)。在介绍匹配点前首先需要了解逻辑锥(Logic Cones)的概念逻辑锥是指从特定的设计对象出发并向后延伸至某些设计对象的组合逻辑结构之所以被称为锥是因为其就像椎体一样一般拥有一个顶点和多个底点如图1所示。图1 逻辑锥Formality进行两个设计等价性检查的过程就是验证两个设计中相应逻辑锥等价性的过程这个过程会在两者相应逻辑锥底点提供相同的测试信号并观察顶点的输出如果输出相同则代表两逻辑锥等价由于比较的是逻辑锥的顶点因此赋予它另一个名字——比较点即逻辑锥等价和比较点等价是一个意思。为了确定两个设计的相应逻辑锥需要匹配逻辑锥的顶点和底点其中顶点自不用说它一定是比较点而底点既可以是另一个逻辑锥的顶点比较点也可以是普通匹配点。比较点可以是输出端口、触发器、锁存器、黑盒输入引脚、循环断开点、多驱动线网、Cut-Point可以是线网类(CUT_NET)或引脚类(CUT_PIN)它们来自探针设置(set_probe_points)、无驱动线网或用户设置(set_cutpoint)而普通匹配点可以是输入端口和黑盒输出引脚。下面以一个例子进行说明其中参考设计(reference design)是RTL代码而实现设计(implementation design)是综合后的网表。// reference design module adder ( input [2:0] a, input [2:0] b, input clk, output reg [2:0] sum, output reg c ); // 定义中间信号 wire [3:0] blackbox_result; // 实例化黑盒模块 BlackBox u_blackbox ( .in1(a), .in2(b), .result(blackbox_result) ); // 使用黑盒的输出计算结果 always (posedge clk) begin {c, sum} blackbox_result; end endmodule // implementation design module adder ( a, b, clk, sum, c ); input [2:0] a; input [2:0] b; output [2:0] sum; input clk; output c; tri [2:0] a; tri [2:0] b; tri [3:0] blackbox_result; BlackBox u_blackbox ( .in1(a), .in2(b), .result(blackbox_result) ); DFFQXL c_reg ( .D(blackbox_result[3]), .CK(clk), .Q(c) ); DFFQXL \sum_reg[2] ( .D(blackbox_result[2]), .CK(clk), .Q(sum[2]) ); DFFQXL \sum_reg[1] ( .D(blackbox_result[1]), .CK(clk), .Q(sum[1]) ); DFFQXL \sum_reg[0] ( .D(blackbox_result[0]), .CK(clk), .Q(sum[0]) ); endmodule由于在该例中存在黑盒使用set_top命令设置顶层模块前需要将hdlin_unresolved_modules变量设置为black_box否则会有以下报错。Error: Unresolved references detected during link. (FM-234)当使用match命令进行匹配后结果如图2所示。图2 匹配结果从图1中可以看出一共有三类匹配点端口输入/输出不区分、触发器输入引脚/输出引脚不区分和黑盒引脚输入引脚/输出引脚不区分总计25个。使用report_matched_points命令也可以得到相似的结果如下所示。Formality (match) report_matched_points ************************************************** Report : matched_points Reference : r:/WORK/adder Implementation : i:/WORK/adder Version : O-2018.06-SP1 Date : Sun Dec 29 17:22:41 2024 ************************************************** 25 Matched points: Ref DFF Name(Last) r:/WORK/adder/c_reg Impl DFF Name(Last) i:/WORK/adder/c_reg Ref DFF Name(Last) r:/WORK/adder/sum_reg[0] Impl DFF Name(Last) i:/WORK/adder/sum_reg[0] Ref DFF Name(Last) r:/WORK/adder/sum_reg[1] Impl DFF Name(Last) i:/WORK/adder/sum_reg[1] Ref DFF Name(Last) r:/WORK/adder/sum_reg[2] Impl DFF Name(Last) i:/WORK/adder/sum_reg[2] Ref BBPin Name(Last) r:/WORK/adder/u_blackbox/in1[0] Impl BBPin Name(Last) i:/WORK/adder/u_blackbox/in1[0] Ref BBPin Name(Last) r:/WORK/adder/u_blackbox/in1[1] Impl BBPin Name(Last) i:/WORK/adder/u_blackbox/in1[1] Ref BBPin Name(Last) r:/WORK/adder/u_blackbox/in1[2] Impl BBPin Name(Last) i:/WORK/adder/u_blackbox/in1[2] Ref BBPin Name(Last) r:/WORK/adder/u_blackbox/in2[0] Impl BBPin Name(Last) i:/WORK/adder/u_blackbox/in2[0] Ref BBPin Name(Last) r:/WORK/adder/u_blackbox/in2[1] Impl BBPin Name(Last) i:/WORK/adder/u_blackbox/in2[1] Ref BBPin Name(Last) r:/WORK/adder/u_blackbox/in2[2] Impl BBPin Name(Last) i:/WORK/adder/u_blackbox/in2[2] Ref BBPin Name(Last) r:/WORK/adder/u_blackbox/result[0] Impl BBPin Name(Last) i:/WORK/adder/u_blackbox/result[0] Ref BBPin Name(Last) r:/WORK/adder/u_blackbox/result[1] Impl BBPin Name(Last) i:/WORK/adder/u_blackbox/result[1] Ref BBPin Name(Last) r:/WORK/adder/u_blackbox/result[2] Impl BBPin Name(Last) i:/WORK/adder/u_blackbox/result[2] Ref BBPin Name(Last) r:/WORK/adder/u_blackbox/result[3] Impl BBPin Name(Last) i:/WORK/adder/u_blackbox/result[3] Ref Port Name(Last) r:/WORK/adder/a[0] Impl Port Name(Last) i:/WORK/adder/a[0] Ref Port Name(Last) r:/WORK/adder/a[1] Impl Port Name(Last) i:/WORK/adder/a[1] Ref Port Name(Last) r:/WORK/adder/a[2] Impl Port Name(Last) i:/WORK/adder/a[2] Ref Port Name(Last) r:/WORK/adder/b[0] Impl Port Name(Last) i:/WORK/adder/b[0] Ref Port Name(Last) r:/WORK/adder/b[1] Impl Port Name(Last) i:/WORK/adder/b[1] Ref Port Name(Last) r:/WORK/adder/b[2] Impl Port Name(Last) i:/WORK/adder/b[2] Ref Port Name(Last) r:/WORK/adder/c Impl Port Name(Last) i:/WORK/adder/c Ref Port Name(Last) r:/WORK/adder/clk Impl Port Name(Last) i:/WORK/adder/clk Ref Port Name(Last) r:/WORK/adder/sum[0] Impl Port Name(Last) i:/WORK/adder/sum[0] Ref Port Name(Last) r:/WORK/adder/sum[1] Impl Port Name(Last) i:/WORK/adder/sum[1] Ref Port Name(Last) r:/WORK/adder/sum[2] Impl Port Name(Last) i:/WORK/adder/sum[2] [BBNet: multiply-driven net BBox: black-box BBPin: black-box pin Block: hierarchical block BlPin: hierarchical block pin Cut: cut-point DFF: non-constant DFF register DFF0: constant 0 DFF register DFF1: constant 1 DFF register DFFX: constant X DFF register DFF0X: constrained 0X DFF register DFF1X: constrained 1X DFF register LAT: non-constant latch register LAT0: constant 0 latch register LAT1: constant 1 latch register LATX: constant X latch register LAT0X: constrained 0X latch register LAT1X: constrained 1X latch register LATCG: clock-gating latch register TLA: transparent latch register TLA0X: transparent constrained 0X latch register TLA1X: transparent constrained 1X latch register Loop: cycle break point Net: matchable net Port: primary (top-level) port Und: undriven signal cut-point Unk: unknown signal cut-point Func: matched by function Name: matched by name Topo: matched by topology User: matched by user Last: matched during most recent matching]除了在GUI窗口能观察到匹配结果在使用match命令后会得到匹配的总体情况如下所示。Formality (setup) match Reference design is r:/WORK/adder Implementation design is i:/WORK/adder Status: Checking designs... Warning: Design r:/FM_BBOX/BlackBox is a black box and there are cells referencing it (FM-160) Warning: Design i:/FM_BBOX/BlackBox is a black box and there are cells referencing it (FM-160) Warning: 1 (1) black-box references found in reference (implementation) design; see formality4.log for list (FM-182) Status: Building verification models... Status: Matching... *********************************** Matching Results *********************************** 14 Compare points matched by name 0 Compare points matched by signature analysis 0 Compare points matched by topology 11 Matched primary inputs, black-box outputs 0(0) Unmatched reference(implementation) compare points 0(0) Unmatched reference(implementation) primary inputs, black-box outputs ****************************************************************************************可以看出 Matching Results中的匹配结果将比较点(Compare points matched by ...)和普通匹配点(Matched primary inputs, black-box outputs)区分开来了其中比较点有14个而普通匹配点有11个。匹配的具体过程匹配可以是基于名称的也可以是其他方式的当进行匹配时默认会使用以下匹配技术并按照以下顺序执行精确名称匹配基于名称的匹配名称过滤基于名称的匹配拓扑等价不基于名称的匹配签名分析不基于名称的匹配基于线网名称的匹配基于名称的匹配还有四种用户指定的匹配技术可用但它们通常用于调试未匹配的点它们是使用用户指定名称进行匹配使用匹配规则进行匹配使用名称子集进行匹配重命名用户提供的名称或使用映射文件。本文的重点不是它们因此将不会讨论。当某种技术成功将一个设计中的匹配点与另一个设计中的匹配点匹配后该点将免于其他匹配技术的处理接下来的章节将详细描述每种默认的匹配技术。表1列出了控制匹配的变量部分变量将在以下章节中进行描述。变量名默认值name_matchallname_match_allow_subset_matchstrictvariablename_match_based_on_netstruename_match_filter_chars‘~!#$%^*()_|\{}[]”:;?,./name_match_flattened_hierarchy_separator_style/name_match_multibit_register_reverse_orderfalsename_match_use_filtertruesignature_analysis_match_primary_inputtruesignature_analysis_match_primary_outputfalsesignature_analysis_match_compare_pointstrueverification_blackbox_match_modeany精确名称匹配Formality首先进行精确的区分大小写名称匹配然后进行精确的不区分大小写名称匹配。精确名称匹配技术是每次验证中默认使用的算法使用该算法时Formality会匹配参考设计和实现设计中名称相同的所有匹配点。例如以下设计对象将由Formality的精确名称匹配技术自动匹配Reference: /WORK/top/memreg(56) Implementation: /WORK/top/MemReg(56)要控制是使用基于名称的匹配还是仅依赖拓扑等价和签名分析来进行匹配可按如下所示设置name_match变量fm_shellGUI使用set_app_var name_match[all | none | port | cell ]命令1、点击Match2、选择Edit Formality Tcl Variables将会显示Formality Tcl Variables对话框。3、在Matching部分选择name_match变量。4、在Choose a value列表中选择all、none、port或cell。5、选择 File Close。默认值all会执行所有的基于名称的匹配使用none可禁用除输入端口外的所有基于名称的匹配使用port只对于端口执行基于名称的匹配使用cell只对于触发器、锁存器、黑盒输入和输出引脚执行基于名称的匹配。名称过滤在精确名称匹配之后Formality会尝试过滤后的不区分大小写的名称匹配通过过滤对象名称中的某些字符来进行匹配。要关闭默认的过滤名称匹配行为可以按照以下方法使用Formality Shell或GUIfm_shellGUI使用set_app_var name_match_use_filterfalse命令1、点击Match2、选择Edit Formality Tcl Variables将会显示Formality Tcl Variables对话框。3、在Matching部分选择name_match_use_filter变量。4、取消选中Use name matching filter。5、选择 File Close。name_match_use_filter变量由name_match_filter_chars变量支持以下是匹配过滤的规则忽略列表中的所有字符都会被替换为一个_注意多个连续的字符只会被替换为一个_。如果忽略的字符是第一个或最后一个字符则不会替换为_而是直接丢弃。数字与字符之间会以_分隔。例如bar2将被转换为bar_2。如果同一设计中的两个字符串在过滤后变为相同的字符串则这两个字符串均不会通过名称过滤来匹配。下面两个例子中的设计对象将通过Formality名称过滤算法匹配Reference: /WORK/top/memreg__[56][1] Implementation: /WORK/top/MemReg_56_1其中需要重点注意的是参考设计的__[被替换为_][被替换为_]被丢弃。Reference: /WORK/top/BUS/A[0] Implementation: /WORK/top/bus__a_0其中需要重点注意的是参考设计的/被替换为_[被替换为_]被丢弃实现设计的__被替换为_。作为层次分隔符的/也会被替换就像名称中的”/“那样可能来自ungroup命令详情见Verilog基础简单标识符和转义标识符。下面一个例子中的不会通过Formality名称过滤算法匹配Reference: /WORK/top/BUS/A[0] Implementation: /WORK/top/busa_0可以在name_match_use_filter变量中移除或附加字符默认的字符列表是~!#$%^*()_-|\[]{}”:;?,./例如以下命令在默认的过滤字符列表中添加包括字符Vfm_shell (match) set_app_var name_match_filter_chars \ {~!#$%^*()_-|\[]{}:;?,./V}拓扑等价Formality尝试通过拓扑等价来匹配剩余的未匹配点——也就是说如果驱动两个未匹配点的逻辑锥(logic cones)在拓扑上是等价的那么这两个点将被匹配。签名分析签名分析是对匹配点的功能性和拓扑签名进行的迭代分析。功能性签名来自于随机模式仿真拓扑签名来自于输入锥(fan-in cone)拓扑。签名分析算法使用仿真生成输出数据模式或输出触发器的值签名签名分析中的仿真过程用于唯一地识别一个控制节点。例如如果一个向量使得一个触发器对的值变为1而所有其他控制触发器的值在两个设计中都变为0那么签名分析完成了一次匹配。为了使签名分析正常工作两个设计中的输入端口必须具有匹配的名称或者在必要的时候使用set_user_match、set_compare_rule或rename_object命令手动匹配它们。在签名分析过程中Formality工具会自动尝试匹配先前未匹配的数据路径和层次结构块及其引脚。要关闭自动匹配数据路径块和引脚可以将signature_analysis_match_datapath变量设置为false。要关闭自动匹配层次结构块和引脚可以将signature_analysis_match_hierarchy变量设置为false。在后一种情况下如果在运行层次化验证时发现性能下降可以将signature_analysis_match_hierarchy的设置改为false。要禁用所有签名分析匹配并忽略其他signature_analysis*变量可以将signature_analysis变量设置为false其默认值为true。如果未匹配对象的数量有限Formality中的签名分析效果良好但如果匹配点存在数千个不匹配的情况算法的效果可能较差。在这种情况下为了节省时间可以在Formality shell或GUI中关闭该算法如下表所示。fm_shellGUI使用set_app_varsignature_analysis_match_compare_points false命令1、点击Match2、选择Edit Formality Tcl Variables将会显示Formality Tcl Variables对话框。3、在Matching部分选择signature_analysis_match_compare_points变量。4、取消选中Use signature analysis。5、选择 File Close。默认情况下签名分析不会尝试匹配输出端口可以通过将 signature_analysis_match_primary_output变量设置为true来指定输出端口的匹配。通过编写比较规则(set_compare_rule)而不是禁用签名分析可能会减少匹配的运行时间。例如如果参考设计和实现设计中都有额外的触发器使用比较规则效果好。注意Formality使用签名分析来匹配具有不同名称的黑盒子。在黑盒子匹配之后工具首先尝试通过名称匹配黑盒子的引脚。如果黑盒子引脚的名称相同则匹配这些引脚。如果引脚名称不同则工具会再次使用签名分析来功能性地匹配引脚。基于线网名称的匹配Formality通过精确匹配和过滤匹配其连接的线网来匹配所有剩余未匹配的比较点匹配可以通过直接连接的驱动线网或被驱动线网进行。要关闭基于线网名称的比较点匹配可以按照以下方法使用Formality Shell或GUIfm_shellGUI使用set_app_varname_match_based_on_nets false命令1、点击Match2、选择Edit Formality Tcl Variables将会显示Formality Tcl Variables对话框。3、在Matching部分选择name_match_based_on_nets变量。4、取消选中Use net names。5、选择 File Close。例如以下设计对象有不同的名称Reference: /WORK/top/memreg(56) Implementation: /WORK/top/MR(56)Formality无法通过精确名称匹配技术将它们匹配但如果这些触发器输出驱动的线网名称相同Formality将成功匹配这些触发器。