【摘 要】
：
由于电路规模不断增大和电路的功能的日益复杂，这就使得大规模的电路设计很难保证逻辑设计的正确无误。然而为了设计和建立高可靠的VLSI系统，必须对VLSI的设计和实现进行有效的
【出 处】
：
中国科学院研究生院 中国科学院大学
论文部分内容阅读
由于电路规模不断增大和电路的功能的日益复杂，这就使得大规模的电路设计很难保证逻辑设计的正确无误。然而为了设计和建立高可靠的VLSI系统，必须对VLSI的设计和实现进行有效的验证。目前主要的验证方法有模拟验证和形式验证两种，模拟验证是当前工业界使用的主要方法，但是由于单纯的模拟验证已不能满足VLSI设计和制造的需要，形式验证方法越来越引起人们的重视。
模型检验(Model Checking)方法是一种很有前途的形式验证方法，它的验证方法是通过对有限状态空间的遍历来实现规范说明(Specification)是否得到满足。这种方法具有高度自动化，执行速度快，能产生反例帮助调试等特点，适合于VLSI的验证。
大型复杂系统的开发过程中不可避免的涉及到非确定或不一致信息的处理，而多值模型检验作为经典模型检验的一种扩展，是处理和分析包含此类信息模型的一种有效手段。提出了一种系统化的多值逻辑(涵盖经典逻辑)的代数表示方法，使用吴方法的基本思想和框架实现复杂系统形式验证中基于多值逻辑的模型检验的代数化，建立了通过吴方法实现多值模型检验技术的整体框架。这种代数化的多值模型检验方法可以作为现有方法的有力补充。
针对DSP电路的高层次设计验证的定界模型检验，提出一种基于有限环上多项式理想的Grobner基的定界模型检验方法。通过使用有限环上多项式等式建模高层次设计和待验证性质，将定界模型检验问题转化为定理证明问题，并采用有限环上多项式理想的Grobner基有效地解决该定理证明问题。与基于布尔可满足性(SAT)和基于线性规划的RTLSAT的定界模型检验方法相比，该方法对一些DSP电路的验证平均要快1倍到1个数量级。
其他文献
人脸识别在计算机视觉和生物识别系统中具有非常重要的作用。尽管现有的人脸识别系统已经比较成熟，但还存在着一些会对系统的可靠性构成威胁的因素。例如，姿态、光照、面部表情
本论文主要基于Karamata正规变化理论,采用上下解的办法研究了三个非线性椭圆型方程奇异边值问题的解的渐近行为. 首先,本文针对边界blow-up的半线性椭圆型问题的解的二次
本文主要利用自洽平均场理论研究了大分子微球复合水凝胶材料的微观相结构.随着高分子材料科学的发展,水凝胶由于具有良好的机械性能、较强的抗压和吸水性,越来越受到科学研
设φαn是指标为α的Hermite型Lagurre展式，它们是Lagurre算子Lα=1/2(-d2/dy2+y2+1/y2(α2-1/4))的特征向量.本学位论文主要研究了与Lagurre算子Lα相关的BMO-型空间.具体包
随着最优化理论的发展与实际应用的需要,矩阵优化问题近年来在世界范围内受到了广泛的关注.而在这类问题中,最让我们觉得感兴趣的,是两类有特殊结构的矩阵,即低秩矩阵与稀疏
保险公司的收益主要来源于承保利润和投资收益,其中承保利润受国家政策变动、市场条件波动等外部因素的影响比较大.而保险公司的投资能力大小往往取决于投资收益,所以保险公司要选择一个合理的投资组合及投资比例,使得保险公司的投资收益达到最大.目前构建资产组合的方法很多,得到的最优投资比例也各不相同,其中随机占优组合优化也已经普遍应用到经济和金融领域.本文研究的是在投资组合优化中如何建立二阶随机占约束的保险资
脉冲切换系统是一类重要的混杂系统,最近几年,由于其在自动化控制,计算机控制,过程控制等领域的广泛应用而受到了人们的关注.迄今为止,关于脉冲系统和切换系统有限时间稳定性
纹理是图像分析和识别中经常使用的关键特征,而小波变换则是图像纹理表示和分类中的常用工具.然而,基于小波变换的纹理分类方法常常忽略了小波低频子带信息,并且无法提取图像纹理的块状奇异信息.本文提出小波子带系数的局部能量直方图建模方法、轮廓波特征的Poisson混合模型建模方法和基于轮廓波子带系数聚类的特征提取方法,并将其应用于图像纹理分类上.基于局部能量直方图的纹理分类方法解决了小波低频子带的建模难题
本文一共包含了三个部分，主要介绍了S-仿Lindelof空间的一些性质。 第一章主要介绍了本文的选题依据及其内外研究背景； 第二章主要介绍了本论文所要使用到的拓扑空间的相
多项式优化问题是优化领域内最根本的问题之一。在生产实践中,有大量源于生物工程、控制、信号处理等领域的问题都可以归结为多项式优化问题.本文着重研究多项式优化领域内的