加速布尔匹配算法的研究

逻辑验证和综合中，布尔匹配利用有序二叉判定图（Ordered Binary Decision Diagram,OBDD)检验两个给定的逻辑函数是否相等。直接枚举每个函数中输入变量的各种排列顺序，并根据这些顺序进行匹配，算法时间复杂度为O(n!2^n2),n为变量数。为了提高匹配算法的效率，文中用最小项数目作为标签标定变量（变量组）。对比两函数 中变量（变量组）的标签，可删除不可能的排序，加快匹配过程。在此基础之上，利用重构将待匹配变量压缩在OBDD图的底部。利用这部分结构可以进一步区分变量。实验结果表明，该算法不仅变量区分能力要好于其他算法，且执行速度快，更具实用价值。     

在数字电路验证中使用模型检验

形式化方法作为仿真方法的补充,为电路功能验证提供了新的途径.介绍了形式化验证方法之一,模型检验的理论基础和实现方法.介绍了分支时态逻辑CTL、CTL的固定点算法,二元决策图BDD,以及符号模型检验方法.最后使用SMV工具在一个CISC处理器的存储管理单元(MMU)上应用了模型检验,验证了模型检验在模块级验证中的可行性.     

基于同构子网判定的结点不可靠网络可靠度计算方法

 为提高结点不可靠网络的可靠度计算效率,提出一种基于子网同构判定的高效计算方法。在生成有序二元决策图（OBDD）的因子分解过程中,利用特征合并划分（CMP）识别网络分解产生的同构子网,然后根据网络中边和节点的逻辑联系,执行边替换操作将不可靠结点存储于OBDD;通过遍历OBDD 计算网络的可靠度。结果显示,该方法减少了同构子网带来的重复计算,并充分利用OBDD 的存储结构进一步增强了计算效率,计算中小型网络可靠度的时间保持在100 s 以下,计算数百结点网络可靠度的时间保持在百秒级,且计算中大型网络的开销远低于标准二元决策图（BDD）方法。     

对称检测算法的研究

对称是逻辑综合，逻辑优化以及映像技术领域中一个非常重要的性质，对于对称函数，可以使用特殊的逻辑综合程序来改进设计结果，使用对称也可以提高映像技术和等价检测的有效性，提出一种用于OBDD布尔函数对称性检测的精确有效的算法。     

可能性测度下计算树逻辑的若干性质

为讨论可能的计算树逻辑(PoCTL)与计算树逻辑(CTL)的关系,给出PoCTL公式与CTL公式等价的概念,利用公式的等价性证明了CTL是PoCTL的一个真子集.通过PoCTL模型检测算法与PoCTL公式的分析,解决了PoCTL模型检测的时间复杂度问题.最后对重复事件与持久性事件的定性性质及定量性质进行研究,用实例验证了CTL公式与PoCTL公式在可能性测度与概率测度下的本质区别.     

测控技术中含有"X"值的验证

利用模型检验技术来验证具有“X” （未知）值的属性.给出了三值（真、假、未知）逻辑公式的模型检验算法,此算法与二值逻辑模型检验算法相比,并没有增加时间复杂度.通过实例说明三值逻辑模型检验算法的应用.     

基于OBDD的描述逻辑ALCIO判定算法

给定描述逻辑ALCIO中的任一知识库,应用NNF变换和FLAT规则对其进行预处理,通过一个重构过程将知识库中TBox模型转化为布尔函数,然后将布尔函数转换为有序二叉决策图(OBDD)表示形式,从而调用已有的OBDD软件包进行可满足性判定,实现描述逻辑ALCIO的判定算法。该算法在实现描述逻辑的推理方面与经典的Tableau判定算法在性能上可以相互弥补和配合。     

HLA-A2限制性CTL表位肽定量构效关系研究

基于SCORE打分函数，运用定量构效关系的理论和方法研究了HLA—A2限制性CTL表位九肽结构与亲和性间的定量关系，并建立了SCORE得分与亲和性的定量关系模型，并用外部样本（5个HLA—A2限制性CTL表位九肽）作为预测集用于检验模型的预测能力．基于SCORE打分函数建立的定量模型具有较好的相关性（r=0，9165，RMS=0．38）和对外部样本的预测能力（rpred=0．9847，RMS=0．135）．基于SCORE打分函数，运用定量构效关系研究的理论和方法建立了HLA—A2限制性CTL表位亲和性的定量预测方法，为实验鉴定高亲和性HLA—A2限制性CTL表位提供了理论依据．     

