一种基于状态转换图的时序电路等价验证算法

A Sequential Equivalence Checking Algorithm Based on State Transfer Graph

提出一种基于状态转换图的时序电路等价验证算法。此算法通过验证两时序电路的状态转换图是否同构,得到两电路是否等价的信息。若两状态转换图同构,则两图中的状态可一一匹配为等价状态对,算法将状态转换图存储为待验证等价状态对的形式,若所有待验证等价状态对均为等价,则两时序电路等价,反之,则不等价。此算法对ISCAS89测试电路进行验证,与基于BDD方法的SIS系统和基于时间帧展开算法相比,均有较好的结果。

A sequential equivalence checking algorithm based on state transfer graph is presented. The state transfer graphs＇ isomorphism is checked to see the corresponding circuits＇ equivalence. If the two state transfer graphs are isomorphic, the states in two different graphs can be matched as equal state pairs. The algorithm presented stores the state transfer graph as state pairs. If all the state pairs stored are checked to be equal, the two circuits have the same sequential behavior. Experiments on ISCAS89 circuits show that the presented algorithm has a promising elapsed time comparing to the algorithm based on BDD and frame expansion.