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

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

可满足性求解技术研究

求解公式的可满足性在诸如形式化验证、电子设计自动化与人工智能等众多领域中都具有非常重要的理论与应用价值,成为近年来的研究热点。本文针对命题公式与一阶公式的可满足性问题,重点介绍了布尔可满足性与可满足性模理论求解技术的基本原理,并且根据算法的类型进行分类阐述,分析了各种算法的优缺点。最后,讨论了目前面临的主要挑战,对今后的研究方向进行了展望。     

CP-nets的可满足性及一致性研究

CP-nets是一种简单而又直观的图形化偏好表示工具,成为近几年人工智能的一个研究热点,然而对于CP-nets的可满足性和一致性等相关性质的研究还很欠缺.既没有给出严格的定义,也没有探讨不同性质之间的联系,没有一个求可满足性序列的通用算法.从研究CP-nets的可满足性和一致性的关系着手,得出了任意结构二值CP-nets的可满足性判定算法及可满足性序列生成算法.首先通过构造CP-nets导出图及其性质的研究,得出CP-nets的可满足性及一致性的相关定理.再把不同性质结合起来分析,给出CP-nets可满足性等价于一致性的结论,从而利用拓扑排序的思想实现了任意结构二值CP-nets的可满足性序列的生成.强化和扩充了Boutilier所提出的一些概念,深化了CP-nets的基础理论研究.     

可满足实例的归结复杂度

GRB模型是一种随机约束满足问题模型,此模型具有精确的可满足相变现象。针对实验中出现的GRB模型在相变区域产生的可满足实例都是难解的现象,利用子句宽度和归结复杂度的关系证明了GRB模型在相变点附近产生的可满足实例对于树型归结证明具有指数下界。因此从理论上证明了在相变区域产生的可满足实例对基于归结的算法是难解的。     

可满足问题中的模型计数

模型计数问题是指计算给定问题的解的个数,这是一类比决策更困难的问题,也是人工智能领域研究的一个热点问题.对模型计数问题的研究不仅可以提高算法的求解效率,更能促进对问题困难本质的了解.以可满足问题（命题可满足（SAT）和约束可满足问题（CSP））为例,从精确算法和近似求解两方面综述了模型计数问题的研究现状,重点介绍了相关概念以及各个算法之间的优缺点,并提出了有待解决的开放性问题,对模型计数问题的研究予以了总结和展望.     

一种目标可满足性定性、定量表示与推理方法

可满足性表示和推理方法是面向目标需求工程领域的重要研究内容.根据从连续定量论域抽取定性概念过程中的主观认知的不确定性特点,提出了一种基于云模型的目标可满足性表示模型.作为定性概念与其定量论域间的不确定性转换模型,云模型能够把主观认知的模糊性和随机性集成在一起,兼顾可满足性定性表示的语义明确性和定量表示的精确性,较好地实现可满足性定性、定量统一表示.在此基础上,设计了一种基于OWA(ordered weighted aggregation)算子核心思想的目标可满足性推理方法,该方法避免了纯逻辑推理过于"偏执"的推理结果.同时,父目标满足程度介于子目标可满足性的最小和最大值之间,较好地反映出了人类一般思维的特点.采用定理证明和对比实验的方式,对推理方法的特点进行分析.最后进行总结,并指出进一步的研究方向.     

基于一阶逻辑的可满足求解方法研究进展

基于命题逻辑的布尔可满足SAT存在描述能力弱、抽象层次低、求解复杂度高等问题,而基于一阶逻辑的可满足性模理论SMT采用高层建模语言,表达能力更强,更接近于字级设计,避免将问题转化到位级求解,在硬件RTL级验证、程序验证与实时系统验证等领域得到了广泛应用。针对近年来涌现的众多SMT求解方法,依据方法的求解方式进行了分类与对比。而后,对3种主流的求解方法Eager方法、Lazy方法和DPLL(T)方法的实现进行了概要介绍。最后,讨论了SMT求解方法当前所面临的主要挑战以及在SMT求解方面的一些研究成果,并对今后的研究进行了展望。     

求解极小SMT不可满足子式的宽度优先搜索算法

极小不可满足子式能够为可满足性模理论(SMT)公式的不可满足的原因提供精确的解释,帮助自动化工具迅速定位错误.针对极小SMT不可满足子式的求解问题,提出了SMT公式搜索树及其3类结点的概念,并给出了不可满足子式、极小不可满足子式与3类结点之间的映射关系.基于这种映射关系,采用宽度优先的搜索策略提出了宽度优先搜索的极小SMT不可满足子式求解算法.基于业界公认的SMT Competition 2007测试集进行实验的结果表明,该算法能够有效地求解极小不可满足子式.     

PSL可满足问题的计算复杂度

