时序电路等价验证的触发器匹配

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

Flip-flops Matching for Sequential Equivalence Checking

Generally, sequential equivalence circuit checking is to expand the sequential circuit into combinational circuit for verification. While in two sequential circuit to be verified, flip-flops is correspondent, identifying and matching corresponding flip-flops in the two sequential circuits to be verified is proved greatly effective. This paper builds a new miter circuit for Automatic Test Pattern Generation (ATPG) module, and then uses Boolean Satisfiability (SAT) tools to solve the Boolean function with timing frame unrolling transmission. Meanwhile, this method improves the SAT tool of information learning to accelerate the calculation process. Results on industrial- sized circuits ISCAS89 show these methods are both practical and efficient.