逻辑等价性检查（LEC）基础知识介绍

逻辑锥Logic Cone

从数字网表的角度来看，可以把设计分成若干个“以DFF为终点的逻辑块”，如下图。

DFF的CK（时钟）、Ｄ（数据）、RN（复位）、SN（置位）就是这个“逻辑块”的终点，它们的输入都是一个组合逻辑。

时钟和复位很可能是clock tree或者buffer tree，也可能有与门、或门、异或门、选择器等稍复杂的逻辑。

（图一）

如果设计（module）是组合逻辑输出，也可想象在设计外面有一个DFF，如下图。

（图二）

而这些组合逻辑的输入是什么呢？不外乎两种情况：一是，前一级DFF的输出；二是，设计（module）的输入pin。

（图三）

那跨模块优化的又是什么情况呢？如下图，组合逻辑分到了两个模块里。但如果忽略设计的层次关系，两段组合逻辑可以合并成一段。

好处是：综合工具可以两段组合逻辑一起考虑，看有没有逻辑可以复用，所以面积和时序会优化得更好。坏处是：模块的端口可能不存了，也可能产生了新的端口。

所以综合和LEC的选项ungroup（flatten）就是这个作用，让工具忽略层次关系。

（图四）

因此，设计（module）就是“以DFF为终点的逻辑块”组成。不仅网表如此，RTL也是一样。

我们知道所有数字电路都可以用always和assign这两种语法来实现（latch可以看作是DFF的一种）。

这些“以DFF为终点的逻辑块”我们把它叫作逻辑锥。

Keypoint Mapping

有了逻辑锥的概念后，关键点映射（keypoint mapping）就好理解多了。

从上文知道逻辑锥的终点是DFF的CK（时钟）、Ｄ（数据）、RN（复位）、SN（置位），如果这几个“关键点”的逻辑都相同或者等价，那么这两个逻辑锥的逻辑就等价。

对于组合逻辑直接输出的逻辑锥来说，“关键点”就是output pin。那么，总结一下“关键点”有以下几种：

DFF的输入（CK、Ｄ、RN、SN）

顶层模块的输出pin  

要检查等价性，那么keypoing mapping是前提，是基础。如果keypoing mapping都错了，等价性检查结果一定Fail。  

对于要对比的两个设计，我们通常叫作golden和revised（S家叫reference和implement）。golden可能是RTL、综合网表，也可能是APR网表，ECO网表，不是绝对的，只是表明以此设计作为基准来对比。

所以在做等价性检查时golden和revised弄反了也问题不大。但是S家的工具依赖svf（setup verification file），所以还是要注意一下。  

当修改RTL或者网表ECO后，逻辑锥的“关键点”可能发生较大的变化，比如：

新加DFF

删掉DFF

DFF改名

复位变成置位

上升沿变下降沿

还可能DFF从模块A挪到模块B

寄存器合并

寄存器复制

multi bit寄存器  

所以，keypoint mapping时，要能够考虑到这些情况。可以手工分析，也可以参考综合的svf文件，还可以用一些算法来测试和分析。

形式验证

在关键点（keypoint）映射正确后，就可以开始做形式验证了。

如果逻辑锥的输入不一致，例如下图中修改后的设计中增加了输入4和5，就需要分析这两个新增加的输入是不是与golden的输入是等价或者反相等价的关系。

如果没有任何关系，纯粹是新加的条件，那么这两个逻辑锥一定会fail。  

（图五）

经过上一步对逻辑锥输入的检查后，接下来就需要通过数学的方法来检查等价性。

这种数学的方法的原理很简单，如下，每个keypoint的逻辑都可以用下面的公式来描述： Y = F(a, b, c, ... , n) 对golden和revised逻辑锥施加相同的测试向量，看是否有相同的输入。

理论上，对于有N个输入的keypoing，一共有2^N种输入可能性。遍历一下，就知道等价性的结果。  

如果其中有一个测试向量fail，那么这个keypoint就不等价，剩余的测试向量也就没有必要继续。如果都pass，就需要遍历完所有的测试向量。  

为了节省测试时间，LEC工具需要对逻辑锥进行优化。现在市场上已经出现一些基于机器学习（Machine Learning）和深度学习（deep learning）的形式验证算法的LEC工具。

审核编辑：刘清