Automatic Vector Generation Using Constraints and Biasing

Constraining and biasing are frequently used techniques to enhance the quality of randomized vector generation. In this paper, we present a novel method that combines constraints and input biasing in automatic bit-vector generation for block-level functional verification of digital designs, which is implemented in a tool called SimGen. Vector generation in SimGen is confined to a legal input space that is defined by constraints symbolically represented in Binary Decision Diagrams (BDDs). A constraint involving state variables in the design defines a state-dependent legal input space. Input biasing can also depend on the state of the design. The effect of constraints and input biasing are combined to form what we called the constrained probabilities of input vectors. An algorithm is developed to efficiently generate input vectors on-the-fly during simulation. The vector generation is a one-pass process, i.e., no backtracking or retry is needed. Also, we describe methods of minimizing the constraint BDDs in an effort to reduce the simulation-time overhead of SimGen. Furthermore we discuss the application of SimGen to a set of commercial design blocks.     

On Design Validation Using Verification Technology

Despite great advances in the area of Formal Verification during the last ten years, simulation is currently the primary means for performing design verification. The definition of an accurate and pragmatic measure for the coverage achieved by a suite of simulation vectors and the related problem of coverage directed automatic test generation are of great importance. In this paper we introduce a new set of metrics, called the Event Sequence Coverage Metrics (ESCMs). Our approach is based on a simple and automatic method to extract the control flow of a circuit so that the resulting state space can be explored for validation coverage analysis and automatic test generation. During simulation we monitor, in addition to state and transition coverage, whether certain control event sequences take place or not. We then combine formal verification techniques, using BDDs as the underlying representation, with traditional ATPG and behavioral test generation techniques to automatically generate additional sequences which traverse uncovered parts of the control state graph, or exercise an uninstantiated control event sequence.     

SoC设计验证策略及方法学

验证在SoC设计过程中有十分重要的作用,它将影响到芯片的整体开销和质量.本文首先介绍了当前业界比较常用的一些验证技术的特点,包括仿真技术、静态验证技术、形式验证、物理验证等,然后通过实例论述在SoC设计验证中的关键技术--重用技术、随机约束验证、自检技术和形式断言验证.     

Cohesive Coverage Management: Simulation Meets Formal Methods

It has been advocated by many experts in design verification that the key to successful verification convergence lies in developing the verification plan with adequate formal rigor. Traditionally, the verification plans for simulation and formal property verification (FPV) are developed in different ways, using different formalisms, and with different coverage goals. In this paper, we propose a framework where the difference between formal properties and simulation test points is diluted by using methods for translating one form of the specification to the other. This allows us to reuse simulation coverage to facilitate formal verification and to reuse proven formal properties to cover simulation test points. We also propose the use of inline assertions in procedural (possibly randomized) test benches, and show that it facilitates the use of hybrid verification techniques between simulation and bounded model checking. We propose the use of promising combinations of formal methods presented in our earlier papers to shape a hierarchical verification flow where simulation and formal methods aim to cover a common design intent specification. The proposed flow is demonstrated using a detailed case study of the ARM AMBA verification benchmark. We believe that the methods presented in this work will stimulate new thought processes and ultimately lead to wider adoption of cohesive coverage management techniques in the design intent validation flow.     

Nonparametric Combinatorial Regression for Shape Constrained Modeling

We introduce a unified approach for calculating nonparametric shape constrained regression. Enforcement of the shape constraint often accounts for the impact of a physical phenomenon or a specific property. It also improves the model's predicability and facilitates subsequent optimizations. The regression models are built by transforming the problem into the combinatorial domain where the shape constraints are imposed by bounding the combinatorial search space. We start by addressing isotonicity shape constraint using a dynamic programming algorithm and demonstrate how the problem can be mapped to the graph combinatorics domain. Next we show how a number of other important shape constraints including unimodality, convexity, limited level set, and limited slope can be addressed using the same framework. The flexibility of proposed framework enables solving the shape constrained regression problem with an arbitrary user-defined error metric. This flexibility is exploited to add robustness against outliers to the model. The algorithms are described in detail and their computational complexity is established. The performance and effectiveness of the shape constrained regression is evaluated on traces of temperature and humidity measurements from a deployed sensor network where a high degree of accuracy and robustness is demonstrated.      

片上系统的模型检验

片上系统(SoC)的验证是一个比较复杂的问题，仅靠模拟仿真无法保证SoC设计的正确。形式化方法是利用数学推理的方法来证明其正确．是对SoC设计进行验证的一条重要途径。模型检验技术是一种完全自动化的形式化方法，针对模型检验技术，讨论了在SoC验证中的应用，指出在SoC设计中，只有把模拟仿真与形式化、半形式化的方法结合起来，才能更好的对SoC进行验证。     

