如何进行Keypoint mapping操作

今天就跟大家聊聊有关如何进行Keypoint mapping操作，可能很多人都不太了解，为了让大家更加了解，小编给大家总结了以下内容，希望大家根据这篇文章可以有所收获。

今次来聊形式验证中关键的一步mapping. 在LEC 中执行命令"set_system_mode lec" 工具即会进行mapping 操作；如果不想让工具在切模式时做mapping 请用命令"set_system_mode lec -nomap" 来切模式，切换到lec 模式之后再用命令"map_key_points" 来做mapping. 如果你不是老顽固，请用第一种方式。

mapping 是形式验证最关键的一步，mapping 算法厉害与否基本决定了一个形式验证工具的优劣。而LEC 的mapping 算法显然是强大的，它不依赖于任何优化工具吐出的指导文件即能完成mapping. LEC mapping 可以分成三步：

• 识别：在分析完golden 跟 revised 设计之后，识别KeyPoint. 

• 配对：对Golden 中的每一个KeyPoint 确定Revised 中与之对应的KeyPoint. 

• 绑定：将对应的KeyPoint 绑定到一起。

识别

LEC 会分别分析Golden 和 Revised 设计来识别KeyPoint 并按照PI, PO, BBOX, DLAT, DFF, CUT, Z, E 将KeyPoint 分类。在解析设计时，LEC 会对设计中的所有Gate 进行编号，每个Gate 都有一个自己专属的编号，俗称"Gate-ID", 在后续的debug 中可以直接用该ID 访问对应Gate. mapping 完之后可以用如下命令来报出设计中对应的KeyPoint. 

report_key_point -type DFF DLAT CUT PO –revised 

配对

配对是mapping 中最重要且复杂的一步，此时LEC 要充当月老角色，通过复杂算法根据出身、性别、年龄、性格给Golden 中每一个KeyPoint 在Revised 中找一个如意郎君。在配对时还需要将Golden 或Revised 中冗余的KeyPoint 剔除掉，如被优化掉的常值寄存器、工具插入的clock gating 逻辑、做了合并的寄存器等，这些冗余的KeyPoint 是天注定的单身狗，没对可配。 到目前为止工具仍是用户的使役，在LEC 中用户可以用命令"add mapped points" 做强行配对。

绑定

配好对之后，需要将对应的KeyPoint 一一绑定起来。绑定完成后Mapping 结束，LEC 会给出一个summary 结果。

Mapping 结束后可以在GUI 中点击长得像一本书的这个按钮，打开Mapping Manager 来检查Mapping 的结果，成功mapping 的点会被标注成"Mapped Key Point", 没有mapping 成功的点，会被分成三类：Unreachable, Extra, Not-mapped, 对于每一类的含义请听下回分解。

在实际项目中，mapping 过程可能需要多次迭代或修正，如综合工具对设计中对象名字的更改超出了LEC 默认的命名匹配规则，则需要在LEC 中用命令"set naming rule" 或"add renaming rule" 做相应设置，或者用命令"set mapping method" 来调整mapping 策略；如综合工具做了冗余/常值寄存器优化，做了寄存器merge, 插了clock gating cell, 则需要用命令"set flatten model" 使能对应的modeling 算法。更新了对应设置后可以用命令"map key points" 做进一步mapping. 

看完上述内容，你们对如何进行Keypoint mapping操作有进一步的了解吗？如果还想了解更多知识或者相关内容，请关注亿速云行业资讯频道，感谢大家的支持。