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

相关阅读Formalityicon-default.png?t=O83Ahttps://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. 精确名称匹配（基于名称的匹配）
  2. 名称过滤（基于名称的匹配）
  3. 拓扑等价（不基于名称的匹配）
  4. 签名分析（不基于名称的匹配）
  5. 基于线网名称的匹配（基于名称的匹配）

        还有四种用户指定的匹配技术可用，但它们通常用于调试未匹配的点，它们是：使用用户指定名称进行匹配；使用匹配规则进行匹配；使用名称子集进行匹配；重命名用户提供的名称或使用映射文件。本文的重点不是它们，因此将不会讨论。

        当某种技术成功将一个设计中的匹配点与另一个设计中的匹配点匹配后，该点将免于其他匹配技术的处理，接下来的章节将详细描述每种默认的匹配技术。

        表1列出了控制匹配的变量，部分变量将在以下章节中进行描述。

变量名默认值
name_match

all

name_match_allow_subset_matchstrict
variablename_match_based_on_netstrue
name_match_filter_chars‘~!@#$%^&*()_+=|\{}[]”:;<>?,./
name_match_flattened_hierarchy_separator_style/
name_match_multibit_register_reverse_orderfalse
name_match_use_filtertrue
signature_analysis_match_primary_inputtrue
signature_analysis_match_primary_outputfalse
signature_analysis_match_compare_pointstrue
verification_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、点击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_shellGUI
使用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变量支持，以下是匹配过滤的规则：

  1. 忽略列表中的所有字符都会被替换为一个"_"，注意：多个连续的字符只会被替换为一个"_"。
  2. 如果忽略的字符是第一个或最后一个字符，则不会替换为"_"，而是直接丢弃。
  3. 数字与字符之间会以"_"分隔。例如，"bar2"将被转换为"bar_2"。
  4. 如果同一设计中的两个字符串在过滤后变为相同的字符串，则这两个字符串均不会通过名称过滤来匹配。

        下面两个例子中的设计对象将通过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_shellGUI
使用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_shellGUI
使用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.mzph.cn/pingmian/65866.shtml

如若内容造成侵权/违法违规/事实不符，请联系多彩编程网进行投诉反馈email:809451989@qq.com，一经查实，立即删除！

相关文章

OpenStack-Dashboard界面简单修改

OpenStack-Dashboard界面简单修改

OpenStack Dashboard界面替换图片 一、dashboard界面Logo的路径及文件 dashboard的Logo存放&#xff08;在Controller节点&#xff09;的路径&#xff1a; /usr/share/openstack-dashboard/openstack_dashboard/static/dashboard/img/涉及需要修改的文件&#xff08;3个&…
阅读更多...
分布式算法（五）：初识ZAB协议

分布式算法（五）：初识ZAB协议

文章目录 一、什么是Zookeeper二、ZAB与Zookeeper的关系为什么Zookeeper不直接使用Paxos 三、ZAB简介1.名词解释提案&#xff08;Proposal&#xff09;事务&#xff08;Transaction&#xff09;原子广播&#xff08;Atomic Broadcast&#xff09; 2.集群角色领导者&#xff08;…
阅读更多...
Mybatis 01

Mybatis 01

JDBC回顾 select 语句 "select *from student" 演示&#xff1a; 驱动包 JDBC 的操作流程&#xff1a; 1. 创建数据库连接池 DataSource 2. 通过 DataSource 获取数据库连接 Connection 3. 编写要执⾏带 ? 占位符的 SQL 语句 4. 通过 Connection 及 SQL 创建…
阅读更多...
tensorboard的界面参数与图像数据分析讲解

tensorboard的界面参数与图像数据分析讲解

目录 1.基础概念&#xff1a; (a)精确率与召回率&#xff1a; (b)mAP: (c)边界框损失&#xff1a; (d)目标损失&#xff1a; (e)分类损失&#xff1a; (f):学习率&#xff1a; 2.设置部分&#xff08;最右边部分&#xff09;&#xff1a; GENERAL&#xff08;常规设置…
阅读更多...
关于HarmonyOS Next中卡片的使用方法

