形式验证相关论文
热导式气压传感器广泛应用于航天、化工、半导体加工、食品加工、电子封装以及科学研究等诸多领域。随着微机电系统(MEMS)和集成电......
在混合系统中,离散事件和连续动态行为相互作用的特性使得系统开发的正确性难以保证,尤其对于安全悠关的系统,如电力系统和化工系......
混合系统主要研究由连续性子系统和离散性子系统相互作用而构成的一类动态系统。连续性子系统和离散性子系统二者相互作用,使系统......
随着过程控制对象越来越复杂,混杂特性已经普遍存在于流程工业中。针对这种情况,论文研究了基于混合逻辑动态(MLD:Mixed Logical D......
形式化方法目前在工业界还没有得到广泛应用，主要是因为各种形式化方法没有很好地整合到工业界的软件开发过程中去，并且目前还没有比......
随着数字IC设计规模的增大和功能复杂性的提高,设计验证成为IC设计流程中越来越重要的方面。传统的模拟验证方法无法满足复杂IC设......
信息时代的发展,引领计算机软件应用深入到千家万户,各行各业。随着软件的应用领域迅速加大,规模急速扩张,软件安全性的要求也逐步......
分段仿射(PWA)模型不仅在描述系统非线性特性和混杂特性方面独具优势,而且能够方便的用于对系统性能的分析和控制方法的研究中,因......
随着集成电路进入超摩尔时代,集成电路规模日益增大,功能日渐复杂,验证工作在芯片研发周期中占到约70%的时间,传统的直接验证已无......
近两年,微电子技术得到了迅速地发展,芯片设计水平不断提高,传统的验证方法已经无法满足目前的验证需求,功能验证逐渐面临着巨大的......
PLC(可编程逻辑控制器)是一种嵌入式设备,广泛应用于工业控制领域。这些领域对程序的正确性要求很高,但传统的模拟、测试等方法无......
随着集成电路设计的复杂度和难度日益增大,验证作为设计过程中的关键环节,面临着巨大挑战。据统计,在芯片设计中,超过50%的人力和......
数字信号处理器(Digital signal processor,DSP)广泛应用于雷达、声纳、数字通信以及语音视频信号处理等领域。为保证DSP能够正常......
混合系统理论是控制工程理论与计算机科学验证交叉的学科领域。混合系统理论主要涉及到有限自动机表示的离散状态与微分方程表示的......
混杂系统是连续变量动态系统和离散事件动态系统相结合，并且二者相互影响相互作用的一类系统。混杂系统形式验证是混杂系统的一个研......
自主车辆是集环境感知、规划决策、多等级辅助驾驶等功能于一体的综合智能系统。它集中运用了计算机、现代传感、信息融合、通信、......
研究成品率分析芯片的特点和设计流程,提出适用的LVS万法.该方法结合传统的LVS及形式验证,能够解决成品率分析芯片中违反设计规则......
符号模型检查（ＳｙｍｂｏｌｉｃＭｏｄｅｌＣｈｅｃｋｉｎｇ，ＳＭＣ）是一种有效的形式验证方法．该方法主要有２个难点：一个是建模，即如何建立并用有限内存来表示电路的状态机模型；另一个是在此......
为了探索更好的验证方式,本文总结了仿真验证方法在应对HDLC协议验证时面临的挑战,提出了以形式验证对HDLC协议设计进行协议级验证......
前言rn断言和功能覆盖率犹如一个硬币的两面.在一个RTL的设计中,两者都提供了详尽的可观察点.断言提供了功能正确与否的信息,而功......
该文从挂篮荷载计算、施工流程、支座及临时固结施工、挂篮安装及试验、合拢段施工、模板制作安装、钢筋安装、混凝土的浇筑及养生......
提出了一个可满足性问题解决器,它结合了DPLL(Davis Putnam Loge-mann and Loveland)算法和作为高级推理技术之一的失败性文字检查......
Object-Z是形式规格说明语言Z的面向对象扩充,适合描述大型面向对象软件规格说明,但它不能很好地描述连续性实时变量和时间限制。......
本文主要阐述了基于断言技术并结合动态仿真,形式测试,测试激励自动化等方法的新硬件验证平台,着重介绍了O-VA的特点及运用,并以LC......
提出了一种基于带参系统的Murphi模型来完成对应的SMV自动化建模的方法.因为Murphi工具拥有带参特性,因此使用其对带参系统进行建......
文章分析了目前常用的等价性检验方法的特点,包括功能性和结构性的验证方法;讨论了基于二叉判决图(BDD)的组合电路等价性检验方法,......
软件模型检测以其潜在的商业价值一直为学术界和工业界关注．本文通过剖析模型检测工具SLAM，探讨软件模型检测的机理、方法及若干核心......
数字系统的验证是一个复杂的过程。结合当前数字电路设计的高复杂度、高度集成化的特性，介绍了模拟验证和形式验证两种验证方法，并对......
基于SAT的运算电路查错方法将被验证系统中系统规范成立与否的问题转换为布尔公式和数学公式的混合形式E-CNF,通过采用了标志子句......
在介绍混合系统形式验证概念的基础上,从可达集表示和可达集计算方法的角度比较了混合系统的各种形式验证方法和验证工具。重点介......
In the compilation of rule program to the intermediate code--RETE network,optimizing compilation is an important comptle......
为了提高组合电路的等价性验证速度，提出了一种利用电路内部等价信息的新型验证方法．该方法结合了通用割集和专用割集．从原始输出进行......
成功设计一个复杂数字系统要求在设计的各个阶段验证实现的正确性，传统的模拟验证已不能完全满足需要，形式验证技术成为了重要的补充......
组合验证是数字集成电路形式化设计验证的重要方面.该文提出了一种基于增量布尔可满足性的组合等价性检验方法,通过合理选择候选等......
提出一新的验证算法,利用电路拓扑信息选择有效割集,以减小验证规模,并对割集进行无依赖性处理,减少伪错误发生概率,提高验证效率;......
采用线性规划作为基本工具开发一个RTL可满足性求解器，并将其应用于解决RTL性质检验问题．深入研究了使用线性规划约束对RTL电路元器......
提出一种无界模型检验的前像计算方法,该方法有效地结合ATPG和SAT引擎,充分利用引擎各自的优点.SAT用来判断是否已经穷尽所有解;每......
以vanishing多项式理想的极小强Grbner基为理论基础,提出一种针对定点算术数据通路的等价性检验方法.通过使用多项式函数建模定点......
为了表示事件出现的时间约束,扩展属性序列图为时间属性序列图,使其继承属性序列图的优点,并且能够表示时间属性,定义了时间属性序......
如今超大规模集成电路（IC）的发展趋势加快了片上系统（System-on-Chip,SoC）技术的开发,而功耗管理与节能技术已经遍及片上系统设计的各......
微处理器验证是微处理器设计的关键环节。该文探讨了微处理器模拟、硬件仿真、形式验证等方法的原理、特点和适用场合，提出了进行多......
目前提高求解SAT问题完全算法的计算效率问题已成为挑战性研究问题。提出了一种基于启发式分组的SAT完备算法。启发式分组策略将一......
在处理器从单核向多核演进的过程中,为了获得更好的性能和可扩展性,适用于多核处理器系统的Cache一致性协议变得越来越复杂。Cache......
非信任代码的安全执行是移动代码安全的重要问题之一。携带模型代码方法同时从移动代码的生产者和使用者的角度考虑,为安全执行非......
针对实时系统软件开发的特殊性要求,本文强调形式方法是保证实时系统软件开发正确的一种重要方法。文章首先对形式方法的含义进行......
研究了极小布尔不可满足子式的提取算法 ,它分为近似算法和精确算法两种 文中就精确算法提出了局部预先赋值的优化方案 ,并且在理......
