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

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

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

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

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

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

基于加权数据通路的RTL级低功耗SoC设计

低功耗是SoC设计与评估的重要技术指标之一,现利用加权数据通路,提出一种新的低功耗SoC设计方法。该算法首先利用程序切片技术提取RTL级数据通路,然后采用贝叶斯网络训练获得各数据通路的权重(使用频率),以形成加权数据通路,最后根据各路径权值控制门控信号的产生,对权值小的通路优先插入门控逻辑或合并门控逻辑,从而有效降低系统功耗。实验结果表明,该算法与已有ODC低功耗算法相比功耗平均下降8. 38%,面积开销平均减少6.8%,同时数据通路的简化也使得算法计算负荷大幅下降。     

一个约束可满足性问题的演化算法求解

约束可满足性问题是一大类常出现于现实应用中的复杂问题,因其繁多的约束条件而出名。本文针对一个经典的约束可满足性问题——斑马属谁问题．基于演化算法的框架进行求解。我们采用矩阵的表示方式．并设计了相应的杂交和变异算予。实验表明．演化算法能高效地解决该问题。     

功耗限制下RTL数据通路扫描测试调度方法

本文提出了利用RTL数据通路中的寄存器构造成移位扫描寄存器来测试功能模块的方法,同时提出一种改进的模块调度思想,实现在功耗限制下的测试调度。实验结果表明本文所给出的测试产生算法与调度算法对于由全加器和半加器构成的功能模块具有良好的性能和实用性。     

可满足性求解技术研究

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

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

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

可满足问题中的模型计数

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

基于DNA折纸术求解可满足性问题的计算模型

DNA折纸术是一种全新的DNA自组装方法,具有可编程性、纳米可寻址性等优点,被广泛地应用于DNA计算中.利用DNA折纸术可折叠出特殊结构的特点,在DNA折纸基底上设计了一种求解可满足性问题的计算模型,该模型采用分子信标原理,通过观察荧光的明灭排除非解,从而找出可满足性问题的解.最后通过实例和模拟仿真表明了模型的可行性.     

Bounded Model Checking Using Satisfiability Solving

The phrase model checking refers to algorithms for exploring the state space of a transition system to determine if it obeys a specification of its intended behavior. These algorithms can perform exhaustive verification in a highly automatic manner, and, thus, have attracted much interest in industry. Model checking programs are now being commercially marketed. However, model checking has been held back by the state explosion problem, which is the problem that the number of states in a system grows exponentially in the number of system components. Much research has been devoted to ameliorating this problem.In this tutorial, we first give a brief overview of the history of model checking to date, and then focus on recent techniques that combine model checking with satisfiability solving. These techniques, known as bounded model checking, do a very fast exploration of the state space, and for some types of problems seem to offer large performance improvements over previous approaches. We review experiments with bounded model checking on both public domain and industrial designs, and propose a methodology for applying the technique in industry for invariance checking. We then summarize the pros and cons of this new technology and discuss future research efforts to extend its capabilities.     

RTL数据通路模拟矢量自动生成方法研究与实现

针对已有的RTL数据通路模拟矢量自动生成方法的不足,提出一种利用约束逻辑编辑(CLP)自动生成数据通路模拟矢量的新方法．该方法首先对给定的Verilog RTL描述采用程序切片进行设计化简,然后对化简后的结果基于位向量算术原理生成CLP约束,并利用CLP求解器GProlog进行约束求解,最终生成满足输出要求的模拟矢量．该方法约束求解速度快,生成的约束是统一的,得到的模拟矢量较完备,能满足模拟验证的要求．实验结果表明,文中方法是一种高效的RTL数据通路模拟矢量自动生成方法．     

A Comparison between SAT and CSP Techniques

The aim of this paper is to establish a connection between the propositional logic and the constraint based reasoning frameworks. This work is based on a translation of the satisfiability problem (SAT) into the binary constraint-satisfaction problem (CSP). The structure of the SAT problem and its associated CSP are then exploited together for characterizing tractable SAT problems, increasing the effectiveness of the classical reduction rules: unit clause and monotone literal rules, and expressing the arc and path consistency concepts with logical inference rules. This study leads to compare the behaviors of the DP and MAC procedures for solving respectively a SAT instance and its binary CSP expression.     

