高级检索

利用不等BDD检测对称变量

Detecting Symmetry of Variables Using Unequal BDD

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

     

    Abstract: In logic synthesis and verification, information of symmetry variables can improve algorithms' efficiency. It is well known that fxixj = fxjxi is used to detect symmetry variables. After setting up two BDDs according to fxixj and fxjxi, 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.

     

/

返回文章
返回