利用不等BDD检测对称变量

变量的对称性在逻辑综合与优化，工艺映射中起着非常重要的作用。如果事先得到变量对称的信息，就可以减少解空间，提高逻辑验证的效率，过去，人们通常用公式fxix↑-j=fxjx↑-i检验变量的对称性，这需要分别建立fxix↑-j和fxjx↑-i的BDD图，然后检查两BDD图是否同构，文中提出一种新算法，整个算法流程仅需建立一次BDD，任何变量对称性的判别遍历BDD一次即可完成，从而减少了算法的空间复杂度和时间复杂度。

Detecting Symmetry of Variables Using Unequal BDD

In logic synthesis and verification, information of symmetry variables can improve algorithms' efficiency. It is well known that f x i j =f x j i is used to detect symmetry variables. After setting up two BDDs according to f x i j and f x j i , one can say these two variables are symmetry if two BDDs are isomorphic. In this paper, a novel algorithm is provided. Only one BDD is built while checking if two variables are symmetry. So, both space complexity and time complexity are reduced. And the experiment results show that our algorithm can reduce runtime greatly.