PSL是一种用于描述并行系统的属性规约语言,包括线性时序逻辑FL和分支时序逻辑OBE两部分。由于OBE就是CTL,因此论文重点研究FL逻辑。理论上已证明许多难解的问题都可多项式变换为“可满足性”问题,“可满足性”问题是研究时序逻辑的核心问题之一,并已成为程序验证的一种有力工具;而计算复杂度是“可满足性”问题需要解决的最深刻的方向之一,其研究意义在于它可作为解决一类问题的难度的标准。文中在利用“铺砖模型”基础上,推导并得出FL的“可满足性”问题的计算复杂度为EXPSPACE—hard,这对正确评价解决该问题的各种算法的效率,进而确定对已有算法的改进余地具有重要的指导意义。     

PSL可满足问题的计算复杂度

PSL是一种用于描述并行系统的属性规约语言,包括线性时序逻辑FL和分支时序逻辑OBE两部分。由于OBE就是CTL,因此论文重点研究FL逻辑。理论上已证明许多难解的问题都可多项式变换为“可满足性”问题,“可满足性”问题是研究时序逻辑的核心问题之一,并已成为程序验证的一种有力工具;而计算复杂度是“可满足性”问题需要解决的最深刻的方向之一,其研究意义在于它可作为解决一类问题的难度的标准。文中在利用“铺砖模型”基础上,推导并得出FL的“可满足性”问题的计算复杂度为EXPSPACE—hard,这对正确评价解决该问题的各种算法的效率,进而确定对已有算法的改进余地具有重要的指导意义。     

Period And Priority Assignment Method For Dcs Design

Distributed control systems (DCS) used in industry environments consist of sensors, actuators, and controllers that are connected with a fieldbus. It is difficult to design the DCS while guaranteeing the time‐critical requirements because of both communication delays due to the fieldbus and computation delays due to many tasks executed in one node. This paper proposes a priority assignment method and a period assignment method that find the shortest periods of control loops and guarantee the end‐to‐end constraints such as precedence constraints and timing constraints. Also, a DCS design method is presented by using the proposed two assignment methods. The presented design method considers the worst‐case response times of tasks and messages simultaneously and is applicable to a practical DCS, which consists of several constraints. The design method is validated by examples.     

一种工业无线手操器的设计与实现

基于工业无线网络相关技术,提出了一种低功耗的基于IEEE802．15．4技术的便携式工业无线手操器。首先概述了手操器的工作原理,然后详细介绍了系统硬件电路结构及实现的总体方案,最后重点描述了系统的软件架构及实现方法。测试结果表明该手操器工作稳定,达到相应性能指标,可满足一般工业应用的要求。     

负载共享系统的设计与实现

文章介绍在 Ｌｉｎｕｘ操作系统网络环境下,负载共享系统的基本设计原理和实现方法。重点描述客户一服务器通信模式以及程序模块的算法框架。     

企业售后服务系统的设计与实现

本文采用面向对象的设计和分析方法,以一个售后服务管理系统为例,介绍如何从分析、设计到编程、测试,全面地运用面向对象的方法进行软件开发,重点解释用况图、类图和顺序图的开发过程。读者可以通过本文学习和掌握面向对象建模方法,并以此为例学习如何运用UML的一些最常用的概念和表示法建立自己的应用系统模型。     

四足机器人的设计制作与实现

随着科技的不断进步和计算机技术的快速发展,机器人技术越来越受到人们的普遍关注,并在众多领域得到了广泛应用。本文基于仿生学原理,以atmel单片机为控制器的核心,舵机作为驱动元件,通过keil软件编写程序下载到控制板进行控制,做出了机构灵活、价格低廉的四足机器人。     

自动调零伺服倾角传感器的设计与实现

零位偏差和漂移是所有倾角传感器都待解决的技术难题.本文通过水泡尺旋转180°找平的古老方法深入研究传感器的调平原理,建立一套倾角传感器自动调零的理论和方法.采用步进电机和单片机控制技术设计实现自动调零伺服倾角传感器,很好的解决了零位偏差,时间漂移和温度漂移等问题,使倾角传感器的性能得到提高,具有非常重要的应用价值.     

自动调零伺服器倾角传感器的设计与实现

零位偏差和漂移是所有倾角传感器都待解决的技术难题。本文通过水泡尺旋转1800找平的古老方法深八研究传感器的调平原理，建立一套倾角传感器自动调零的理论和方法。采用步进电机和单片机控制技术设计实现自动调零伺服倾角传感器，很好的解决了零位偏差，时间漂移和温度漂移等问题，使倾角传感器的性能得到提高，具有非常重要的应用价值。     

FIR数字滤波器的DSP实现

针对电力质量分析仪中的信号数字滤波处理部分,基于TMS320VC5402芯片的数字信号处理功能,采用窗函数法,借助MATLAB程序设计语言,设计了FIR数字滤波器,应用DSP汇编语言编程实现了该滤波器。实践证明,该滤波器准确度高、稳定性好,易于移植使用,具有较强的实用性与灵活性。     

一种带自学习算子的GA-BP方法的设计与实现

本文提出一种带自学习算子的GA-BP预测模型,并将其应用于城市发展预测中,在MATLAB,GAOT工具箱上进行了实现,进而分别运用BP,GA-BP,带自学习算子的GA-BP方法对南京的实例进行了预测,将三种方法的预测结果与实际值进行了对比分析,结果表明,增加了自学习算子的GA-BP方法有效且收敛性得到提高。