Heavy-Tailed Phenomena in Satisfiability and Constraint Satisfaction Problems

We study the runtime distributions of backtrack procedures for propositional satisfiability and constraint satisfaction. Such procedures often exhibit a large variability in performance. Our study reveals some intriguing properties of such distributions: They are often characterized by very long tails or heavy tails. We will show that these distributions are best characterized by a general class of distributions that can have infinite moments (i.e., an infinite mean, variance, etc.). Such nonstandard distributions have recently been observed in areas as diverse as economics, statistical physics, and geophysics. They are closely related to fractal phenomena, whose study was introduced by Mandelbrot. We also show how random restarts can effectively eliminate heavy-tailed behavior. Furthermore, for harder problem instances, we observe long tails on the left-hand side of the distribution, which is indicative of a non-negligible fraction of relatively short, successful runs. A rapid restart strategy eliminates heavy-tailed behavior and takes advantage of short runs, significantly reducing expected solution time. We demonstrate speedups of up to two orders of magnitude on SAT and CSP encodings of hard problems in planning, scheduling, and circuit synthesis.     

在形式验证和ATPG中的布尔可满足性问题

介绍布尔可满足性(SAT)求解程序在测试向量自动生成、符号模型检查、组合等价性检查和RTL电路设计验证等电子设计自动化领域中的应用．着重阐述如何在算法中有机地结合电路拓扑结构及其与特定应用相关的信息，以便提高问题求解效率．最后给出下一步可能的研究方向。     

Penalty Formulations and Trap-Avoidance Strategies for Solving Hard Satisfiability Problems

In this paper we study the solution of SAT problems formulated as discrete decision and discrete constrained optimization problems. Constrained formulations are better than traditional unconstrained formulations because violated constraints may provide additional forces to lead a search towards a satisfiable assignment. We summarize the theory of extended saddle points in penalty formulations for solving discrete constrained optimization problems and the associated discrete penalty method (DPM). We then examine various formulations of the objective function, choices of neighborhood in DPM, strategies for updating penalties, and heuristics for avoiding traps. Experimental evaluations on hard benchmark instances pinpoint that traps contribute significantly to the inefficiency of DPM and force a trajectory to repeatedly visit the same set of or nearby points in the original variable space. To address this issue, we propose and study two trap-avoidance strategies. The first strategy adds extra penalties on unsatisfied clauses inside a trap, leading to very large penalties for unsatisfied clauses that are trapped more often and making these clauses more likely to be satisfied in the future. The second strategy stores information on points visited before, whether inside traps or not, and avoids visiting points that are close to points visited before. It can be implemented by modifying the penalty function in such a way that, if a trajectory gets close to points visited before, an extra penalty will take effect and force the trajectory to a new region. It specializes to the first strategy because traps are special cases of points visited before. Finally, we show experimental results on evaluating benchmarks in the DIMACS and SATLIB archives and compare our results with existing results on GSAT, WalkSAT, LSDL, and Grasp. The results demonstrate that DPM with trap avoidance is robust as well as effective for solving hard SAT problems.     

Relaxations of the Satisfiability Problem Using Semidefinite Programming

We derive a semidefinite relaxation of the satisfiability (SAT) problem and discuss its strength. We give both the primal and dual formulation of the relaxation. The primal formulation is an eigenvalue optimization problem, while the dual formulation is a semidefinite feasibility problem. We show that using the relaxation, a proof of the unsatisfiability of the notorious pigeonhole and mutilated chessboard problems can be computed in polynomial time. As a byproduct we find a new `sandwich" theorem that is similar to the sandwich theorem for Lovász' -function. Furthermore, the semidefinite relaxation gives a certificate of (un)satisfiability for 2SAT problems in polynomial time. By adding an objective function to the dual formulation, a specific class of polynomially solvable 3SAT instances can be identified. We conclude with discussing how the relaxation can be used to solve more general SAT problems and with some empirical observations.