带黑盒组合电路的等价性验证

为了在早期阶段发现电路设计错误,需要对包含未知部分的实现电路和规范电路进行等价性验证.本文提出了一种"分而治之"的方法,把电路划分成若干子电路,使用四值逻辑模拟技术对电路未知部分进行量化,然后对子电路的合取范式进行可满足性验证.这种方法增强了算法的错误检测能力,通过在ISCAS'85基准电路和10个简单组合电路上得到的两组实验数据表明了此算法的有效性和可行性.     

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

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

基于布尔可满足性的电路设计错误诊断算法

提出了一种组合电路设计错误诊断算法,该算法结合传统基于模拟的方法和可满足性问题求解技术,在不依赖于故障模型的条件下实现对电路逻辑错误的诊断定位．提出了基于布尔可满足性的增量式电路诊断方法,通过对可满足解依据电路结构信息筛选分级,提高了多错误诊断定位的分辨率和准确性;并提出多项启发式方法,避免了大量不必要的操作,使算法在时间和内存上保持有效性．实验结果表明,利用形式验证的技术来导向模拟的过程,抓住了高复杂度的多错误定位问题的特征,提高了电路错误诊断的效率．     

使用逻辑锥分割的组合电路等价性验证

为了提高等价性验证在数字电路中的验证效率,提出一种逻辑锥分割和可满足性相结合的方法。通过划分规则把参照电路和实现电路划分成若干个逻辑锥,利用匹配技术对两者的逻辑锥进行匹配,将已匹配的两个逻辑锥的输出用一个异或门连接,从而得到Miter电路,将该结构转换成相应的合取范式,用可满足性引擎来验证Miter电路是否功能等价。在ISCAS’85基准电路的实验结果表明该方法的可行性。     

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

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

基于电路拓扑结构分析的等价性验证方法

随着集成电路设计规模的日益增大,结合多种推理引擎已成为组合电路形式化等价性验证的重要手段.提出一种基于电路拓扑结构分析的组合等价性验证方法,将电路的拓扑结构与验证算法的复杂性关联起来.在验证过程开始之前,利用min-cut方法计算表征电路复杂性的"电路宽度",以确定最佳的推理引擎,避免了传统的引擎切换过程,提高了算法的效率.针对ISCAS85电路的实验结果表明了该方法的效率和可行性.     

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

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

基于BDD的组合电路等价性检验

本文分析了基于BDD的组合电路等价性检验；讨论了构造输出函数的二叉判定图BDD的不同方法，并分析了BDD间布尔操作的不同的算法的异同；然后给出了一种基于BDD的组合电路等价性检验方法。     

基于Mining-SEC方法的电路等价性验证

针对时序电路的等价性验证难题,提出基于Mining-SEC的定界等价性验证方法。将待验证时序电路按时间帧展开为多项式符号代数表示的电路集合,利用时间序列数据挖掘方法挖掘其中的不变量和相应的全局约束,不变量可以是任意多项式。此外还可挖掘电路中的不合法约束和复杂的多项式关系,通过以上方法可以明显降低求解空间。使用基于SMT的验证引擎检验电路等价性。实验结果表明,该方法可以快速地实现验证收敛,得到平均1~2个量级的验证加速,并且可以有效消除虚假验证。     

时序电路等价性检验中的存储元素映射方法研究

随着集成电路规模越来越大,系统的功能日益复杂,功能验证已成为整个设计流程的瓶颈.对于大规模的时序电路,传统基于状态空间遍历的等价性检验方法可能会遇到内存爆炸问题.为了降低等价性检验方法的复杂度,提高验证效率和处理大规模电路的能力,通常需要构造两个被验证电路的存储元素映射之间的映射关系,从而将时序电路等价性检验问题转化为组合电路等价性检验问题.较全面地介绍了时序电路等价性检验的基本方法及其研究进展,讨论了基于存储元素映射的时序电路等价检验方法的基本思想,并介绍了若干具有代表性的存储元素映射方法,展望了集成电路等价检验方法的研究发展方向.     

改进的时间帧展开的时序电路等价验证算法

提出一种改进的基于时间帧展开的时序电路等价验证算法,其来源于模型检查中的基于数学归纳的验证算法,在使用并简化了SAT问题中不可满足子集提取过程后,将基本条件检查和归纳检查合并处理．为了能在时间帧展开过程中减少状态搜索空间,利用结构不动点技术并提出了准动态唯一状态约束等改进的方法．实验表明,随着时间帧的不断展开,文中算法运行时间的增长速度明显慢于基于数学归纳法的验证算法,其适合验证经过时序优化后的电路．     

Formal Verification Techniques Based on Boolean Satisfiability Problem