Generation of design verification tests from behavioral VHDLprograms using path enumeration and constraint programming

A method for generation of design verification tests from behavior-level VHDL programs is presented. The method generates stimuli to execute desired control-flow paths in the given VHDL program. This method is based on path enumeration, constraint generation and constraint solving techniques that have been traditionally used for software testing. Behavioral VHDL programs contain multiple communicating processes, signal assignment statements, and wait statements which are not found in traditional software programming languages. Our model of constraint generation is specifically developed for VHDL programs with such constructs. Control-flow paths for which design verification tests are desired are specified through certain annotations attached to the control statements in the VHDL programs. These annotations are used to enumerate the desired paths. Each enumerated path is translated into a set of mathematical constraints corresponding to the statements in the path. Methods for generating constraint variables corresponding to various types of carriers in VHDL and for mapping various VHDL statements into mathematical relationships among these constraint variables are developed. These methods treat spatial and temporal incarnations of VHDL carriers as unique constraint variables thereby preserving the semantics of the behavioral VHDL programs. Constraints are generated in the constraint programming language CLP(R) and are solved using the CLP(R) system. A solution to the set of constraints so generated yields a design verification test sequence which can be applied for executing the corresponding control path when the design is simulated. If no solution exists, then it implies that the corresponding path can never be executed. Experimental studies pertaining to the quality of path coverage and fault coverage of the verification tests are presented     

Linear antenna array pattern synthesis with prescribed broad nulls

A technique of synthesizing an antenna array pattern with prescribed broad nulls is presented. The array pattern synthesis problem is formulated as a least-square null constrained optimization problem. Numerical techniques based on the matrix factorization method are developed for reducing the computational complexity of determining the optimal weight vector. Subsequently, a set of eigenvector constraints are used to approximate the effect of the quadratic constraint. Numerical results are presented to illustrate the performance achievable     

SEChecker: A Sequential Equivalence Checking Framework Based on ${K}$th Invariants

In recent years, considerable research efforts have been devoted to utilizing circuit structural information to improve the efficiency of Boolean satisfiability (SAT) solving, resulting in several efficient circuit-based SAT solvers. In this paper, we present a sequential equivalence checking framework based on a number of circuit-based SAT solving techniques as well as a novel invariant checker. We first introduce the notion of $k$th invariants. In contrast to the traditional invariants that hold for all cycles, $k$ th invariants are guaranteed to hold only after the $k$th cycle from the initial state. We then present a bounded model checker (BMChecker) and an invariant checker (IChecker), both of which are based on circuit SAT techniques. Jointly, BMChecker and IChecker are used to compute the $k$th invariants, and are further integrated in a sequential circuit SAT solver for checking sequential equivalence. Experimental results demonstrate that the new sequential equivalence checking framework can efficiently verify large industrial designs that cannot be verified by existing solutions.      

林业信息系统模型检测应用方法研究

模型检测作为一种形式化验证技术已成功应用于硬件以及协议的性质验证过程,目前正转向软件验证领域并逐渐扩展其应用范围。针对特定的森林防火专家系统的知识库规则,研究其所需满足的性质规范的形式化验证问题。首先将规则体描述为状态迁移图,通过引入转换函数对状态迁移图的变迁过程及状态性质进行了有效说明,然后将性质规范描述为相应的时序逻辑表达式,最后通过实例对模型检测过程进行了详细说明,本文的研究成果有效地说明了将模型检测应用于森林防火专家系统等林业信息系统的可行性与正确性。     

IP最小参数空间提取模型

为了能使IP在不同的系统中被重用,通常将IP参数化.参数的广泛使用一方面给IP重用带来方便,另一方面大量的参数又将给IP认证、验证和集成带来新的问题.针对IP参数化带来的问题提出一种新的递交方法,首先基于参数及其相互依赖关系,对大量的参数进行统一描述,再构成参数域值图PDG将参数空间分为多个正交的有效予空间.依靠PDG,用户进行参数检查所需要的测试向量条件可以自动产生,而且也可以获取验证环境的约束条件,收集、分析功能覆盖率的数据,减少了系统设计过程中的验证工作.     

分布式MIMO雷达的目标定位

针对多输入多输出雷达系统，研究了目标定位问题，并提出基于双基测距的分布式多输入多输出(Multiple-Input Multiple-Output, MIMO)雷达的目标定位算法。首先，通过引入多余参数和这些参数与未知目标定位的关系，将目标定位问题转化为约束二次规划(Quadratically Constrained Quadratic Programming, QCQP)问题，然后，考虑到QCQP问题是非凸和NP-Hard，再将每个非凸约束近似为线性约束，最终QCQP问题就转化为线性约束二次规划(Linearly Constrained Quadratic Programming, LCQP)问题。最后，利用迭代约束权重最小二乘(Iterative Constrained Weighted Least Square, ICWLS)算法求解LCQP问题。实验数据表明，提出的ICWLS算法能够收敛于一个最优值。     

