带黑盒组合电路的等价性验证

为了在早期阶段发现电路设计错误,需要对包含未知部分的实现电路和规范电路进行等价性验证.本文提出了一种"分而治之"的方法,把电路划分成若干子电路,使用四值逻辑模拟技术对电路未知部分进行量化,然后对子电路的合取范式进行可满足性验证.这种方法增强了算法的错误检测能力,通过在ISCAS'85基准电路和10个简单组合电路上得到的两组实验数据表明了此算法的有效性和可行性.     

改进的时间帧展开的时序电路等价验证算法

提出一种改进的基于时间帧展开的时序电路等价验证算法,其来源于模型检查中的基于数学归纳的验证算法,在使用并简化了SAT问题中不可满足子集提取过程后,将基本条件检查和归纳检查合并处理．为了能在时间帧展开过程中减少状态搜索空间,利用结构不动点技术并提出了准动态唯一状态约束等改进的方法．实验表明,随着时间帧的不断展开,文中算法运行时间的增长速度明显慢于基于数学归纳法的验证算法,其适合验证经过时序优化后的电路．     

使用逻辑锥分割的组合电路等价性验证

为了提高等价性验证在数字电路中的验证效率,提出一种逻辑锥分割和可满足性相结合的方法。通过划分规则把参照电路和实现电路划分成若干个逻辑锥,利用匹配技术对两者的逻辑锥进行匹配,将已匹配的两个逻辑锥的输出用一个异或门连接,从而得到Miter电路,将该结构转换成相应的合取范式,用可满足性引擎来验证Miter电路是否功能等价。在ISCAS’85基准电路的实验结果表明该方法的可行性。     

使用输出分组和电路可满足性的等价性验证算法

介绍了一种使用电路可满足性解算器的组合电路等价性验证算法．对包含多输出的复杂验证问题,首先对联接电路作输出分组,将等价性验证问题转化为包含若干个组的电路可满足性问题,继而使用电路解算器解决问题．同时,注意各个子问题间的有用隐含信息的共享,减小了SAT推理的搜索空间．实验结果表明,该算法是实用有效的．     

基于电路拓扑结构分析的等价性验证方法

随着集成电路设计规模的日益增大,结合多种推理引擎已成为组合电路形式化等价性验证的重要手段.提出一种基于电路拓扑结构分析的组合等价性验证方法,将电路的拓扑结构与验证算法的复杂性关联起来.在验证过程开始之前,利用min-cut方法计算表征电路复杂性的"电路宽度",以确定最佳的推理引擎,避免了传统的引擎切换过程,提高了算法的效率.针对ISCAS85电路的实验结果表明了该方法的效率和可行性.     

基于增量可满足性的等价性检验方法

组合验证是数字集成电路形式化设计验证的重要方面．该文提出了一种基于增量布尔可满足性的组合等价性检验方法,通过合理选择候选等价结点和增量可满足性算法来提高算法性能,并通过对内部等价结点的置换及将等价关系转化为相应的合取范式公式,避免了误判的发生,又能缩小验证程序的搜索空间．针对ISCAS’85电路的实验结果表明,该文提出的方法比以往同类方法更快、更强健．     

基于多项式符号代数方法的高层次数据通路的等价验证

基于BDD或布尔SAT的等价验证方法虽然能够成功验证低层次门级电路,但却难以满足高层次设计验证要求. 由此,以多项式符号代数为理论基础,提出了一个高层次数据通路的等价验证算法. 深入研究了使用多项式表达式描述复杂数据通路行为的方法,得到了高层次数据通路的多项式集合表示的一般形式. 从多项式集合公共零点的角度定义了高层次数据通路的功能等价,给出了一个基于Grbner基计算的有效代数求解算法. 针对不同基准数据通路的实验结果表明了该算法的有效性.     

RTL验证中的混合可满足性求解

RTL混合可满足性求解方法分为基于可满足性模理论(SMT)和基于电路结构搜索两大类.前者主要使用逻辑推理的方法,目前已在处理器验证中得到了广泛的应用,主要得益于SMT支持用于描述验证条件的基础理论;后者能够充分地利用电路中的约束信息,因而求解效率较高.介绍了每一大类中的典型研究及其所采用的重要策略,以及RTL可满足性求解方面的研究进展.     

组合电路等价性检验方法研究

分析了数字电路等价性检验方法的基本原理，对组合电路等价性检验方法进行了综合研究，讨论了各种方法的特点，指出了各种方法的优缺点及其适用场合，总结了组合电路等价性检验方法的发展规律，指出了未来的发展方向。     

通用CPU设计验证中的等价性检验方法

针对传统的模拟验证方法需要大量的时间且难以获得完全的覆盖率的局限性,提出了目前应用最广泛的一种形式验证方法——等价性检验在一款通用CPU设计验证中的应用方案,包括寄存器传输级(RTL)设计与门级网表、门级网表与门级网表、RTL设计与RTL设计之间的功能等价性验证．此外,给出了验证过程中一些常见问题的解决办法．验证结果表明了该方法的可行性,显著地减少了门级模拟的时间．     

基于报警时序信息挖掘的报警关联分析方法

