递归学习寻找对称变量

Recognizing Symmetric Variables Using Recursive Learning

逻辑验证和逻辑综合中 ,利用对称变量的性质能提高算法整体的效率 .通常 fxixj=fxjxi被用来检验变量的对称性 .一般先分别建立 fxixj和 fxjxi的 BDD( Binary Decision Diagram)二分决策图 ,然后通过检查两 BDD图是否同构来验证 fxixj=fxjxi.但将电路转化为 BDD图本身就需要一定的时间 ,而且对于大的电路 ,存在 BDD图不能建立的可能性 ,致使同构验证无法进行 .本文利用递归学习 ,无需建立 BDD图直接在电路拓扑图上验证 fxixj=fxjxi.递归学习算法执行效率高 ,可以大大缩减对称变量检测的过程 .试验结果表明 ,利用递归学习算法检测对称变量执行时间减少 ,并且能将大的电路作为检测对象 .

In logic synthesis and verification, information of symmetry variables can improve algorithms' efficiency. As usual, f x i j =f x j i is used to detect the symmetry variables. After building two BDDs (Binary Decision Diagrams) according to f x i j and f x j i ,one can say these two variables are symmetry if the two BDDs are isomorphic. But BDD is sensitive to the order of variables and sometimes it can not be built because of its enormously big size. In this paper, recursive learning is used to detect symmetry variables without building BDD. Recursive learning runs with high efficiency, which is helpful to reduce the detecting time. The results show that the recursive learning can run in less time and deal with big circuits where BDD can not be built.