有序二叉决策图在防火墙规则库设计中的应用

在防火墙规则库的设计中利用有序二叉决策图（ordered binary decision diagram，OBDD）来表示防火墙的访问控制规则集，改变了传统的顺序存储规则的规则库设计方法，以增加预处理时间为代价，有效地提高了规则的匹配速度，从而提高了防火墙的性能及其安全性．     

An asymptotically optimal lower bound on the OBDD size of the middle bit of multiplication for the pairwise ascending variable order

We prove that each OBDD (ordered binary decision diagram) for the middle bit of n-bit integer multiplication for one of the variable orders which so far achieve the smallest OBDD sizes with respect to asymptotic order of growth, namely the pairwise ascending order x₀,y₀,…,x_n−1,y_n−1, requires a size of Ω(2^(6/5)n). This is asymptotically optimal due to a bound of the same order by Amano and Maruoka (2007) [1].     

A Binary Decision Diagram based on-line testing of digital VLSI circuits for feedback bridging faults

Classical manufacturing test verifies that a circuit is fault free during fabrication, however, cannot detect any fault that occurs after deployment or during operation. As complexity of integration rises, frequency of such failures is increasing for which on-line testing (OLT) is becoming an essential part in design for testability. In majority of the works on OLT, single stuck at fault model is considered. However in modern integration technology, single stuck at fault model can capture only a small fraction of real defects and as a remedy, advanced fault models such as bridging faults, transition faults, delay faults, etc. are now being considered. In this paper we concentrate on bridging faults for OLT. The reported works on OLT using bridging fault model have considered non-feedback faults only. The basic idea is, as feedback bridging faults may cause oscillations, detecting them on-line using logic testing is difficult. However, not all feedback bridging faults create oscillations and even if some does, there are test patterns for which the fault effect is manifested logically. In this paper it is shown that the number of such cases is not insignificant and discarding them impacts OLT in terms of fault coverage and detection latency. The present work aims at developing an OLT scheme for bridging faults including the feedback bridging faults also, that can be detected using logic test patterns. The proposed scheme is based on Binary Decision Diagrams, which enables it to handle fairly large circuits. Results on ISCAS 89 benchmarks illustrate that consideration of feedback bridging faults along with non-feedback ones improves fault coverage, however, increase in area overhead is marginal, compared to schemes only involving non-feedback faults.     

Approximating Boolean functions by OBDDs

In learning theory and genetic programming, OBDDs are used to represent approximations of Boolean functions. This motivates the investigation of the OBDD complexity of approximating Boolean functions with respect to given distributions on the inputs. We present a new type of reduction for one-round communication problems that is suitable for approximations. Using this new type of reduction, we improve a known lower bound on the size of OBDD approximations of the hidden weighted bit function for uniformly distributed inputs to an asymptotically tight bound and prove new results about OBDD approximations of integer multiplication and squaring for uniformly distributed inputs.     

OBDD在组合逻辑电路测试中的应用研究

由于的传统的组合电路测试方法,如Ｄ算法、ＰＯＤＥＭ算法和ＦＡＮ算法等,在搜索过程中都不可避免地要进行反射回溯,因此严重地影响了算法的效率。而ＯＢＤＤ是一种表示和操纵布尔函数的有效方法,用ＯＢＤＤ来表示电路中每个节点所代表的逻辑函数,可以把反向回溯过程转换为ＯＢＤＤ的ｓａｔｉｓｆｉａｂｉｌｉｔｙ问题,从而避免了反向回溯过程,加快了故障测试的速度。同时,ＯＢＤＤ在测试矢量集的生成以及ｎｅｃｅｓｓａｒｙ     

一种基于有序二元决策图和布尔函数性质计算网络可靠性的算法

有序二元决策图(OBDD)被广泛用到网络可靠度的计算中,在基于OBDD计算网络可靠度时,其计算时间主要取决于参与操作的OBDD的大小,而OBDD的大小严重依赖于OBDD的变量序。该文根据布尔函数的性质和OBDD原理提出一种优化计算网络可靠性的算法(BF-OBDD),提高计算网络可靠性的效率。实验结果表明改进的算法有较少的 OBDD节点数量,在计算网络可靠性时,花费的时间较少。     

Performance assessment and reliability analysis of dependable and distributed computing systems based on BDD and recursive merge

System reliability evaluation, sensitivity analysis, failure frequency analysis, importance measures, and optimal design are important issues that have become research topics for distributed dependable computing. Finding all of the Minimal File Spanning Trees (MFST) and avoiding repeatedly computing the redundant MFSTs have been key techniques for evaluating the reliability of a distributed computing system (DCS) in previous works. However, identifying all of the disjointed MFSTs is difficult and time consuming for large-scale networks. Although existing algorithms have been demonstrated to work well on medium-scale networks, they have two inherent drawbacks. First, they do not support efficient manipulation of Boolean algebra. The sum-of-disjoint-products method used by these algorithms is inefficient when dealing with large Boolean functions. Second, the tree-based partitioning algorithm does not merge isomorphic sub-problems, and therefore, redundant computations cannot be avoided. In this paper, we propose a new efficient algorithm for the reliability evaluation of a DCS based on the recursive merge and the binary decision diagram (BDD). Using the BDD substitution method, we can easily apply our algorithm to a network with imperfect nodes. The experimental results show a significant improvement in the execution time compared to previous works.     

Representation of graphs by OBDDs

Recently, it has been shown in a series of works that the representation of graphs by Ordered Binary Decision Diagrams (OBDDs) often leads to good algorithmic behavior. However, the question for which graph classes an OBDD representation is advantageous, has not been investigated, yet. In this paper, the space requirements for the OBDD representation of certain graph classes, specifically cographs, several types of graphs with few P₄s, unit interval graphs, interval graphs and bipartite graphs are investigated. Upper and lower bounds are proven for all these graph classes and it is shown that in most (but not all) cases a representation of the graphs by OBDDs is advantageous with respect to space requirements.     

基于算术方法的高层次匹配算法

在数字集成电路设计过程中，为了实现巳有组件的复用，文章提出了一种基于多项式表示法的组件匹配算法。通过要求实现功能的多项式表示式与巳有组件库的多项式表示式两者的对比，使系统的抽象系统的算法级得到综合。     

PSL的有界模型检验

 基于SAT的有界模型检验被视为是基于OBDD的符号化模型检验技术的重要补充,是并行反应式系统的一种有效验证方法.然而,直至现在,有界模型检验已验证的属性逻辑还十分有限.PSL是一种用于描述并行系统的属性规约语言(IEEE-1850),包括线性时序逻辑FL和分支时序逻辑OBE两部分.通过模型检验可验证系统的PSL属性,本文提出了PSL的有界模型检验方法及其算法框架.首先,定义PSL逻辑的有界语义,而后,将有界语义进一步简化为SAT,分别将PSL性质规约公式和系统M的状态迁移关系转换为SAT命题公式,最后验证上述两个SAT命题公式合取式的可满足性,这样就将时序逻辑PSL的存在模型检验转化为一个命题公式的可满足性问题,并用一个队列控制电路实例具体解释算法执行过程.