利用FAN算法进行组合电路的等价性检验*

讨论了组合电路的等价性检验方法,分析了FAN算法的关键技术。利用该算法进行了组合电路的等价性检验,实验结果表明了该方法的有效性。     

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

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

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

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

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

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

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

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

片上系统高层等价性检验研究进展

针对近年来SoC领域的工作,首先分析了高层等价性检验的难点;然后从算法类型归类角度对各种高层等价性检验方法进行了概述评论,同时分析了各类算法的优缺点和现有算法的主要技术手段;最后讨论了SoC高层等价性检验方法目前面临的挑战,并对该领域今后的研究方向进行了展望.     

使用输出分组和电路可满足性的等价性验证算法

介绍了一种使用电路可满足性解算器的组合电路等价性验证算法．对包含多输出的复杂验证问题,首先对联接电路作输出分组,将等价性验证问题转化为包含若干个组的电路可满足性问题,继而使用电路解算器解决问题．同时,注意各个子问题间的有用隐含信息的共享,减小了SAT推理的搜索空间．实验结果表明,该算法是实用有效的．     

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

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

用VIS验证微处理器PIC

近年来,二叉判定图ＢＤＤ和符号模型检验在形式验证数字电路设计中取得了突破性进展,文中介绍了符号模型检验的基本原理和方法,重点介绍了如何用ＶＩＳ系统验证微处理器ＰＩＣ设计的正确性。利用ＶＩＳ证明了ＰＩＣ设计部分电路的等价性。发现了一个设计错误并证明了ＰＩＣ中一些重要模块的特性。     

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

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

Error Diagnosis in Equivalence Checking of High Performance Microprocessors

We describe techniques for diagnosing errors in formal equivalence checking of RTL and transistor level models of high performance microprocessors at Freescale Semiconductor Inc. We use Symbolic Trajectory based Evalaution (STE) for combinational equivalence checking. STE accurately captures transistor level behaviors. We use simulation based error diagnosis techniques and present a seamless integration of them in our current verification environments.     

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

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

Application of BDDs in Boolean matching techniques for formal logic combinational verification

Verifying that an implementation of a combinational circuit meets its golden specification is an important step in the design process. As inputs and outputs can be swapped by synthesis tools or by interaction of the designer, the correspondence between the inputs and the outputs of the synthesized circuit and the inputs and the outputs of the golden specification has to be restored before checking equivalence. In this paper, we review the main approaches to this isomorphism problem and show how to apply OBDDs in order to obtain efficient methods. Published online: 15 May 2001     

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.     

Limits of Using Signatures for Permutation Independent Boolean Comparison

This paper addresses problems that arise while checking the equivalence of two Boolean functions under arbitrary input permutations. The permutation problem has several applications in the synthesis and verification of combinational logic: it arises in the technology mapping stage of logic synthesis and in logic verification. A popular method to solve it is to compute a signature for each variable that helps to establish a correspondence between the variables. Several researchers have suggested a wide range of signatures that have been used for this purpose. However, for each choice of signature, there remain variables that cannot be uniquely identified. Our research has shown that, for a given example, this set of problematic variables tends to be the same–regardless of the choice of signatures. The paper investigates this problem.