摘要
逻辑验证和综合中 ,布尔匹配利用有序二叉判定图 (Ordered Binary Decision Diagram,OBDD)检验两个给定的逻辑函数是否相等 .直接枚举每个函数中输入变量的各种排列顺序 ,并根据这些顺序进行匹配 ,算法时间复杂度为 O(n!2 n2 ) ,n为变量数 .为了提高匹配算法的效率 ,文中用最小项数目作为标签标定变量 (变量组 ) .对比两函数中变量 (变量组 )的标签 ,可删除不可能的排序 ,加快匹配过程 .在此基础之上 ,利用重构将待匹配变量压缩在 OBDD图的底部 .利用这部分结构可以进一步区分变量 .实验结果表明 ,该算法不仅变量区分能力要好于其他算法 ,且执行速度快 。
In logic verification and logic synthesis, Boolean matching is widely used to testify whether two given function is logically equal by means of OBDD. Without any pretreatment, the time complexity of matching algorithm is O(n!2 n2) in the light of all the possible orders of variables, where n is the number of variables. In order to improve the efficiency of matching algorithm, the numbers of minterms connected with every single variable or every variable composition are used as “signature” of the variables. The impossible orders of variables are pruned during matching and time is saved. This paper introduced a new method to distinguish variables, which reduces variables unrecognized to the bottom of OBDD by restructuring. According to those parts of OBDD, variables can be efficiently recognized. The experiment results show that the algorithm in this paper can distinguish variables in some complex circuits while others can't.
出处
《上海交通大学学报》
EI
CAS
CSCD
北大核心
2002年第3期319-322,共4页
Journal of Shanghai Jiaotong University
基金
美国国家科学基金资助项目 ( 5 978East Asia andPacific Program -96 0 2 485 )
