基于SBDD图的布尔匹配  

Boolean Matching Using SBDD

作　　者：张镭[1] 吕宗伟[1] 林争辉[1] 

机构地区：[1]上海交通大学大规模集成电路研究所,上海200030

出　　处：《计算机辅助设计与图形学学报》2001年第7期582-585,共4页Journal of Computer-Aided Design & Computer Graphics

基　　金：美国国家科学基金(5 978East Asia and Pacific Program -96 0 2 485 )资助

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

关 键 词：OBDD SBDD图 布尔匹配 数字系统 有序二叉判定图 

分 类 号：TP271.82[自动化与计算机技术—检测技术与自动化装置]