面对现代流程工业监控系统报警泛滥问题,为了寻找报警根源以减少无效报警,并针对传统方法在面对大量的报警数据时计算效率低下的问题,提出了一种基于报警数据时序信息挖掘的报警关联分析方法.通过将报警时序信息进行区块化处理,将报警时间序列转换为报警时间的节点序列,然后将区块之间的匹配度作为报警关联度的评价标准,减少了关联分析的运算量;采用滑动窗口比对计算相关报警时间序列的时间关联信息;采用TE过程（Tennessee Eastman process）数据,验证了所提方法的有效性.     

可信应用环境的安全性验证方法

针对可信应用环境的安全性验证问题,利用通信顺序进程描述系统应具有的无干扰属性,基于强制访问控制机制对系统中的软件包进行标记,并对系统应用流程建模。将该模型输入FDR2中进行实验,结果证明,系统应用在运行过程中达到安全可信状态,可以屏蔽环境中其他应用非预期的干扰。     

基于SMT求解器的微处理器指令验证数据约束生成技术

处理器研制过程中需要对指令算术数据路径进行覆盖验证.针对现有模拟验证方法存在的不足,提出了一种基于可满足模理论(satisfiability modulo theory, SMT)的指令约束求解方法：利用可满足模理论求解器将指令级功能验证任务转化成数据约束求解满足问题.在结果操作数约束、操作数间约束、指令内部约束以及浮点操作数约束4个方面分别给出示例,并分别给出了利用SMT求解器进行约束建模的关键过程以及可以用于指令级功能验证的元组数据.为提高求解模型效率,提出了2种解决方法：首先利用时间阈值实现问题求解超时即终止的策略;其次是结合进程管理与线程管理技术,实现了指令功能约束并行求解框架,将串行求解任务分派给可并行执行的多个线程,提高了求解速度.该技术已成功应用于系统级验证中,有效提升了测试覆盖与质量,取得了很好的效益.     

基于J2EE组件技术的水文时间序列相似性挖掘系统

时间序列的相似性挖掘是数据挖掘中的重要内容,通过对水文时间序列的相似性挖掘研究,设计并实现一个基于J2EE组件技术的相似性挖掘系统。并对该系统进行了测试实验,证明其有效性和正确性．     

符号化近似SAX在时序数据挖掘中的应用研究

聚类是数据挖掘研究中最常见的一种方法,可以作为规则发现、异常发现等其它数据挖掘操作的基础,一直以来都是数据挖掘的研究热点之一。股票数据是一种典型的时间序列数据,利用股票数据进行时间序列数据挖掘的研究既有一定的实际应用价值,也是国内外的热点问题之一。文章首次将一种新型符号化方法SAX[1]应用到标准普尔500指数的股票数据的聚类研究中,使用传统的欧氏距离和动态时间弯曲两种时间序列相似性度量方法进行实验。实验结果表明将SAX应用到股票数据聚类操作,可以得到更好的趋势聚类效果和更高的效率。     

基于LSTM的动态图模型异常检测算法研究

传统异常检测模型往往基于内容特征，随着攻击手段的提高，该方法易于被绕过，因此图挖掘技术逐渐成为了国内外学术研究的热点。为了提高异常检测的准确率，提出了一种基于长短时记忆网络的动态图模型异常检测算法。首先通过对动态图的变化特征进行分析，总结了Egonet图结构距离和编辑距离两类特征，高效地表示动态图结构的变化情况。其次，通过基于LSTM的时间序列分类算法，进行模型的训练。最后对抓取的网络数据流进行入侵检测，对超过6万节点和300万条边的拓扑图进行测试。最终实验结果表明，该算法具有更高的准确率和召回率，可以有效地检测出网络入侵事件。     

基于约束求解的微处理器功能验证程序生成

针对伪随机方法生成微处理器功能验证程序缺乏完备性、灵活性的问题,构建一种用于生成验证程序的C++约束函数库。以微处理器指令系统为对象,以约束满足问题的数学模型为理论依据,结合用户验证需求,利用约束函数库生成功能验证程序。验证结果表明,该方法开发验证程序简单、高效,加快了验证收敛速度。     

基于状态空间等价类的有色Petri网特性验证

在有色Petri网的状态空间中,有时一些状态具有相似的行为,这些状态可以用定义在状态空间上的一致的等价关系来表达,对每个等价状态类只研究它的一个代表状态的行为,这极大地减小了有色Petri网的状态空间。但是,通常对一个给定的等价关系是否为一致的验证都是通过用户的经验人工进行的,这不但容易产生错误,而且效率低下。该文依据普通状态图和等价类状态图的标记迁移系统关系,对状态空间一致性等价定义的计算机辅助验证做了深入的讨论,给出了相应的结果。     

基于UML的软件形式化需求分析与验证

针对软件开发中传统的需求分析方法所存在的需求描述不完整、具有二义性和不一致性问题,提出一种形式化需求分析方法。介绍根据用户需求采用形式化方法获取软件需求说明书并设计软件的统一建模语言（UML）模型的过程,及对该UML模型进行形式化描述,采用形式化验证技术对形式化后的UML模型进行需求验证,以确保设计的UML模型的正确性。实验结果表明,形式化的需求分析方法克服了传统需求分析方法中存在的问题。