启发式协议验证

本文讨论和建立了一种状态空间探寻式(SEV)协议验证问题的图论模型,并形式地定义了协议错误、协议正确程度、验证算法复杂度等概念.本文提出了一个基于启发式搜索的协议验证算法 Z(?),并就其复杂度同耗尽式验证算法 Breadfirst 进行了比较.     

异步电路的计算机辅助设计软件

异步电路由于没有时钟频率的限制,所以较同步电路有很多优点,其研究也越来越广泛,是未来解决计算机CPU设计的一种重要方案。异步电路的计算机辅助设计软件代表了异步电路当前研究的前沿,通过研究这些软件可以对异步电路的模型有更为深入的认识。论文整理列举了有关异步电路的63种软件工具,并将其分为设计、仿真、相关设计工具、前端设计、综合和验证6个方面。最后,在这些软件中选取两种设计软件对一个简单的例子进行了设计实现,以体现异步电路的设计特点。     

工作流时序约束模型分析与验证方法

为了解决工作流时间建模与时序一致性验证问题,以时序逻辑和模型检查为基础,提出了一种工作流时间建模与时序一致性验证方法.该方法用一阶逻辑描述工作流模型及其时间信息,用时序逻辑描述工作流的时序约束,用模型检查算法对时序约束进行验证与分析.该方法不是针对某一种时序约束提出来的,而是能够验证任何用时序逻辑描述的工作流时序约束.该方法还能够对未通过验证的时序约束提供工作流运行实例作为反例,帮助用户定位模型的问题.以一个工作流时间建模和时序一致性验证的实例证实了所提出方法的有效性.     

单电子电路的鲁棒性研究

分析了单电子器件和人工神经网络的特性,从理论上证明了用人工神经网络构建单电子电路的可行性,并对单电子器件隧穿结隧穿特性和单电子振荡器的功能进行了仿真分析验证,同时研究了单电子振荡器的应用.本着可靠和复杂度低的前提,应用人工神经网络构建了一个单电子电路加法器模型,从模型的鲁棒性角度和电路的复杂性角度,用仿真软件对其进行了仿真分析.结果表明,神经网络是构建鲁棒性单电子电路的可靠方法,Pspice能够为成为单电子电路仿真的有效工具,为以后相关研究奠定了一定基础.     

异步集成电路设计方法综述

异步电路相对同步电路而言具有无时钟偏斜、模块化程度高、功耗低、电磁兼容性强等优势,越来越受到人们的广泛关注.异步电路设计方法是异步电路研究中的一个重点,文中将异步电路设计方法的发展历程划分为3个阶段,并着重对第3个阶段的设计方法进行了综述.根据设计方法的描述方式和设计粒度,首先将第3阶段进一步划分为语法驱动转换的设计方法、同步-异步转换的设计方法和基于定制的细粒度高性能异步流水线设计方法3类;然后从设计方法的理论基础、电路模型、设计自动化程度、电路性能等多个角度进行介绍并比较.最后对异步电路设计方法未来的发展趋势进行了展望.     

着色Petri网模型检测工具的扩展及其在Web服务组合中的应用

Web服务组合的形式化描述和验证是一个重要的研究问题.为了更好地完成验证工作,提出了扩展着色Petri网的模型检测方法.首先,在着色Petri网原有的基于CTL的局部模型检测算法基础上,给出了获取模型检测证据/反例的算法,并在着色Petri网模型检测工具--CPN Tools--中使用ML(meta language)语言实现了这些算法,然后将扩展后的CPN模型检测工具应用在Web服务组合的验证问题中.该方法不仅可以验证Web服务组合是否存在逻辑错误,还能告诉用户发生错误的原因,为Web服务组合的验证提供了技术上的保障.实验表明对着色Petri网的模型检测工具的扩展是正确、有效的.     

基于商空间理论的模糊粒度计算方法

商空间信息粒度模型可以从不同角度、不同层次观察问题.本文首先将商空间理论中论域合成技术进行推广,根据已知的粒度知识给出了粒度搜索范围,在问题求解中,降低了计算复杂度.然后讨论了模糊商空间粒度计算和分层递阶结构的关系,用不同粒度的商空间模型来表示聚类的结构.据此提出了基于Gaussian型函数的模糊聚类算法(G-FCluster算法),算法用距离表示信息粒度,不需要定义隶属函数和求出相似矩阵,并且不需要讨论参数的选择.将算法应用于中国证券市场,并与FCM算法进行比较.实验说明了算法可以很直观地从不同粒度(距离)观察聚类结果,大大降低了计算复杂度和空间复杂度,适于处理大数据量的样本.     

