基于状态转换图同构求解的等价性验证算法

Verifying Algorithm of Equivalence Based on State Transfer Graph's Isomorphism Solving

文中提出了一种基于状态转换图同构求解的时序电路等价性验证算法。算法将两时序电路的等价性问题转化为验证相应状态转换图的同构性。首先将初始状态对匹配为待验证对,然后采用递归的方法验证以初始状态对的下一状态对为初始状态的子状态转换图是否同构,从而得到时序电路是否等价的信息。若两状态转换图同构,则两图中的状态均可一一配对为待验证状态对,即所有的代验证状态对均为等价状态对。该方法可以有效地克服算法级描述到底层实现之间跨度太大的问题。

Present a sequential circuit＇s equivalence verifying algorithm, which is based on the graph＇s isomorphism solving. Adopt recursive method to verify whether all the sub-STG（state transfer graph） is isomorphic, thus can obtain some information about sequential circuits＇ equivalence. If the state transfer graphs are isornorphism, all the states in different graphs can be matched as equal state pairs. The method based on STG can effectively overcomes the big span from algorithm-level description to low-level implementation.