This paper exploits Boolean satisfiability problem in equivalence checking and model checking respectively. A combinational equivalence checking method based on incremental satisfiability is presented. This method chooses the candidate equivalent pairs with some new techniques, and uses incremental satisfiability algorithm to improve its performance.By substituting the internal equivalent pairs and converting the equivalence relations into conjunctive normal form (CNF)formulas, this approach can avoid the false negatives, and reduce the search space of SAT procedure. Experimental results on ISCAS‘85 benchmark circuits show that, the presented approach is faster and more robust than those existed in literature.This paper also presents an algorithm for extracting of unsatisfiable core, which has an important application in abstraction and refinement for model checking to alleviate the state space explosion bottleneck. The error of approximate extraction is analyzed by means of simulation. An analysis reveals that an interesting phenomenon occurs, with the increasing density of the formula, the average error of the extraction is decreasing. An exact extraction approach for MU subformula, referred to as pre-assignment algorithm, is proposed. Both theoretical analysis and experimental results show that it is more efficient.     

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

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

Easy Cases of Probabilistic Satisfiability

The Probabilistic Satisfiability problem (PSAT) can be considered as a probabilistic counterpart of the classical SAT problem. In a PSAT instance, each clause in a CNF formula is assigned a probability of being true; the problem consists in checking the consistency of the assigned probabilities. Actually, PSAT turns out to be computationally much harder than SAT, e.g., it remains difficult for some classes of formulas where SAT can be solved in polynomial time. A column generation approach has been proposed in the literature, where the pricing sub-problem reduces to a Weighted Max-SAT problem on the original formula. Here we consider some easy cases of PSAT, where it is possible to give a compact representation of the set of consistent probability assignments. We follow two different approaches, based on two different representations of CNF formulas. First we consider a representation based on directed hypergraphs. By extending a well-known integer programming formulation of SAT and Max-SAT, we solve the case in which the hypergraph does not contain cycles; a linear time algorithm is provided for this case. Then we consider the co-occurrence graph associated with a formula. We provide a solution method for the case in which the co-occurrence graph is a partial 2-tree, and we show how to extend this result to partial k-trees with k>2.     

二元可满足性问题有解的充要条件

二元可满足性问题是一个多项式可解的问题．本文首先证明了该问题有解的充要条件，然后给出了判定该问题的一个新的多项式算法．如果判定某个表达式是可满足的话，那么求解算法不需要任何回溯就能准确地给出它的每个解．本文试图通过对二元可满足性的研究为研究其它问题提供一点启示．     

Experimental Study on Strategy of CombiningSAT Algorithms

The effectiveness of many SAT algorithms is mainly reflected by their significant performances on one or several classes of specific SAT problems.Different kinds of SAT algorithms all have their own hard instances respectively.Therefore,to get the better performance on all kinds of problems,SAT solver should know how to select different algorithms according to the feature of instances.In this paper the differences of several effective SAT algorithms are analyzed and two new parameters φand δ are proposed to characterize the feature of SAT instances.Experiments are performed to study the relationship between SAT algorithms and some statistical parameters including φ，δ.Based on this analysis,a strategy is presented for designing a faster SAT tester by carefully combining some existing SAT algorithms.With this strategy,a faster SAT tester to solve many kinds of SAT problem is obtained.     

由一阶逻辑公式得到命题逻辑可满足性问题实例

命题逻辑可满足性(SAT)问题是计算机科学中的一个重要问题.近年来许多学者在这方面进行了大量的研究,提出了不少有效的算法.但是,很多实际问题如果用一组一阶逻辑公式来描述,往往更为自然.当解释的论域是一个固定大小的有限集合时,一阶逻辑公式的可满足性问题可以等价地归约为SAT问题.为了利用现有的高效SAT工具,提出了一种从一阶逻辑公式生成SAT问题实例的算法,并描述了一个自动的转换工具,给出了相应的实验结果.还讨论了通过增加公式来消除同构从而减小搜索空间的一些方法.实验表明,这一算法是有效的,可以用来解决数学研究和实际应用中的许多问题.     

Automatic equivalence checking of programs with uninterpreted functions and integer arithmetic

Proving equivalence of programs has several important applications, including algorithm recognition, regression checking, compiler optimization verification and validation, and information flow checking. Despite being a topic with so many important applications, program equivalence checking has seen little advances over the past decades due to its inherent (high) complexity. In this paper, we propose, to the best of our knowledge, the first semi-algorithm for the automatic verification of partial equivalence of two programs over the combined theory of uninterpreted function symbols and integer arithmetic (UF+IA). The proposed algorithm supports, in particular, programs with nested loops. The crux of the technique is a transformation of uninterpreted functions (UFs) applications into integer polynomials, which enables the precise summarization of loops with UF applications using recurrences. The equivalence checking algorithm then proceeds on loop-free, integer only programs. We implemented the proposed technique in CORK, a tool that automatically verifies the correctness of compiler optimizations, and we show that it can prove more optimizations correct than state-of-the-art techniques.     

基于函数变换的求解SAT问题的新算法

提出了一种基于函数变换的求解SAT问题的新算法,这个新算法利用SAT问题自身的特点将判定问题转化为连续函数的求极值问题。随机选取一组初始值,利用最速下降法求解变换后的连续函数在每个初始值邻域内所能达到的局部极值,如果这个局部极值为0,则该SAT问题就是可满足的。实验结果表明：与现有的求解SAT问题的算法相比,基于函数变换的求解算法在求解速度、成功率和求解问题的规模等方面都有明显的提高。