当前位置：首页 > article >正文

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

article 2025/1/5 7:20:03

相关阅读Formalityhttps://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_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_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

其中需要重点注意的是：参考设计的"/"被替换为"_"，"["被替换为"_"，"]"被丢弃；实现设计的"__"被替换为"_"。参考设计和实现设计中除了前两个以外的"/"不应被理解为是层次分隔符，而应当是总线名字的一部分，这是转义标识符的使用，详情见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将成功匹配这些寄存器。

查看全文

http://www.kler.cn/a/457484.html

数据结构与算法之动态规划: LeetCode 213. 打家劫舍 II (Ts版)

CentOS — 目录管理

云效流水线使用Node构建部署前端web项目

第R3周：RNN-心脏病预测

UnityRenderStreaming使用记录（三）

GPU 进阶笔记（一）：高性能 GPU 服务器硬件拓扑与集群组网

通过MySQL binlog日志，使用canal同步分库分表数据，到 Elasticsearch

大数据技术-Hadoop（一）Hadoop集群的安装与配置

【每日学点鸿蒙知识】navigation跳转异常、默认加载移动端版本网页、Menu位置、View生成图片保存相册、H5原生交互

2024/12/29 黄冈师范学院计算机学院网络工程《路由期末复习作业一》

Linux day 1129

java高频面试之SE-05

关于ESD（静电放电）等级的划分

.net8使用log4.net并自定义日志表的字段

Django管理界面自定义操作重启ECS服务

业务智能化的关键：探索事件驱动的业务规则模型

网络的类型

面试场景题系列：设计键值存储系统

在Bash Shell脚本中创建和使用变量

如何正确使用Jmeter

vue2使用pdfjs-dist和jsPDF生成pdf文件

多显卡服务器如何设置使用集成显卡输出信号？

从零开始开发纯血鸿蒙应用之UI封装

HarmonyOS NEXT应用开发实战：一分钟写一个网络接口，JsonFormat插件推荐

java开发配置文件集合

E6 中的扩展运算符(Spread) 和剩余运算符(Rest)

匹配点、对比点和逻辑锥

匹配的具体过程

精确名称匹配

名称过滤

拓扑等价

签名分析

基于线网名称的匹配

相关文章：