LEC 起了头之后，本想着是一气儿写下去，怎奈经常会有小姐姐小哥哥蹦出来，一起愉快地讨论了别的问题，于是拐过去哼哧哼哧的写了旁的，今儿接着前面的继续写，如果你是第一次读这个系列，可以快速回顾《论形式验证 | LEC Jumpstart》《论形式验证 | 撸 LEC flow》《论形式验证 | KeyPoint》。
闲话少叙，书接上回，上回陈诉了KeyPoint 的定义跟分类，今次来聊形式验证中关键的一步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.
作者：陌上风骑驴
来源：https://mp.weixin.qq.com/s/H\_g7as9IOO53tPliygtPpQ
作者微信公众号
相关文章推荐
• STA | 串扰，理论分析
•论形式验证 | KeyPoint
更多IC设计技术干货请关注IC设计技术专栏。
