论文部分内容阅读
通常的时序电路等价性验证方法是将触发器按时序展开，从而将时序电路转化为组合电路进行验证。而一般在待验证的两个时序电路中，触发器是一一对应的，找到触发器的对应关系，时序电路的验证就会得到很大的简化。该文通过一种新的基于布尔可满足性（SAT）算法的自动测试模式生成（ATPG）匹配模型建立联接电路，使用时序帧展开传递算法比较触发器的帧时序状态输出，同时在SAT解算中加入信息学习继承等启发式算法，将时序电路的触发器一一匹配。在ISCAS89电路上的实验结果表明，该文算法在对触发器的匹配问题上是非常有效的。