简化BDD的SBDD和变量重排序结合算法  

A Technique for Reordering Variables in an SBDD to Reduce the Size of BDD

作　　者：李绍荣[1] 徐琳琳[1] 

机构地区：[1]电子科技大学光电信息学院,成都610054

出　　处：《计算机科学》2007年第4期287-288,共2页Computer Science

基　　金：(No.TDXX0502)获得铁道部"铁路信息科学与工程"开放实验室/北京市"现代信息科学与网络技术"重点实验室科学基金资助

摘　　要：二叉判定图是一种基于图表的用来表示布尔函数的数据结构。它泛广地应用于计算机半辅助设计和数字电路的形式化验证中。本文主要研究如何存储和如何简化BDD。提出了一种把SBDD和变量重排序结合在一起的新算法,用来简化BDD的大小。Binary Decision Diagram is a graph-based data structure for representing Boolean function. They have found widespread use in computer-aided design and in formal verification of digital circuits. We mainly investigate how to store BDD and to reduce the size of BDD. Firstly, we mainly introduce some background knowledge about Binary Decision Diagrams （BDD） in this paper. Secondly, we describe the ITE algorithm Finally, we provide a technique for reordering variables in an SBDD to reduce the size of BDD.

关 键 词：布尔函数 形式化验证 二叉判定图 变量重排序 共享BDD 

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