【摘要】 在逻辑验证和综合中 ,布尔匹配利用有序二叉判定图 OBDD来检验两个给定的逻辑函数是否相等 .为了提高匹配算法的效率 ,文中用最小项数作为标签标定变量 (变量组 ) .对比两函数中变量 (变量组 )的“标签”,可以删除不可能的排序 ,从而加快匹配过程 .在提取变量标签时 ,提出简约二分决策图—— SBDD,并利用其节点少的特性进一步提高“标签”提取算法的效率 .实验结果表明本算法执行速度快 ,变量区分能力强更多还原

【Abstract】 In logic verification and logic synthesis, Boolean matching is widely used to testify whether two given functions are logically equal by means of OBDD. In order to improve the efficiency of matching algorithm, we count the number of minterms connected with every single variable or variable composition. Treating these numbers as “signature” of variables, algorithm can distinguish variables from each other. Then, impossible orders of variables are pruned during matching and time is saved. For extracting signatures of variables, we put forward SBDD, a new kind of binary decision diagram containing less nodes than OBDD, thus accerlating the extraction of signature. Experiments show that our algorithm reduces execution time.更多还原