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

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

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

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

基于线性规划的RTL可满足性求解和性质检验

采用线性规划作为基本工具开发一个RTL可满足性求解器,并将其应用于解决RTL性质检验问题．深入研究了使用线性规划约束对RTL电路元器件的建模方法,得到了一种对RTL电路建模的通用方法．通过将RTL性质转化为虚拟RTL电路,找到了一种验证RTL性质的方法．通过实验,并与采用zchaff布尔可满足性求解器的模型检验工具NuSMV进行比较,证明了基于RTL可满足性求解器的性质验证方法在内存和时间消耗上具有相当大的优势．     

基于SAT求解器的故障树最小割集求解算法

故障树分析广泛应用于核工业、航空航天和交通控制等安全攸关领域的安全性分析。求解故障树的最小割集是故障树分析的关键步骤。目前,对于大规模故障树的最小割集的求解方法主要是将故障树转化为二元决策图之后求解,其主要缺点在于算法在时间和空间上的消耗严重依赖良好的变量顺序。为了减少存储资源并加快求解速度,提出了一种基于可满足性问题的故障树最小割集求解算法。首先,将求解故障树最小割集问题转化为求解布尔可满足性问题。然后,利用可满足性问题求解器,通过迭代分析求得最小可满足解集合,即为对应故障树的最小割集。实验表明,本文算法求得的最小割集准确、有效并且在空间和时间上的消耗均要优于传统的基于二元决策图的故障树最小割集求解算法。     

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

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

一个基于可满足性算法的时序深度计算方法

有界模型校验（Bounded Model Checking）由于验证的不完备性而经常受到验证人员的指责。为了解决这个问题，计算时序深度的算法被提出。该文算法基于可满足性算法引擎，与其它基于可满足性算法引擎的算法不同，为了减少可满足性算法引擎的负担，采用了状态空间显式存储的方法。ISCAS’89的实例很好证明了该算法的有效性。     

可满足性求解技术研究

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

基于改进的遗传算法求解可满足性问题

遗传算法(GA)是由Holland提出的一种基于进化论的仿生算法,非常适于求解最优化问题.为了更好地利用SGA求解SAT问题,在将SAT问题等价转换为{0,1}n上的多项式是否存在零点的判断问题基础上,将局部搜索算法(LSA)与SGA相结合,给出一种求解3-SAT问题的改进混合遗传算法(MHGA),并通过对随机大规模3-SAT问题实例的实际求解验证了MHGA的可行性与有效性.     

求解可满足性问题的改进的模拟退火算法

该文为可满足性问题的高效近似求解提出了改进的模拟退火算法。数值实验表明,对于该文随机产生的测试问题例,改进的模拟退火算法完全胜过局部搜索算法、模拟退火算法以及目前国际上流行的WSAT算法。     

基于增量可满足性的等价性检验方法

组合验证是数字集成电路形式化设计验证的重要方面．该文提出了一种基于增量布尔可满足性的组合等价性检验方法,通过合理选择候选等价结点和增量可满足性算法来提高算法性能,并通过对内部等价结点的置换及将等价关系转化为相应的合取范式公式,避免了误判的发生,又能缩小验证程序的搜索空间．针对ISCAS’85电路的实验结果表明,该文提出的方法比以往同类方法更快、更强健．     

基于MCS51单片机的汽车专用理财电子计算器

设计了由主控制器电路及外围的键盘电路、存储电路、实时时钟电路、LCD显示电路组成的汽车专用理财电子计算器.该计算器用于记录车主日常最关心的汽车消费支出项目,极大地方便了车主.实验证明,计算器具有抗震性和抗干扰性,且结构简单、操作方便.     

基于MCS的SVM参数优化研究

由于优化杜鹃算法是利用了鸟类特殊的利维飞行模式的群体智能算法,并且增加了粒子间的信息交流,故将该算法引入支持向量机惩罚系数和核参数的自动寻优中。给出了实现方式,并讨论了概率参数的设置对收敛性的影响。通过与传统的GA/PSO-SVM对比验证,MCS-SVM方法使得分类精确率平均提高2.28%,既能显著提高分类效率,又表现出很好的泛化性能。     

基于分组的启发式SAT新算法——DC&DS算法

目前提高求解SAT问题完全算法的计算效率问题已成为挑战性研究问题。提出了一种基于启发式分组的SAT完备算法。启发式分组策略将一个全局搜索问题,转为局部搜索问题。并将该策略引入到结合BDD与SAT算法的形式验证中,与一般的启发式SAT算法相比,该算法在求解速度和求解问题的规模等方面都明显地改进了,实验结果表明了该算法的可行性和有效性。     

GF(p)上ECC的有效实现--在MCS51微处理器系列

文章详细描述了在192-bit素域上椭圆曲线公钥密码体制ECC(Elliptic Curve public key Cryptography)Intel MCS51微处理器系列智能卡上的实现过程。采用了Generalized—Mersenne素数作基域GF(p)(p=2^192-2^64-1)，利用模数的特殊形式及椭圆曲线的特殊参数，实现了GF(p)上ECC的全部过程，并且建立了软件库。运行速度表明ECC在计算资源受限、低功耗微处理器上实现是可行的。     

基于单片机的煤气浓度监控系统的设计

介绍了煤气浓度实时监测、采集、处理系统的设计方案。该系统以MCS-51单片机为核心,由防爆型煤气浓度监测器、AD0832及8端口HUB组成,应用于煤气生产各关键部位的煤气浓度监控。该系统通过RS-485实现与工控机(IPC)通信,并由多个模块与工控机(IPC)一起构成基于单片机模块的测控网络。     

广州地铁4号线主控系统

阐述了广州市轨道交通4号线主控系统的应用情况。     

MCS51兼容芯片的正向设计

本文阐述了借助VHDL语言进行MCS51兼容芯片的正各设计与实现的方法。其基本思想是把MCS51芯片的系统结构设计，行为级建模仿真，寄存器级建模仿真，门级综合仿真，FPAG综合仿真等融贯于不可综合层次上和可综合层次上对MCS51芯片的描述和仿真过程中，最终实现对MCS51兼容芯片的正向设计。     

由不交化矩阵求最小割集的改进算法

利用早期不交化法求解最小割集是目前进行故障树定性分析的一种有效方法。但不交化最小割集矩阵行数随着故障树规模的大小呈指数增长,对于数万乃至数百万行的不交化矩阵求解最小割集的过程就会慢得让人无法接受。通过对原算法的分析和改进,采用静态指针法建立动态数组,避免了原算法最耗时间的对不交化矩阵的排序运算。通过与原算法的对比分析,结果验证了本算法的有效性。     

高精度MCS96微控制器压频接口电路设计

介绍了提高ＭＣＳ９６微控制器压频接口电路性能与采样精度的几种方法。     

基于MCS1210的便携式数字血压计的设计

为提高血压测量的抗干扰能力,提升测量准确性和简化操作,利用示波法检测血压的原理,提出了一种便携式数字血压计的设计方案,并进行了主要由微控制器、充放气控制、压力采集、信号调理、人机交互、实时时钟、电源等模块构成的系统架构设计;设计的主要方法是微控制器控制气泵给袖带充放气,袖带压力信号经调理后分离出静压力信号和脉搏波信号,送A/D转换、滤波处理,根据傅里叶拟合法计算收缩压、舒张压等数值,并通过LCD进行血压测量值显示;测试结果表明,该系统具有测量精度高、便携式的特点,具有一定的市场推广价值.