共查询到19条相似文献,搜索用时 62 毫秒
1.
2.
提出一种改进的基于时间帧展开的时序电路等价验证算法,其来源于模型检查中的基于数学归纳的验证算法,在使用并简化了SAT问题中不可满足子集提取过程后,将基本条件检查和归纳检查合并处理.为了能在时间帧展开过程中减少状态搜索空间,利用结构不动点技术并提出了准动态唯一状态约束等改进的方法.实验表明,随着时间帧的不断展开,文中算法运行时间的增长速度明显慢于基于数学归纳法的验证算法,其适合验证经过时序优化后的电路. 相似文献
3.
为了提高等价性验证在数字电路中的验证效率,提出一种逻辑锥分割和可满足性相结合的方法。通过划分规则把参照电路和实现电路划分成若干个逻辑锥,利用匹配技术对两者的逻辑锥进行匹配,将已匹配的两个逻辑锥的输出用一个异或门连接,从而得到Miter电路,将该结构转换成相应的合取范式,用可满足性引擎来验证Miter电路是否功能等价。在ISCAS’85基准电路的实验结果表明该方法的可行性。 相似文献
4.
介绍了一种使用电路可满足性解算器的组合电路等价性验证算法.对包含多输出的复杂验证问题,首先对联接电路作输出分组,将等价性验证问题转化为包含若干个组的电路可满足性问题,继而使用电路解算器解决问题.同时,注意各个子问题间的有用隐含信息的共享,减小了SAT推理的搜索空间.实验结果表明,该算法是实用有效的. 相似文献
5.
随着集成电路设计规模的日益增大,结合多种推理引擎已成为组合电路形式化等价性验证的重要手段.提出一种基于电路拓扑结构分析的组合等价性验证方法,将电路的拓扑结构与验证算法的复杂性关联起来.在验证过程开始之前,利用min-cut方法计算表征电路复杂性的"电路宽度",以确定最佳的推理引擎,避免了传统的引擎切换过程,提高了算法的效率.针对ISCAS85电路的实验结果表明了该方法的效率和可行性. 相似文献
6.
组合验证是数字集成电路形式化设计验证的重要方面.该文提出了一种基于增量布尔可满足性的组合等价性检验方法,通过合理选择候选等价结点和增量可满足性算法来提高算法性能,并通过对内部等价结点的置换及将等价关系转化为相应的合取范式公式,避免了误判的发生,又能缩小验证程序的搜索空间.针对ISCAS’85电路的实验结果表明,该文提出的方法比以往同类方法更快、更强健. 相似文献
7.
基于BDD或布尔SAT的等价验证方法虽然能够成功验证低层次门级电路,但却难以满足高层次设计验证要求. 由此,以多项式符号代数为理论基础,提出了一个高层次数据通路的等价验证算法. 深入研究了使用多项式表达式描述复杂数据通路行为的方法,得到了高层次数据通路的多项式集合表示的一般形式. 从多项式集合公共零点的角度定义了高层次数据通路的功能等价,给出了一个基于Grbner基计算的有效代数求解算法. 针对不同基准数据通路的实验结果表明了该算法的有效性. 相似文献
8.
RTL混合可满足性求解方法分为基于可满足性模理论(SMT)和基于电路结构搜索两大类.前者主要使用逻辑推理的方法,目前已在处理器验证中得到了广泛的应用,主要得益于SMT支持用于描述验证条件的基础理论;后者能够充分地利用电路中的约束信息,因而求解效率较高.介绍了每一大类中的典型研究及其所采用的重要策略,以及RTL可满足性求解方面的研究进展. 相似文献
9.
10.
通用CPU设计验证中的等价性检验方法 总被引:3,自引:2,他引:1
针对传统的模拟验证方法需要大量的时间且难以获得完全的覆盖率的局限性,提出了目前应用最广泛的一种形式验证方法——等价性检验在一款通用CPU设计验证中的应用方案,包括寄存器传输级(RTL)设计与门级网表、门级网表与门级网表、RTL设计与RTL设计之间的功能等价性验证.此外,给出了验证过程中一些常见问题的解决办法.验证结果表明了该方法的可行性,显著地减少了门级模拟的时间. 相似文献
11.
12.
13.
处理器研制过程中需要对指令算术数据路径进行覆盖验证.针对现有模拟验证方法存在的不足,提出了一种基于可满足模理论(satisfiability modulo theory, SMT)的指令约束求解方法:利用可满足模理论求解器将指令级功能验证任务转化成数据约束求解满足问题.在结果操作数约束、操作数间约束、指令内部约束以及浮点操作数约束4个方面分别给出示例,并分别给出了利用SMT求解器进行约束建模的关键过程以及可以用于指令级功能验证的元组数据.为提高求解模型效率,提出了2种解决方法:首先利用时间阈值实现问题求解超时即终止的策略;其次是结合进程管理与线程管理技术,实现了指令功能约束并行求解框架,将串行求解任务分派给可并行执行的多个线程,提高了求解速度.该技术已成功应用于系统级验证中,有效提升了测试覆盖与质量,取得了很好的效益. 相似文献
14.
15.
聚类是数据挖掘研究中最常见的一种方法,可以作为规则发现、异常发现等其它数据挖掘操作的基础,一直以来都是数据挖掘的研究热点之一。股票数据是一种典型的时间序列数据,利用股票数据进行时间序列数据挖掘的研究既有一定的实际应用价值,也是国内外的热点问题之一。文章首次将一种新型符号化方法SAX[1]应用到标准普尔500指数的股票数据的聚类研究中,使用传统的欧氏距离和动态时间弯曲两种时间序列相似性度量方法进行实验。实验结果表明将SAX应用到股票数据聚类操作,可以得到更好的趋势聚类效果和更高的效率。 相似文献
16.
传统异常检测模型往往基于内容特征,随着攻击手段的提高,该方法易于被绕过,因此图挖掘技术逐渐成为了国内外学术研究的热点。为了提高异常检测的准确率,提出了一种基于长短时记忆网络的动态图模型异常检测算法。首先通过对动态图的变化特征进行分析,总结了Egonet图结构距离和编辑距离两类特征,高效地表示动态图结构的变化情况。其次,通过基于LSTM的时间序列分类算法,进行模型的训练。最后对抓取的网络数据流进行入侵检测,对超过6万节点和300万条边的拓扑图进行测试。最终实验结果表明,该算法具有更高的准确率和召回率,可以有效地检测出网络入侵事件。 相似文献
17.
基于状态空间等价类的有色Petri网特性验证 总被引:1,自引:0,他引:1
李沛武 《计算机工程与应用》2003,39(11):16-18
在有色Petri网的状态空间中,有时一些状态具有相似的行为,这些状态可以用定义在状态空间上的一致的等价关系来表达,对每个等价状态类只研究它的一个代表状态的行为,这极大地减小了有色Petri网的状态空间。但是,通常对一个给定的等价关系是否为一致的验证都是通过用户的经验人工进行的,这不但容易产生错误,而且效率低下。该文依据普通状态图和等价类状态图的标记迁移系统关系,对状态空间一致性等价定义的计算机辅助验证做了深入的讨论,给出了相应的结果。 相似文献
18.
基于UML的软件形式化需求分析与验证 总被引:1,自引:0,他引:1
针对软件开发中传统的需求分析方法所存在的需求描述不完整、具有二义性和不一致性问题,提出一种形式化需求分析方法。介绍根据用户需求采用形式化方法获取软件需求说明书并设计软件的统一建模语言(UML)模型的过程,及对该UML模型进行形式化描述,采用形式化验证技术对形式化后的UML模型进行需求验证,以确保设计的UML模型的正确性。实验结果表明,形式化的需求分析方法克服了传统需求分析方法中存在的问题。 相似文献