A nonexpansive monotonicity constraint operator for use in constrained iterative deconvolution

This letter describes a nonexpansive monotonicity constraint operator. It can be used in constrained iterative deconvolution in order to compute impulse response functions which are known to be piecewise monotonous or piecewise constant. The operator may also be combined with, for instance, positivity and finite support constraint operators to put further constraints upon the impulse response function. Constrained deconvolutions are generally less noise-sensitive than nonconstrained deconvolutions.     

Analyzing encryption protocols using formal verification techniques

An approach to analyzing encryption protocols using machine-aided formal verification techniques is presented. The properties that the protocol should preserve are expressed as state invariants, and the theorems that must be proved to guarantee that the cryptographic facility satisfies the invariants are automatically generated by the verification system. A formal specification of an example system is presented, and several weaknesses that were revealed by attempting to verify and test the specification formally are discussed.<>     

Invisible formal methods for embedded control systems

Embedded control systems typically comprise continuous control laws combined with discrete mode logic. These systems are modeled using a hybrid automaton formalism, which is obtained by combining the discrete transition system formalism with continuous dynamical systems. This paper develops automated analysis techniques for asserting correctness of hybrid system designs. Our approach is based on symbolic representation of the state space of the system using mathematical formulas in an appropriate logic. Such formulas are manipulated using symbolic theorem proving techniques. It is important that formal analysis should be unobtrusive and acceptable to engineering practice. We motivate a methodology called invisible formal methods that provides a graded sequence of formal analysis technologies ranging from extended typechecking, through approximation and abstraction, to model checking and theorem proving. As an instance of invisible formal methods, we describe techniques to check inductive invariants, or extended types, for hybrid systems and compute discrete finite state abstractions automatically to perform reachability set computation. The abstract system is sound with respect to the formal semantics of hybrid automata. We also discuss techniques for performing analysis on nonstandard semantics of hybrid automata. We also briefly discuss the problem of translating models in Simulink/Stateflow language, which is widely used in practice, into the modeling formalisms, like hybrid automata, for which analysis tools are being developed.     

Constrained solutions in importance via robust statistics

The problem of estimating estimating expectations of functions of random vectors via simulation is investigated. Monte Carlo simulations, also known as simple averaging, have been used as a direct means of estimation. A technique known as importance sampling can be used to modify the simulation via weighted averaging in the hope that the estimate will converge more rapidly to the expected value than standard Monte Carlo simulations. A constrained optimal solution to the problem of minimizing the variance of the importance sampling estimator is derived. This is accomplished by finding the distribution which is closest to the unconstrained optimal solution in the Ali-Silvey sense (S. Ali et al., 1966). The solution from the constraint class is shown to be the least favorable density function in terms of Bayes risk against the optimal density function. Examples of constraint classes, which include ϵ-mixture, show that the constrained optimal solution can be made arbitrarily close to the optimal solution. Applications to estimating probability of error in communication systems are presented     

Sparsity in optical flow and trajectories

In this article, we apply sparse constraints to improve optical flow and trajectories. We apply sparsity in two ways. First, with two-frame optical flow, we enforce a sparse representation of flow patches using a learned overcomplete dictionary. Second, we apply a low-rank constraint to trajectories via robust coupling. Optical flow is an ill-posed underconstrained inverse problem. Many recent approaches use total variation to constrain the flow solution to satisfy color constancy. In our first results presented, we find that learning a 2D overcomplete dictionary from the total variation result and then enforcing a sparse constraint on the flow improves the result. A new technique using partially overlapping patches accelerates the calculation. This approach is implemented in a coarse-to-fine strategy. Our results show that combining total variation and a sparse constraint from a learned dictionary is more effective than total variation alone. In the second part, we compute optical flow and trajectories from an image sequence. Sparsity in trajectories is measured by matrix rank. We introduce a low-rank constraint of linear complexity using random subsampling of the data. We demonstrate that, by using a robust coupling with the low-rank constraint, our approach outperforms baseline methods on general image sequences.     

A new approach to the optimization of robust antenna arrayprocessors

The authors present a method for solving a class of optimization problems with nonsmooth constraints. In particular, they apply the method to the design of narrowband minimum-power antenna array processors which are robust in the presence of errors such as array element placement, look direction misalignment, and frequency offset. They first show that the constrained minimum power problem has a unique global minimum provided that the constraint set is nonempty. Then it is shown how the design problem derived directly from considerations of the sensitivity of the antenna array processor to errors can be transformed into a quadratic programming problem with linear inequality constraints which can be solved efficiently by the standard active set strategy. They also present numerical results for two types of nonsmooth constraints developed to provided robustness. These results confirm the effectiveness of the method