LEC 功能ECO理论基础：逻辑等价性检查 _lec

逻辑锥Logic Cone
从数字网表的角度来看，可以把设计分成若干个“以DFF为终点的逻辑块”，如下图。DFF的CK（时钟）、Ｄ（数据）、RN（复位）、SN（置位）就是这个“逻辑块”的终点，它们的输入都是一个组合逻辑。时钟和复位很可能是clock tree或者 tree，也可能有与门、或门、异或门、选择器等稍复杂的逻辑。
（图一）
如果设计（）是组合逻辑输出，也可想像在设计外面有一个DFF，如下图。
（图二）
而这些组合逻辑的输入是什么呢？不外乎两种情况：一是，前一级DFF的输出；二是，设计（）的输入pin 。
（图三）
那跨模块优化的又是什么情况呢？如下图，组合逻辑分到了两个模块里。但如果忽略设计的层次关系，两段组合逻辑可以合并成一段。好处是：综合工具可以两段组合逻辑一起考虑，看有没有逻辑可以复用，所以面积和时序会优化得更好。坏处是：模块的端口可能不存了，也可能产生了新的端口。所以综合和LEC的选项（）就是这个作用，让工具忽略层次关系。
（图四）
因此，设计（）就是“以DFF为终点的逻辑块”组成。不仅网表如此，RTL也是一样。我们知道所有数字电路都可以用和这两种语法来实现（latch可以看作是DFF的一种）。这些“以DFF为终点的逻辑块”我们把它叫作逻辑锥。
有了逻辑锥的概念后，关键点映射（）就好理解多了。从上文知道逻辑锥的终点是DFF的CK（时钟）、Ｄ（数据）、RN（复位）、SN（置位），如果这几个“关键点”的逻辑都相同或者等价，那么这两个逻辑锥的逻辑就等价。对于组合逻辑直接输出的逻辑锥来说，“关键点”就是 pin 。那么，总结一下“关键点”有以下几种：
要检查等价性，那么是前提，是基础。如果都错了，等价性检查结果一定Fail 。
对于要对比的两个设计，我们通常叫作和（S家叫和）。可能是RTL、综合网表，也可能是APR网表，ECO网表，不是绝对的，只是表明以此设计作为基准来对比。所以在做等价性检查时和弄反了也问题不大。但是S家的工具依赖svf（setupfile），所以还是要注意一下。
当修改RTL或者网表ECO后，逻辑锥的“关键点”可能发生较大的变化，比如：

文章插图
所以，时，要能够考虑到这些情况。可以手工分析，也可以参考综合的svf文件，还可以用一些算法来测试和分析。
形式验证
在关键点（）映射正确后，就可以开始做形式验证了。如果逻辑锥的输入不一致，例如下图中修改后的设计中增加了输入4和5，就需要分析这两个新增加的输入是不是与的输入是等价或者反相等价的关系。如果没有任何关系，纯粹是新加的条件，那么这两个逻辑锥一定会fail 。
（图五）
经过上一步对逻辑锥输入的检查后，接下来就需要通过数学的方法来检查等价性。这种数学的方法的原理很简单，如下，每个的逻辑都可以用下面的公式来描述：
Y = F(a, b, c, ... , n)
对和逻辑锥施加相同的测试向量，看是否有相同的输入。理论上，对于有N个输入的，一共有2^N种输入可能性。遍历一下，就知道等价性的结果。
如果其中有一个测试向量fail，那么这个就不等价，剩余的测试向量也就没有必要继续。如果都pass，就需要遍历完所有的测试向量。
【LEC功能ECO理论基础：逻辑等价性检查】为了节省测试时间，LEC工具需要对逻辑锥进行优化。现在市场上已经出现一些基于机器学习（）和深度学习（deep ）的形式验证算法的LEC工具。