基于可满足性的组合电路等价性检验方法

摘要

本发明涉及超大规模集成电路设计验证技术领域，特别是组合电路的形式验证方法——等价性检验方法。该方法是以可满足性算法为引擎，增量地验证整个电路设计，所述方法具有两个阶段，第一阶段是确定两个电路内部的候选等价信号，并通过电路结构分析，对候选等价信号作静态筛选，第二阶段是通过子句分组实现增量可满足性方法，并验证每对候选信号的等价性。其主要特点在于：1)通过电路结构分析对电路内部的候选等价信号进行筛选，在验证过程中则动态地选择分割集中的等价信号，保证分割集中信号是相互独立的。2)通过对子句进行分组，来实现增量的可满足性算法，节省计算资源，提高算法性能和处理能力。

主权项

1、一种基于可满足性的组合电路等价性检验方法，其特征在于，第一步对两个电路进行分级处理；第二步确定两个电路的候选等价信号；第三步通过电路结构分析，筛选候选等价信号；第四步按照扇入优先次序验证各候选等价信号的等价性；最后一步检查各对候选原始输出信号是否等价，具体步骤如下：S1：对被验证的两个电路进行分级处理，原始输入信号是第0级，其它任意的非原始输入信号a的分级为l(a)＝b{max(l(b))+1，b是a的扇入信号}，然后，将所有电路信号按所在分级从小到大顺序排列；S2：找出两个被验证电路的内部候选等价信号，首先使用相同的随机向量对两个电路同时作并行模拟，存储各电路信号的响应特征，然后对规范电路中的各个信号按第S1步的排列次序遍历，对于任意信号a，如果实现电路中的某个信号b与信号a名称匹配或模拟响应特征相同，那么信号b为信号a的一个候选等价信号；S3：对上一步得到的候选等价信号进行静态筛选，遍历规范电路中的各个信号，进行下列电路结构分析：1)如果信号a的扇入数少于2，那么从候选表中删除所有包含信号a的候选等价信号对；2)如果信号a的某个候选信号依赖的原始输入个数比a多，那么删除该候选信号对；S4：按扇入优先的次序，调用增量可满足性算法验证每一对候选信号的等价性，该算法使用了两个主要策略：动态选择分割集合，增量验证候选信号对的等价性；通过子句分组来实现增量的可满足性算法，具体过程如下：1)构造实现电路的合取范式公式，作为永久子句组，避免重复构造相同信号的合取范式公式；2)动态调整分割集合中的候选等价信号，对于每对候选信号(a，b)，假定a是规范电路中的信号，b是实现电路中的信号，构造ab的合取范式公式，对于a的扇入逻辑锥作深度优先搜索，直到遇到原始输入或已知的等价信号为止，称这些信号为一个分割集合，基于上述的分割集合，如果得到的CNF公式不可满足，那么a与b是等价的；否则，需要进一步确定是否误判，这时对分割集中的信号继续深度优先搜索，重复上述构造合取范式公式的过程，在分割集中只包含原始输入信号的情况下，为了尽量避免误判的发生，在每次得到的分割集中，如果某个信号是另一信号的扇出信号，那么把该信号从分割集中删除，保证分割集中各信号是相互独立的；3)使用增量可满足性算法验证每对候选信号的等价性，如果一对候选信号a和b是等价的，那么用b置换a，这时要增加相应的表示等价关系的子句，并加入永久子句组，最后，删除表示信号a及ab的合取范式子句组，并且与a对应的其它候选信号对不必再验证，然后验证剩余的每对候选等价信号；S5：检查每一对原始输出信号是否等价，如果是，则两个电路等价，否则不等价。