关于HarmonyOS Next中卡片的使用方法

关于Harmony OS中卡片的使用方法 在Harmony OS中&#xff0c;静态卡片是一种非常有用的组件&#xff0c;用于提供应用内功能组件的交互和信息展示。本文将详细介绍如何在Harmony OS中使用静态卡片以及相关的API接口。 1. 概述 静态卡片是Harmony OS中的一种交互组件&#xf…
阅读更多...
《计算机网络A》单选题-复习题库解析-2

《计算机网络A》单选题-复习题库解析-2

目录 51、下列关于以太网网卡地址特点的说法中&#xff0c;不正确的是&#xff08; &#xff09;。 52、当一个Web Browser向一个使用标准服务器端口的Web Server提出请求时&#xff0c;那么在服务返回的响应包中&#xff0c;所使用的源端口是&#xff08; &#xff0…
阅读更多...
软件工程期末大复习（三）

软件工程期末大复习（三）

让我们来复习一下第三章的结构化分析与设计的内容&#xff0c;并做一些相关的题目。 3.1 概述 结构化分析与设计是一种系统开发方法&#xff0c;它强调将复杂问题分解成更小、更易于管理和解决的部分。这种方法基于结构化编程的原则&#xff0c;即通过将程序分解成模块来提高…
阅读更多...
Linux总结之CentOS Stream 9安装mysql8.0实操安装成功记录

Linux总结之CentOS Stream 9安装mysql8.0实操安装成功记录

Linux总结之CentOS Stream 9安装mysql8.0实操安装成功记录 由于网上很多的mysql8.0安装教程都是老版本或者安装过程记录有问题&#xff0c;导致经常安装到一半需要删除重新安装。所以将成功的实操安装过程记录一下&#xff0c;方面后面查阅&#xff0c;大家还有问题的可以在此讨…
阅读更多...
高等数学学习笔记 ☞ 无穷小与无穷大

高等数学学习笔记 ☞ 无穷小与无穷大

1. 无穷小 1. 定义&#xff1a;若函数当或时的极限为零&#xff0c;那么称函数是当或时的无穷小。 备注&#xff1a; ①&#xff1a;无穷小描述的是自变量的变化过程中&#xff0c;函数值的变化趋势&#xff0c;绝不能认为无穷小是一个很小很小的数。 ②&#xff1a;说无穷小时…
阅读更多...
KMP 2024 年总结，Kotlin 崛起的一年

KMP 2024 年总结，Kotlin 崛起的一年

2024 Google I/O 上正式官宣了 KMP&#xff08;Kotlin Multiplatform&#xff09;项目&#xff0c;它是 Google Workspace 团队的一项长期「投资」项目&#xff0c;由 JetBrains 开发维护和开源的项目&#xff0c;简单来说&#xff0c;JetBrains 主导&#xff0c;Google Worksp…
阅读更多...
欧拉-伯努利梁自由波动的频散关系

欧拉-伯努利梁自由波动的频散关系

梁和杆都是一维结构，但是梁的弯曲波比杆的纵波要复杂多。例如即使最简单的欧拉-伯努利(Euler-Bernoulli)梁的弯曲波也具有频散特征，且当梁的特征尺寸和弯曲波波长满足某个比值时，欧拉-伯努利梁不再适用，需要引入铁摩辛克(Timoshenko)梁模型。 考察某一欧拉-伯努利梁，长度…
阅读更多...
【SpringBoot教程】搭建SpringBoot项目之编写pom.xml

【SpringBoot教程】搭建SpringBoot项目之编写pom.xml

&#x1f64b;大家好&#xff01;我是毛毛张! &#x1f308;个人首页&#xff1a; 神马都会亿点点的毛毛张 &#x1f44f;今天毛毛张分享的内容主要是Maven 中 pom 文件&#x1f195;&#xff0c;涵盖基本概念、标签属性、配置等内容 文章目录 1.前言&#x1f96d;2.项目基本…
阅读更多...
【Java 学习】详讲代码块：控制流语句代码块、方法代码块、实例代码块（构造代码块）、静态代码块、同步代码块

