基于混合自动机的PSL模型研究

基于SPICE的计算机仿真方法在混合信号电路验证应用中具有较大的计算开销,讨论基于属性描述的建模方法减小计算开销的问题。通过分析PSL(property specification language)对系统属性的形式化描述方法,并分析混合自动机理论对混合信号系统抽象能力,提出了适合于混合信号电路系统快速验证的PSL模型。结合混合自动机对PSL进行了基于混合自动机语义特点的扩展,使用巴克斯—诺尔范式对其拓展后语法进行规范,提出具有描述混合信号电路行为特性的HAPSL(hybrid automata-base     

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

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

基于边界扫描的混合电路系统机内测试研究

当今电子系统多由模数混合电路组成,随着电子技术的飞速发展,混合电路系统的集成度不断增加,其检测问题一直是测试领域的一个难点;针对混合电路系统的测试特点,以IEEE1149.4标准为研究基础,对某系统控制盒电路进行基于边界扫描的BIT(Builit-in Test机内测试)测试性设计和改造,并将改进后的被测系统进行测试性验证;实验结果表明,该电路系统通过74BCT8373与STA400边界扫描芯片的置换和置人,能够实现混合电路的互连测试与参数测试,且测量迅速,故障定位准确,可以有效提高电路系统的测试性.     

On simulation-based probabilistic model checking of mixed-analog circuits

In this paper, we consider verifying properties of mixed-signal circuits, i.e., circuits for which there is an interaction between analog (continuous) and digital (discrete) values. We use a simulation-based approach that consists of evaluating the property on a representative subset of behaviors and answering the question of whether the circuit satisfies the property with a probability greater than or equal to some threshold. We propose a logic adapted to the specification of properties of mixed-signal circuits in the temporal domain as well as in the frequency domain. We also demonstrate the applicability of the method on different models of Δ–Σ modulators for which previous formal verification attempts were too conservative and required excessive computation time.     

Verifying global start-up for a Möbius ring-oscillator

This paper presents the formal verification of start-up for a differential ring-oscillator circuit used in industrial designs. We present an efficient algorithm for finding DC equilibria to establish a condition that ensure the oscillator is free from lock-up. Further, we present a formal verification solution for the problem. Using dynamical systems theory, we show that any oscillator must have a non-empty set of states from which it fails to start properly. However, it is possible to show that these failures only occur with zero probability. To do so, this paper generalizes the “cone argument” initially presented in (Mitchell and Greenstreet, in Proceedings of the third workshop on designing correct circuits, 1996) and proves the soundness of this generalization. This paper also shows how concepts from analog design such as differential operation can be soundly incorporated into the verification to produce simpler models and reduce the complexity of the verification task.     

Time Domain Verification of Oscillator Circuit Properties

The application of formal methods to analog and mixed signal circuits requires efficient methods for constructing abstractions of circuit behaviors. This paper concerns the verification of properties of oscillator circuits. Generic monitor automata are proposed to facilitate the application of hybrid system reachability computations to characterize time domain features of oscillatory behavior, such as bounds on the signal amplitude and jitter. The approach is illustrated for a nonlinear tunnel-diode circuit model using PHAVer, a hybrid system analysis tool that provides sound verification results based on linear hybrid automata approximations and infinite precision computations.     

Analog Circuit Verification: a State of an Art

Extending formal verification methodology toward analog circuits is a very challenging task that will occupy researchers for some time. To put this challenge in context we sketch some of the history of digital circuit verification as well as more recent attempts to adapt it to continnuous and hybrid systems.     

基于边界扫描的混合信号电路可测性结构设计

在深入研究IEEE1149.1及IEEE1149.4标准的基础上,设计并实现了符合标准的混合信号电路边界扫描可测性结构各组成部分,包括测试访问口控制器、数字边界扫描单元、模拟边界扫描单元、测试总线接口电路及测试寄存器;构建验证电路进行了测试验证。测试结果表明,所设计的混合信号电路可测性结构是可行的,并可以应用到混合信号电路中提高电路的可测试性。     

Time Constrained Verification of Analog Circuits using Model-Checking Algorithms

In this contribution we present algorithms for model checking of analog circuits enabling the specification of time constraints. Furthermore, a methodology for defining time-based specifications is introduced. An already known method for model checking of integrated analog circuits has been extended to take into account time constraints. The method will be presented using three industrial circuits. The results of model checking will be compared to verification by simulation.     

The Case for Analog Circuit Verification

The traditional approach to validate analog circuits is to utilize extensive SPICE-level simulations. The main challenge of this approach is knowing when all important corner cases have been simulated. A new alternative is to utilize formal verification techniques. This paper utilizes a simple example to illustrate the potential flaws of a simulation-only based validation methodology and the potential benefits of formal verification of analog circuits.     

基于IEEE1149.4的混合信号边界扫描测试控制器设计

简要介绍了IEEE1149.4混合信号测试总线及其特点,并根据该标准定义的测试结构对混合信号电路的测试方法进行研究,设计出符合IEEE1149.4标准的边界扫描控制器及其验证电路,实验结果表明该测试控制器能实现对混合信号电路板的测试,大大提高了混合信号电路板的可观性和可控性.     

Efficient Combinational Verification Using Overlapping Local BDDs and a Hash Table

We propose a novel methodology that combines local BDDs with a hash table for very efficient verification of combinational circuits. The main purpose of this technique is to remove the considerable overhead associated with case-by-case verification of internal node pairs in typical internal correspondence based verification methods. Two heuristics based on the number of structural levels of circuitry looked at and the total number of nodes in the BDD manager are used to control the BDD sizes and introduce new cutsets based on already found equivalent nodes. We verify the ISCAS85 benchmark circuits and demonstrate significant speedup over existing methods. We also verify several hard industrial circuits and show our superiority in extracting internal equivalences.     

事务级形式验证技术及8051验证模型

提出一种基于事务的用于电路系统的形式验证方法(TBFV)．应用该方法，验证工程师可以在行为级对系统进行验证，无需了解设计的细节．为了对该方法进行示范，验证了8051的RTL级实现，并给出了8051指令集的TBFV模型．     

硬件加速功能验证问题的DAG划分算法

功能验证是超大规模集成电路(very large scale integration, VLSI)设计的一个基本环节. 随着超大规模电路的普及与发展, 在单处理器上对整个电路进行功能验证在可行性和效率上都存在较大的缺陷. 基于硬件加速器的功能验证是将整个电路划分成若干个规模更小的子电路; 然后在多个硬件处理器上并行的执行功能验证. 当电路划分结果的并行性较优时可提高功能验证的效率, 缩短时间周期. 类似电路设计中的其他划分问题, 用于硬件加速功能验证的电路划分问题可以被抽象成图划分问题. 相较于传统图划分问题, 硬件加速功能验证的划分问题还需要保证较小的模拟深度和较高的调度并行性. 为了满足硬件加速功能验证的划分需求, 提出了一种基于传统多级图划分策略的有效算法. 该算法结合调度思想, 利用电路的关键路径信息和时序信息, 将硬件加速功能验证问题转化为有向无环图的多级划分问题. 随机电路网表数据的实验结果表明, 所构造的算法可以有效的减少关键路径长度并且不会引起切边数的增长恶化.     

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

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

Practical formal verification in microprocessor design

Practical application of formal methods requires more than advanced technology and tools; it requires an appropriate methodology. A verification methodology for data-path-dominated hardware combines model checking and theorem proving in a customizable framework. This methodology has been effective in large-scale industrial trials, including verification of an IEEE-compliant floating-point adder     

基于IEEE1149.4的差分测试方法的研究与应用

IEEE1149．4标准（DOT4）为解决数模混合电路的边界扫描测试提供了有效的方法,对于数模混合差分电路的互联测试,一直是数模混合电路中巨联测试的重点之一,介绍了一种基于此标准的差分互联电路的测试方法以及差分模拟边界扫描单元的应用,对混合差分电路实现了简荤互联和扩展互联的边界扫描测试,从而提高了差分电路互联测试的能力。