| 主权项 |
一种数字硬件电路逻辑错误诊断方法，其特征在于是这样实现的：步骤一：过滤候选区域根据候选错误区域的内部特点，利用结构相似性有选择地去掉一些候选区域。从选出的候选区域中找到等价的区域对，即可能等价的区域对，可以采用拓扑排序的方法，即按扇入优先的次序排序，这样可以使以前推导出来的内部等价性能够为后面的等价性推导过程所用，即通过等价区域置换来简化miter电路。该方法的核心步骤是，利用增量可满足性算法，按拓扑排序依次验证所有候选区域的等价性或证明他们是不等价的。如果一个区域f是一个已经证明不包含错误的区域，在该区域设置一个标志x，该标志的输出为1，另一个候选区域为g，把g区域的输出与x连接到一个异或门y上，如果结点y恒为0，说明其相应的CNF公式是不可满足的，那么f和g是等价的，可以把g区域从候选列表中删除。使用该方法可以快速过滤一部分的候选区域。步骤二：随机模拟使用随机模拟的方法，同时对两个电路进行随机模拟，然后比较两个电路中各结点的响应特征，具有相同特征或者相反特征的结点作为候选节点，加入一个候选表中。获取候选结点的多少严重影响算法的性能，如果候选结点太多，会导致SAT程序的频繁调用，如果候选结点太少，则可能因为缺少等价结点的置换而导致miter太大，使SAT程序无法正常运行。并且如果候选结点太少，也可能漏掉一些可能包含错误的区域。步骤三：排除候选结点采用基于SAT的方法排除候选结点，发现区域外部有错误，那么该区域被排除，算法结束，如果没有发现候选区域的外部有错，那么调用SAT的布尔比较进行检查，这时可将候选区域当作一个黑盒，并使用两个布尔变量来表示每个受黑盒输出影响的电路信号，然后构造相应的CNF公式。如果该公式是可满足的，那么说明这个区域外部存在错误，可以把它从候选区域列表中删除，否则将它保留在候选区域表中。 |