【Java 学习】详讲代码块：控制流语句代码块、方法代码块、实例代码块（构造代码块）、静态代码块、同步代码块

&#x1f4ac; 欢迎讨论&#xff1a;如对文章内容有疑问或见解&#xff0c;欢迎在评论区留言&#xff0c;我需要您的帮助&#xff01; &#x1f44d; 点赞、收藏与分享&#xff1a;如果这篇文章对您有所帮助&#xff0c;请不吝点赞、收藏或分享&#xff0c;谢谢您的支持&#x…
阅读更多...
【亚马逊云科技】基于Amazon EKS部署高可用的OceanBase的最佳实践

【亚马逊云科技】基于Amazon EKS部署高可用的OceanBase的最佳实践

一、前言 随着企业业务的快速发展和数据量的不断增长&#xff0c;高性能、高可用的数据库解决方案成为了关键需求。OceanBase作为一款分布式关系型数据库&#xff0c;以其高扩展性、高可用性和高性能的特点&#xff0c;逐渐受到企业的广泛关注。然而&#xff0c;在复杂的分布式…
阅读更多...
代码随想录-笔记-其九

代码随想录-笔记-其九

继续我们之前未完成的动态规划的题目&#xff1a; 139. 单词拆分 - 力扣&#xff08;LeetCode&#xff09; 给你一个字符串 s 和一个字符串列表 wordDict 作为字典。如果可以利用字典中出现的一个或多个单词拼接出 s 则返回 true。 注意&#xff1a;不要求字典中出现的单词全…
阅读更多...
【工具】—— SpringBoot3.x整合swagger

【工具】—— SpringBoot3.x整合swagger

Swagger 是一个规范和完整的框架&#xff0c;用于生成、描述、调用和可视化 RESTful 风格的 Web 服务的接口文档。Swagger简单说就是可以帮助生成接口说明文档&#xff0c;操作比较简单添加注解说明&#xff0c;可以自动生成格式化的文档。 项目环境 jdk17SpringBoot 3.4.0Sp…
阅读更多...
从0入门自主空中机器人-2-1【无人机硬件框架】

从0入门自主空中机器人-2-1【无人机硬件框架】

关于本课程&#xff1a; 本次课程是一套面向对自主空中机器人感兴趣的学生、爱好者、相关从业人员的免费课程&#xff0c;包含了从硬件组装、机载电脑环境设置、代码部署、实机实验等全套详细流程&#xff0c;带你从0开始&#xff0c;组装属于自己的自主无人机&#xff0c;并让…
阅读更多...
基于视觉语言模型（VLM)的CogAgent

基于视觉语言模型（VLM)的CogAgent

前言 CogAgent 是由清华大学与智谱AI联合推出的一个多模态大模型&#xff0c;专注于图形用户界面&#xff08;GUI&#xff09;的理解和导航。它代表了在视觉语言模型&#xff08;VLM&#xff09;领域的一项重要进展&#xff0c;特别是在GUI Agent能力方面。相较于传统的基于文…
阅读更多...
win10、win11-鼠标右键还原、暂停更新

win10、win11-鼠标右键还原、暂停更新

系统优化 win 10jihuo win 11jihuo鼠标右键还原暂停更新 update 2024.12.28win 10 jihuo winx&#xff0c;打开powershell管理员&#xff0c;输入以下命令,选择1并等待 irm https://get.activated.win | iex参考&#xff1a;https://www.bilibili.com/video/BV1TN411M72J/?sp…
阅读更多...
C# 找出给定三角形的所有角度（Find all angles of a given triangle）

C# 找出给定三角形的所有角度（Find all angles of a given triangle）

给定三角形在二维平面上所有三个顶点的坐标&#xff0c;任务是找到所有三个角度。 示例&#xff1a; 输入&#xff1a;A (0, 0), B (0, 1), C (1, 0) 输出&#xff1a;90, 45, 45 为了解决这个问题&#xff0c;我们使用下面的余弦定律。 c^2 a^2 …
阅读更多...
最新文章

Copyright @ 2022~2023