温故知新，如果你是初次阅读该系列，建议先阅读一下《论形式验证 | LEC Jumpstart》《论形式验证 | 撸 LEC flow》《论形式验证 | KeyPoint》《论形式验证 | Keypoint mapping》。本文来看Mapping 之后KeyPoint 的分类。
Mapping 之后，配对且绑定成功的点被称作"Mapped Key Points"; 没有配对或绑定，或即便配了对却是 "假夫妻" 的统统被称作 "Unmapped Key Points". 这世上的幸福大抵相似也没什么好去描述的，而不幸福却有各自的孤独，故值得探讨。"Unmapped Key Points" 缘于不同原因可被分为三类：
- Unreachable key points
- Extra key points
- Not-mapped key points
Unreachable key points:
这一类是 "假夫妻"，因为他们不具功能性。
严肃定义：这些key points 不会扇出到任何的primary output 端口、也不会扇出到任何其他时序单元的输入、也不会扇出到任何black box 的输入。
说人话：这些key points, 在当前模式下，对整个电路没有实际的逻辑功能，他们只是在那里占着面积耗着功耗。
原因：一类是：这些key points 在该模式下没逻辑功能，但在其他模式下有，在该模式下被设置的约束给bypass 掉了，如function 模式下DFT 相关的逻辑；另一类是：被LEC modeling 处理了，如clock gating cell, 在设置了" set flatten modeling -gated\_clock " 会被LEC model 成寄存器D pin 的MUX; 另一类是：这些key points 真的就是 "渣渣"，它们没有意义地活着且浪费着资源，多数是由逻辑优化工具优化不彻底造成的。
对待方式：默认，LEC 不会对unreachable key points 做map, 也不建议对unreachable key points 做map, 如果你同情心泛滥非要给它们配对，可以在map 前设置命令 "set mapping method –unreach", 后果是增加compare 的时间且导致更多假的non-eq 点。如果你只想给某一组unreachable key poins 做map 可以用命令 "add mapped points" 设置。
示例：在如下示例中，由于SEL 端被设置成了0, 导致FF2 的输出永远不会被传播下去，成了一个unreachable 的key points.
Extra key points：
这一类是"天注孤"，因为命里就没有对象可与之匹配。
严肃定义：这些key points 只存在于Golden 或Revised 其中之一，不会同时存在于两个设计中。
说人话：这些key poins 可能是primary input, primary output, DFF, Latch, 它们要么是被优化掉的冗余逻辑，要么是被增加的非功能ports。
类别及解决办法：
- 由于穿了马甲，被误认为"天注孤" 的，对于这一类，需要用户加一些renaming rule 将其马甲脱掉，帮其配对成功。
- 新增加的非功能ports, 如P&R 阶段加入的PG pin, 可以用命令"add pin constraints" 将其设为常值。如综合时加入的DFT ports, 这类ports 不属于要验证逻辑功能的范畴，如果是output ports 可以直接用命令"add ignored outputs" 将其逐出，设了ignored 之后不会被计入任何mapping status 类型；如果是input ports 如果这些input ports 是某些key points 的输入，则需要根据设计意图用命令 "add pin constraints" 做约束，如scan\_enable, 如果这些input ports 不扇出到任何key points 则可以直接无视或用命令"add ignored inputs" 将其逐出。
- 冗余的的DFF 和Latch, 如无特别设置综合工具会将冗余逻辑优化掉，大部分情况下，在LEC 中如果设了对应的modeling option, LEC 可以识别出对应的冗余逻辑，并将对其做modeling. 对于一些复杂设计，在compare 之前，LEC 无法确认Not-mapped DFF/Latch 是否是冗余的，在compare 过程中，工具会做更深刻地分析，在比较结束后会将这些Not-mapped DFF/Latch 归类到Extra key points. 所以在一些case 上会看到比较前后的Extra key points 个数发生变化。
Not-mapped key points:
这一类是"老大难"，他们是来历劫的，是要历经万难才能配对成功。
严肃定义：由于各种原因，LEC 无法轻易在另一个design 中找到与这些key points 对应的点。
说人话：这类key points 既可能在Golden 中也可能在Revised 中，在无外力协助时，LEC 用尽全力也找不到与其对应的点，而这些点大多都是会导致比较结果失败的点，所以要施加各种小魔法，在compare 前将其配对成功。只有极少数的点，在compare 过程中，LEC通过深入了解发现它们不是『老大难』而是『天注孤』或『假夫妻』，在compare 后会把他们归于『天注孤』或『假夫妻』。
类别及解决办法：
- 由于穿了马甲，他就认不出她，对于这一类，需要用户加一些renaming rule 将其马甲脱掉，帮其配对成功。
- modeling option 设置不全，LEC 未对优化工具的优化行为对应建模，如优化动作：寄存器的复制及合并、被优化掉的常值寄存器、"don't care" 逻辑被优化为常值0/1、将寄存器替换成master-slave latches 、clock gating cell 的插入及复制、冗余寄存器的优化等。对于这类，需要用"set flatten model" 加对应的option 予以解决；也可以用analyze\_setup -effort \<high | ultra\> 来解；也可以用set\_analyze\_option -effort\_analyze\_setup \<high | ultra\> 来解；但要注意effort 越高用的runtime 越多。
- 在一些case 中，在以上招数都失败后，需要用"remodel -notmapped < modeling option >" 对剩余的点重新建模及匹配。
- 如果上述所有招式都用完，还是有notmapped 点，就先run 一次compare 以确定是否有假的『老大难』隐藏其中。
影响：
『老大难』就是那种让父母操心朋友挂念的人，对世界和谐有诸多不良影响。
- Not-mapped 点不会被当做compared 点进行逻辑等效性检查；如果未按如上步骤解决，或努力了仍未解决掉，那比较结果将被标识成"Incomplete".
- 如果Not-mapped 点是其他key points 的扇入，则会导致验证结果失败，即Non-eq.
- 如果比较结果无Non-eq 且可证实真没有对应的点与其匹配，则这类Not-mapped 的点人畜无害可被忽略。
作者：陌上风骑驴
来源：https://mp.weixin.qq.com/s/\_1N5TJ4iYM2VuOps1aR\_vg
作者微信公众号
相关文章推荐
•论形式验证 | KeyPoint
•大牛访谈：DFT一哥老K
更多IC设计技术干货请关注IC设计技术专栏。
