功能ECO理论基础:逻辑等价性检查

描述

逻辑锥Logic Cone

从数字网表的角度来看,可以把设计分成若干个“以DFF为终点的逻辑块”,如下图。DFF的CK(时钟)、D(数据)、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(时钟)、D(数据)、RN(复位)、SN(置位),如果这几个“关键点”的逻辑都相同或者等价,那么这两个逻辑锥的逻辑就等价。对于组合逻辑直接输出的逻辑锥来说,“关键点”就是output pin。那么,总结一下“关键点”有以下几种:DFF的输入(CK、D、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删掉DFFDFF改名

复位变成置位上升沿变下降沿还可能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工具。

审核编辑:符乾江
打开APP阅读更多精彩内容
声明:本文内容及配图由入驻作者撰写或者入驻合作网站授权转载。文章观点仅代表作者本人,不代表电子发烧友网立场。文章及其配图仅供工程师学习之用,如有内容侵权或者其他违规问题,请联系本站处理。 举报投诉

全部0条评论

快来发表一下你的评论吧 !

×
20
完善资料,
赚取积分