改进的基于属性不变量生成和数学归纳法的时序逻辑优化算法

为了在时序逻辑综合中使电路面积和关键路径延迟同时得到快速优化,提出一种改进的基于假设后验证的时序优化算法.在位并行随机模拟提取候选属性不变量之前,利用寄存器共享来降低初始候选不变量数目,以减少SAT程序的频繁调用;然后利用推测化简模型和改进的数学归纳法将基本条件和归纳步骤合并处理,有效地降低了电路规模和关键路径延迟,同时提高了算法运行速度.实验数据表明,文中算法使寄存器和节点规模平均下降41％和48％,关键路径延迟减小30％;与同类方法相比,该算法运行时间平均下降17％.     

面向移动设备的3D图形处理器设计

提出一种面向移动设备的3D图形处理器的设计方法,从图形算法和硬件架构两个层次进行优化.对图形算法进行C语言的仿真模拟,并设计高效的具有并行和流水线结构的图形处理器架构.该架构采用定点的数据通道,拥有一个可编程的顶点处理器和基于像素块的光栅扫描转换模块,降低电路复杂度的同时提高了整体性能.该设计已经在FPGA上验证,并给出了实验结果.实验结果显示该图形处理器结构可以满足移动设备的图形应用要求,具有可行性.     

一致性全局快照与稳定属性检测算法研究

文中首先介绍了分布式算法的相关概念和分布式算法的分类，然后根据同步模型和异步模型的特点，分别讨论了两种模型的研究方法，重点研究了异步网络模型中的一致性全局快照与稳定属性检测的问题，详细解释并改进了异步网络模型A算法的终止检测镜像算法，同时分析了算法的时间及通信复杂度。     

针对同步时序电路VHDL设计的有效模型判别器VERIS

介绍了一个针对同步时序电路VHDL设计的性质验证的解决方案-一个有效的符号模型判别器VERIS,该模型判别器利用同步时序电路设计的特点以及待验证性质的局部性,可显著地减少有限状态机（FSM）的状态空间;大大地提高可达性分析和性质验证的速度;同时,实现了反例生成机制,实验结果表明,与Deharbe的模型判别器相比,用这个模型判别器验证一些基准电路更加适用于同步时序电路。     

复杂嵌入式系统原型设计工具Statemate

嵌入式系统的设计面临着系统复杂性的挑战。StatemateMAGNUM是面向功能需求的系统级自动设计软件包,定位于复杂的反应型嵌入式实时混合系统的原型设计与正规化验证。通过对Statemate主要特性、方法论、核心技术及国内外应用情况的介绍与讨论,展示了该工具的良好应用前景。     

专用集成电路的设计验证方法及一种实际的通用微处理器设计的多级验证体系

随着专用集成电路制造工艺及设计方法的飞速发展,片上系统可集成的功能越来越多,规模越来越大,设计验证越来越复杂,只有使用先进的设计验证方法充分地验证其设计,才能保证一次投片成功.文中针对专用集成电路设计验证的各种方法和一种实际的通用微处理器设计的多级验证体系作了专门的描述,对片上系统设计者在构建自己的设计验证方案、使设计得以充分验证方面能给予一定的参考.     

利用SMT约束分解方法求解RTL可满足性问题

随着集成电路技术与工艺的不断发展,目前工业界所采用的形式验证工具已很难适应集成电路规模的飞速增长.为了对RTL电路的可满足性问题进行形式验证,提出基于超图划分的约束分解实现可满足性模理论(SMT)求解的分级验证方法.通过分析RTL电路的结构约束,对约束集合中的元素和相关变量进行约束建模,并构建带有合适权重的超图模型;利用超图划分的机制寻找带有最小割集的等量划分,实现约束分解,完成RTL电路的定界模型检验.实验结果表明,该方法能够减小处理问题的规模和求解过程中的搜索空间,提高验证效率.     

并发和实时系统的模型检验技术

模型检验是一种重要的自动验证技术,通过显式状态搜索或隐式不动点计算来验证并发或实时系统的模态／命题性质,以保证通信协议、数字电路等设计的正确性。详细阐述了模型检验技术的发展与研究现状。首先描述了并发系统分别基于自动机理论和符号化的两种主要模型检验策略,并给出解决状态爆炸问题的主要方法;然后介绍了针对实时系统以及面向对象设计的模型检验方法;对每种方法都介绍了相应的典型工具,最后分析了模型检验面临的困难以及今后的发展趋势。