集成电路的设计验证

集成电路设计业正面临着一系列的挑战:芯片性能越来越强,规模越来越大,开发周期越来越长,设计质量越来越难于控制。而随着半导体技术的发展,设计验证已经逐渐成为大规模集成电路设计的主要瓶颈。而设计验证最基本的内容是功能验证,用于判别设计规范和实现之间是否一致。对模拟验证、形式验证中的等价性检验和模型检验进行了介绍,然后引入传统方法的一种改进——基于覆盖率的验证方法。     

集成电路的设计验证

集成电路设计业正面临着一系列的挑战：芯片性能越来越强，规模越来越大，开发周期越来越长，设计质量越采越难于控制。而随着半导体技术的发展，设计验证已经逐渐成为大规模集成电路设计的主要瓶颈。而设计验证最基本的内容是功能验证，用于判别设计规范和实现之间是否一致；对模拟验证、形式验证中的等价性检验和模型检验进行了介绍，然后引入传统方法的一种改进——基于覆盖率的验证方法。     

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

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

基于状态转换图同构求解的等价性验证算法

文中提出了一种基于状态转换图同构求解的时序电路等价性验证算法.算法将两时序电路的等价性问题转化为验证相应状态转换图的同构性.首先将初始状态对匹配为待验证对,然后采用递归的方法验证以初始状态对的下一状态对为初始状态的子状态转换图是否同构,从而得到时序电路是否等价的信息.若两状态转换图同构,则两图中的状态均可--配对为待验证状态对,即所有的代验证状态对均为等价状态对.该方法可以有效地克服算法级描述到底层实现之间跨度太大的问题.     

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

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

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

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

基于虚拟可重构平台的时序电路演化设计

目前,电路进化设计是演化硬件研究的主要方向之一。而时序电路由于存在反馈环不便于进行电路描述和软件仿真。文中对时序电路的演化设计方法进行了改进,提出了专门针对时序电路演化的虚拟可重构平台,建立起电路编码与HDL代码的映射关系。应用TEXTIO和MATLAB来辅助仿真测试过程,使测试向量数量巨大、难以处理的问题得到很好地解决。最后调用ModelSim完成了FSM的演化实验。实验结果验证了基于此平台演化时序电路的可行性和有效性。     

基于HDL仿真的同步时序电路演化方法

时序电路存在反馈环,不便于电路描述和软件仿真,很难进行演化。为此,以D触发器和逻辑门为基本单元,构建描述时序电路的全向连接电路网络模型。建立电路编码、电路拓扑与硬件描述语言(HDL)代码文件之间的映射关系,设计由电路编码获取相应HDL代码的方法,利用批处理技术实现电路评估过程的自动运行。四倍分频器电路演化实验结果验证了该方法的可行性与有效性。     

基于HPVEE的数字电路器件仿真及其在测试上的应用

介绍了使用HPVEE (图形编程语言 )进行通用数字集成电路 (包括组合电路和时序电路 )器件仿真的方法 ,给出了利用该仿真电路实现通用数字集成电路的在线测试与故障诊断的具体实例。     

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

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

Program equivalence checking by two-tape automata

This paper shows how two-tape automata can be employed to design efficient equivalence checking procedures for sequential programs. The semantics of sequential programs is defined in terms of dynamic logic structures. If a dynamic frame is acyclic (i.e., all program statements are irreversible), then it can be specified by means of a two-tape deterministic automaton. Then the equivalence checking problem for sequential programs in which the semantics of operators is determined by acyclic dynamic frames can be reduced to the emptiness problem for two-tape automata (compound machines).     

Principles of sequential-equivalence verification

Traditionally, designers use simulation to check the functional equivalence of specification and implementation models. Although simulation can eliminate some or most design errors, it can never completely certify design correctness. Formal equivalence verification (FEV) is a viable alternative that has gained wide industrial acceptance. FEV, which uses automata theory and mathematical logic to formally reason about the correctness of design transformations, is broadly divided into two categories: combinational and sequential. This article is a general survey of conceptual and algorithmic approaches to sequential equivalence checking. Although this fundamental problem is very complex, recent advances in satisfiability solvers and ATPG approaches are making good headway.     

Distributed On-the-Fly Equivalence Checking

On-the-fly equivalence checking consists in comparing two Labeled Transition Systems (Ltss) modulo a given equivalence relation by exploring them in a demand-driven way. Since it avoids the explicit construction of Ltss, this method is able to detect errors even in systems that are too large to fit in the memory of a computer. In this paper, we aim at further improving the performance of on-the-fly equivalence checking using several machines connected by a network. We propose DSolve, a new algorithm for distributed on-the-fly resolution of Boolean Equation Systems (Bess), which enables equivalence checking modulo various relations characterized in terms of Bess. DSolve serves as verification engine for the distributed version of Bisimulator, an on-the-fly equivalence checker developed within the Cadp verification toolbox using the Open/Cæsar environment. Our experimental measures show quasi-linear speedups and a good scalability of the distributed version of Bisimulator w.r.t. its sequential version.     

Functional Equivalence Verification Tools in High-Level Synthesis Flows

Editor's note:High-level synthesis facilitates the use of formal verification methodologies that check the equivalence of the generated RTL model against the original source specification. The article provides an overview of sequential equivalence checking techniques, its challenges, and successes in real-world designs.—Andres Takach, Mentor Graphics     

组合电路等价性检验方法研究

分析了数字电路等价性检验方法的基本原理，对组合电路等价性检验方法进行了综合研究，讨论了各种方法的特点，指出了各种方法的优缺点及其适用场合，总结了组合电路等价性检验方法的发展规律，指出了未来的发展方向。     

多核模型检测工具CTAV的实现与优化

在计算机计算能力大大增强的时代,为了提高对时间自动机进行空性检测的效率,进一步高效利用多核处理器的优势,研究了利用Büchi自动机的多核空性判定算法改造CTAV,使它成为一款时间自动机模型关于线性时序逻辑的多核模型检测工具,从而提高模型检测的效率.通过对符号化状态之间包含关系的研究,利用这种状态之间的包含关系更快的找到接收路径并避免不必要的状态展开,实现了多核模型检测算法的优化,对比了一些常见模型的验证数据,取得了更好的效果.     

通用CPU设计验证中的等价性检验方法

针对传统的模拟验证方法需要大量的时间且难以获得完全的覆盖率的局限性,提出了目前应用最广泛的一种形式验证方法——等价性检验在一款通用CPU设计验证中的应用方案,包括寄存器传输级(RTL)设计与门级网表、门级网表与门级网表、RTL设计与RTL设计之间的功能等价性验证．此外,给出了验证过程中一些常见问题的解决办法．验证结果表明了该方法的可行性,显著地减少了门级模拟的时间．     

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.