一种形式验证比较点匹配方法、系统、处理器及存储器

摘要

本发明公开了一种形式验证比较点匹配方法、系统、处理器及存储器，该方法包括：接收待验证的时序电路的参考电路模型和实现电路模型；控制参考电路模型和实现电路模型待匹配的比较点的测试向量随机生成，使得参考电路模型和实现电路模型的比较点的输出值可进行二叉树匹配；基于二叉树匹配对参考电路模型的待匹配的各比较点的输出值与实现电路模型的待匹配的各比较点的输出值进行匹配，直至参考电路模型和实现电路模型所有比较点全部一一匹配成功，则验证成功；若存在参考电路模型和实现电路模型待匹配的比较点匹配失败，则验证失败。本发明降低了时序电路等价检验过程中对应比较点的匹配复杂度，降低了匹配时间，降低了内存的消耗。