安全计算机平台测试序列的生成与优化

基于模型检验的测试序列生成及优化方法,在描述符号模型检验原理和CTL(计算树逻辑,Computation Tree Logic)覆盖标准的基础上,通过分析测试序列的覆盖范围,证明了测试序列的覆盖完整性,并生成和优化了安全计算机平台测试序列.     

模糊交互时态逻辑及其语义结构

Alur等人建立的交互时态逻辑（ATL ＊）是一种重要的多Agent合作逻辑,它对计算树逻辑（CTL ＊）进行了合作算子拓展,然而它缺乏对不确定时态信息的刻画。通过考察模糊时态事件和模糊时态状态、描述相对时间来改进并发博弈结构,并给出模糊并发博弈结构;把模糊并发博弈结构的若干要件从相对时间域到绝对时间域进行映射,给出已映射模糊并发博弈结构;建立了模糊交互时态逻辑（FATL ＊）,给出其语法,在已映射模糊并发博弈结构下给出其语义;阐述了FATL ＊的表达力比ATL ＊强。     

计算K-终端网络可靠度的一种新算法

讨论了由一个源点s到一个指定的点集K的网络可靠度问题。首先提出了两个网络门限变量化简原则及计算网络K-树和极小K-割的算法。然后,基于具有门限变量的布尔方程和有序二分决策图方法,给出网络K-终端可靠度算法。结果表明这种算法是有效的,改进并推广了Rauzy提出的算法。     

基于布尔代数的功能树简化研究

当前较大规模的功能树存在解空间庞大、冲突定位困难的问题,对此提出基于布尔代数的与或功能树简化方法;证明了收缩简化、删除简化、提取简化的相关定理,并籍此给出其布尔代数的简化算法;最后通过实例,证明该方法可在保持逻辑等价的前提下有效降低问题的复杂度,从而提高设计者进行概念设计的效率.     

频谱技术在布尔函数的多项式逼近中的应用

利用布尔函数的频谱来构造布尔函数的多项式逼近已得到研究。本文分析了这种逼近的构造,给出了不同阶数逼近所引起的误差上界及同阶逼近的等价性。     

分配格的等价关系刻画

通过在格上定义等价关系，给出了分配格，Heyting代数，Boolean代数的一致等价刻画。由此得到了Heyting代数与Boolean代数分解定理．     

Arithmetic Operand Ordering for Equivalence Checking

An information extraction-based technique is proposed for RTL-to-gate equivalence checking. Distances are calculated on directed acyclic graph (AIG). Multiplier and multiplicand are distinguished on multiplications with different coding methods, with which the operand ordering/grouping information could be extracted from a given implementation gate netlist, helping the RTL synthesis engine generate a gate netlist with great similarity. This technique has been implemented in an internal equivalence checking tool, ZD_VIS. Compared with the simple equivalence checking, the speed is accelerated by at least 40% in its application to a class of arithmetic designs, addition and multiplication trees. The method can be easily incorporated into existing RTL-to-gate equivalence checking frameworks, increasing the robustness of equivalence checking for arithmetic circuits.     

原子布尔代数理论的计算复杂性

运用Ｅｈｒｅｎｆｅｕｃｈｔ Ｇａｍｅｓ理论给出原子布尔代数理论的一个判定过程及其复杂度,并说明这个过程在初等等价意义下是最优的。     

Zmin上秩-1矩阵的周长不等式及线性保持算子

利用Boolean秩-1矩阵的周长保持性质和Boolean代数B与Z_min上矩阵之间支配关系的等价性获得了Z_min上秩-1矩阵和的周长所满足的不等式, 保持其秩与周长的线性算子以及保持秩-1和周长2的性质.     

用概率方法研究Walsh谱的性质

给出了布尔函数的ｍ阶Ｗａｌｓｈ谱的概率表达式及布尔函数与一个ｍ阶布尔函数相互独立的判别条件；并用概率方法证明了布尔函数ｍ阶Ｗａｌｓｈ谱的性质