This browser does not support music or audio playback. Please play it in Weixin or another browser. 北区楼四 刘昊霖 许久未更新技术文章，今天继续论述形式验证，温故：《论形式验证 | LEC Jumpstart》《论形式验证 | 撸 LEC flow》《论形式验证 | KeyPoint》《论形式验证 | Keypoint mapping》《论形式验证 | KeyPoint Mapping status》，知新：Diagnosing unmapped key points.
上一篇文章论述了做完map 之后，根据map 结果对key points 的分类，本文论述如何对unmapped key points 进行诊断。
在map 完后，如果有unmappped key points, 可以用命令 "report\_unmapped\_points" 加不同的option 来报每一种unmapped key points, 对于option -unreachable 有两个子选项可以分别根据造成unreachable 的原因进一步细分。
举例：
可以用命令"report\_gate -unreach" 来进一步确认是哪个fanout gate 造成了unreachable, LEC 会从unreachable key point 开始往后trace 一直到造成unreachable 的点。
举例：
对于Extra key point, 首先要确认其是否是真的Extra, 是否可以通过设置为其找到配对。如果用命令 "add\_pin\_constraints" 对Extra 的primary input 做了常值约束，则这些被约束的点将不再被归类到 "Extra key point", 至于是否可以加这样的约束需要designer 进行确认。如果某些Extra primary output 在function 模式下无用，则可以如果用命令 "add\_ignored\_outputs" 对其进行设置，如scan\_out.
对于Not-mapped key points, 首先要确认是否由于renaming 造成，如果是，确认是否可以通过命令"add\_renaming\_rule" 加renaming rule 予以解决；然后要确认是否由于modeling 不全或不当造成，如果是，可以用命令 "set\_flatten\_model" 设置对应的modeling option. 通常会在map 之前设置 "set\_analyze\_option -auto" 让LEC 在map 的过程中自动enable 常用的modeling option. 也可以用命令"analyze\_setup" 来分析。
可以用命令"remodel -notmapped "
来限制使用哪些modeling option.
通常建议先用命令"set\_flatten\_model" 做全局设置，如果map 后仍有not-mapped point 再尝试使用命令"remodel".
可以用命令"analyze\_redundancy" 来分析一个Seqential cell 是否是冗余cell.
可以用命令"analyze\_gate" 来分析not-mapped key points 是否是常值寄存器，它会报出被分析的点是否为常值，同时也会去trace 该key points 的fanin 是否有常值的spport key point. 如下例所示：
本文列出了debug unmapped key points 常用的方法，高亮了所用到的命令，对于每个命令在LEC 中用"man command-ID -verbose" 可以得到所有可用的option 及对应的释义。百闻不如一见，百读不如一试，动起手来。
作者：陌上风骑驴
来源：https://mp.weixin.qq.com/s/Tw0LmXcibf04qGyyBIvLhQ
作者微信公众号
相关文章推荐
•论功耗：低功耗检查
•Innovus Mixed Placer
更多IC设计技术干货请关注IC设计技术专栏。
