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_xixj = f_xjxi is used to detect symmetry variables. After setting up two BDDs according to f_xixj and f_xjxi, 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.