相关阅读Formality
https://blog.csdn.net/weixin_45791458/category_12841971.html?spm=1001.2014.3001.5482
匹配点、对比点和逻辑锥
匹配指的是Formality工具尝试将参考设计中的每个匹配点与实现设计中的相应匹配点进行配对，这里的匹配点包括对比点(Compare Points)以及普通的匹配点(Points)。
在介绍匹配点前首先需要了解逻辑锥(Logic Cones)的概念，逻辑锥是指从特定的设计对象出发，并向后延伸至某些设计对象的组合逻辑结构，之所以被称为锥，是因为其就像椎体一样（一般）拥有一个顶点和多个底点，如图1所示。
图1 逻辑锥
Formality进行两个设计等价性检查的过程，就是验证两个设计中相应逻辑锥等价性的过程，这个过程会在两者相应逻辑锥底点提供相同的测试信号并观察顶点的输出，如果输出相同则代表两逻辑锥等价，由于对比的是逻辑锥的顶点，因此赋予它另一个名字——对比点，即逻辑锥等价和对比点等价是一个意思。
为了确定两个设计的相应逻辑锥，需要匹配逻辑锥的顶点和底点，其中顶点自不用说，它一定是对比点，而底点既可以是另一个逻辑锥的顶点（对比点）也可以是普通匹配点。
对比点可以是：输出端口、触发器、锁存器、黑盒输入引脚、循环断开点、多驱动线网、Cut-Point。而普通匹配点可以是：输入端口和黑盒输出引脚。
下面以一个例子进行说明，其中参考设计(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_pointsReference : 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_regImpl DFF Name(Last) i:/WORK/adder/c_regRef 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/cImpl Port Name(Last) i:/WORK/adder/cRef Port Name(Last) r:/WORK/adder/clkImpl Port Name(Last) i:/WORK/adder/clkRef 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 netBBox: black-boxBBPin: black-box pinBlock: hierarchical blockBlPin: hierarchical block pinCut: cut-pointDFF: non-constant DFF registerDFF0: constant 0 DFF registerDFF1: constant 1 DFF registerDFFX: constant X DFF registerDFF0X: constrained 0X DFF registerDFF1X: constrained 1X DFF registerLAT: non-constant latch registerLAT0: constant 0 latch registerLAT1: constant 1 latch registerLATX: constant X latch registerLAT0X: constrained 0X latch registerLAT1X: constrained 1X latch registerLATCG: clock-gating latch registerTLA: transparent latch registerTLA0X: transparent constrained 0X latch registerTLA1X: transparent constrained 1X latch registerLoop: cycle break pointNet: matchable netPort: primary (top-level) portUnd: undriven signal cut-pointUnk: unknown signal cut-pointFunc: matched by functionName: matched by nameTopo: matched by topologyUser: matched by userLast: 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 name0 Compare points matched by signature analysis0 Compare points matched by topology11 Matched primary inputs, black-box outputs0(0) Unmatched reference(implementation) compare points0(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_match | all |
| name_match_allow_subset_match | strict |
| variablename_match_based_on_nets | true |
| name_match_filter_chars | ‘~!@#$%^&*()_+=|\{}[]”:;<>?,./ |
| name_match_flattened_hierarchy_separator_style | / |
| name_match_multibit_register_reverse_order | false |
| name_match_use_filter | true |
| signature_analysis_match_primary_input | true |
| signature_analysis_match_primary_output | false |
| signature_analysis_match_compare_points | true |
| verification_blackbox_match_mode | any |
精确名称匹配
Formality首先进行精确的区分大小写名称匹配，然后进行精确的不区分大小写名称匹配。精确名称匹配技术是每次验证中默认使用的算法，使用该算法时，Formality会匹配参考设计和实现设计中名称相同的所有匹配点。
例如，以下设计对象将由Formality的精确名称匹配技术自动匹配：
Reference: /WORK/top/memreg(56)
Implementation: /WORK/top/MemReg(56)要控制是使用基于名称的匹配，还是仅依赖拓扑等价和签名分析来进行匹配，可按如下所示设置name_match变量：
| fm_shell | GUI |
| 使用set_app_var name_match [all | none | port | cell ]命令 | 1、点击Match 2、选择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或GUI：
| fm_shell | GUI |
| 使用set_app_var name_match_use_filter false命令 | 1、点击Match 2、选择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变量中移除或附加字符，默认的字符列表是：
~!@#$%^&*()_-+=|\[]{}”':;<>?,./例如，以下命令在默认的过滤字符列表中添加包括字符V：
fm_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_shell | GUI |
| 使用set_app_var signature_analysis_match_compa re_points false命令 | 1、点击Match 2、选择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或GUI：
| fm_shell | GUI |
| 使用set_app_var name_match_based_on_nets false命令 | 1、点击Match 2、选择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将成功匹配这些寄存器。
