公开(公告)号：US07853906B2

公开(公告)日：2010-12-14

申请号：US11689803

申请日：2007-03-22

申请人： Malay Ganai ,  Aarti Gupta

发明人： Malay Ganai ,  Aarti Gupta

IPC分类号： G06F9/45 ,  G06F17/50

CPC分类号： G06F17/504

摘要： An accelerated High-Level Bounded Model Checking method that efficiently extracts high-level information from the model, uses that extracted information to obtain an improved verification model, and applies relevant information on-the-fly to simplify the BMC-problem instances.

摘要翻译： 一种从模型中有效提取高级别信息的加速高级有界模型检查方法，利用提取的信息获取改进的验证模型，并即时应用相关信息，简化BMC问题实例。

公开(公告)号：US07711525B2

公开(公告)日：2010-05-04

申请号：US10157486

申请日：2002-05-30

申请人： Malay Ganai ,  Lintao Zhang ,  Aarti Gupta ,  Zijiang Yang ,  Pranav Ashar

发明人： Malay Ganai ,  Lintao Zhang ,  Aarti Gupta ,  Zijiang Yang ,  Pranav Ashar

IPC分类号： G06F17/10

CPC分类号： G06F17/504

摘要： A method for bounded model checking of arbitrary Linear Time Logic temporal properties. The method comprises translating properties associated with temporal operators F(p), G(p), U(p, q) and X(p) into property checking schemas comprising Boolean satisfiability checks, wherein F represents an eventuality operator, G represents a globally operator, U represents an until operator and X represents a next-time operator. The overall property is checked in a customized manner by repeated invocations of the property checking schemas for F(p), G(p), U(p, q), X(p) operators and standard handling of atomic propositions and Boolean operators.

摘要翻译： 一种用于任意线性时间逻辑时间属性的有界模型检查的方法。 该方法包括将与时间运算符F（p），G（p），U（p，q）和X（p）相关联的属性转换成包括布尔可满足性检查的属性检查模式，其中F表示可能性运算符，G表示全局 运算符，U表示直到运算符，X表示下一运算符。 通过重复调用F（p），G（p），U（p，q），X（p）运算符的属性检查模式以及原子命题和布尔运算符的标准处理来检查整体属性。

公开(公告)号：US20090282288A1

公开(公告)日：2009-11-12

申请号：US12397696

申请日：2009-03-04

申请人： Chao Wang ,  Aarti Gupta

发明人： Chao Wang ,  Aarti Gupta

IPC分类号： G06F11/07

CPC分类号： G06F11/3612

摘要： A system and method for dynamic data race detection for concurrent systems includes computing lockset information using a processor for different components of a concurrent system. A controlled execution of the system is performed where the controlled execution explores different interleavings of the concurrent components. The lockset information is used during the controlled execution to check whether a search subspace associated with a state in the execution is free of data races. A race-free search subspace is dynamically pruned to reduce resource usage.

摘要翻译： 用于并行系统的用于动态数据竞争检测的系统和方法包括使用用于并发系统的不同组件的处理器来计算锁定信息。 执行系统的受控执行，其中受控执行探讨并发组件的不同交织。 在受控执行期间使用锁定信息来检查与执行中的状态相关联的搜索子空间是否没有数据竞争。 动态修剪无竞争的搜索子空间，以减少资源的使用。

公开(公告)号：US20090204968A1

公开(公告)日：2009-08-13

申请号：US12367140

申请日：2009-02-06

申请人： Vineet Kahlon ,  Chao Wang ,  Aarti Gupta

发明人： Vineet Kahlon ,  Chao Wang ,  Aarti Gupta

IPC分类号： G06F9/44

CPC分类号： G06F11/3604 ,  G06F11/30

摘要： A system and method for analyzing concurrent programs that guarantees optimality in the number of thread inter-leavings to be explored. Optimality is ensured by globally constraining the inter-leavings of the local operations of its threads so that only quasi-monotonic sequences of threads operations are explored. For efficiency, a SAT/SMT solver is used to explore the quasi-monotonic computations of the given concurrent program. Constraints are added dynamically during exploration of the concurrent program via a SAT/SMT solver to ensure quasi-montonicity for model checking.

摘要翻译： 一种用于分析并发程序的系统和方法，保证要探索的线程间隔数量的最优化。 通过全局约束其线程的本地操作的离开来确保优化，从而仅探索准单调序列的线程操作。 为了效率，使用SAT / SMT求解器来探索给定并发程序的准单调计算。 通过SAT / SMT求解器在并发程序的探索期间动态添加约束，以确保模型检查的准单调性。

公开(公告)号：US20090007038A1

公开(公告)日：2009-01-01

申请号：US11950730

申请日：2007-12-05

申请人： Chao Wang ,  Aarti Gupta ,  Hyondeuk Kim

发明人： Chao Wang ,  Aarti Gupta ,  Hyondeuk Kim

IPC分类号： G06F17/50

CPC分类号： G06F17/504

摘要： Systems and methods are disclosed for performing counterexample guided abstraction refinement by transforming a design into a functionally equivalent Control and Data Flow Graph (CDFG); performing a hybrid abstraction of the design; generating a hybrid abstract model; and checking the hybrid abstract model.

摘要翻译： 公开了用于通过将设计变换成功能等同的控制和数据流图（CDFG）来执行反例引导的抽象改进的系统和方法; 执行设计的混合抽象; 产生混合抽象模型; 并检查混合抽象模型。

公开(公告)号：US20060190864A1

公开(公告)日：2006-08-24

申请号：US11037920

申请日：2005-01-18

申请人： Malay Ganai ,  Aarti Gupta ,  Pranav Ashar

发明人： Malay Ganai ,  Aarti Gupta ,  Pranav Ashar

IPC分类号： G06F17/50

CPC分类号： G11C29/54 ,  G06F17/504 ,  G11C2029/0401

摘要： A computer-implemented method for augmenting SAT-based BMC to handle embedded memory designs without explicitly modeling memory bits. As is known, verifying designs having large embedded memories is typically handled by abstracting out (over-approximating) the memories. Such abstraction is not useful for finding real bugs. SAT-based BMC, as of now, is incapable of handling designs with explicit memory modeling due to enormously increased search space complexity. Advantageously, our method does not require analyzing the designs and also guarantees not to generate false negatives.

摘要翻译： 一种用于增加基于SAT的BMC来处理嵌入式存储器设计而不明确建模存储器位的计算机实现的方法。 众所周知，验证具有大嵌入存储器的设计通常通过抽象出（过近似）存储器来处理。 这样的抽象对于找到真实的错误是没有用的。 目前，基于SAT的BMC由于搜索空间复杂度的大幅增加，无法处理具有显式内存建模的设计。 有利的是，我们的方法不需要分析设计，也不保证不产生假阴性。

公开(公告)号：US20050149301A1

公开(公告)日：2005-07-07

申请号：US11053915

申请日：2005-02-10

申请人： Aarti Gupta ,  Pranav Ashar ,  Sharad Malik

发明人： Aarti Gupta ,  Pranav Ashar ,  Sharad Malik

IPC分类号： G06F17/10 ,  G06F17/50

CPC分类号： G06F17/5031

摘要： A method for derivation and abstraction of test models for validation of industrial designs using guided simulation is described. The method employs automatic abstractions for the test model which reduce its complexity while preserving the class of errors that can be detected by a transition tour. A method for design validation comprising generating a state-based test model of the design, abstracting said test model by retiming and latch removal; and applying validation technique on the abstracted test model. First, the number of internal (non-peripheral) latches in a design is minimized via retiming using a method of Maximal Peripheral Retiming (MPR). According to the MPR method, internal latches are retimed to the periphery of the circuit. Subsequently, all latches that can be retimed to the periphery are automatically abstracted in the test model. The validation technique may comprise of model checking, invariant checking or guided simulation using test sequences generated from the abstracted test model.

摘要翻译： 描述了使用引导模拟验证工业设计的测试模型的推导和抽象方法。 该方法对测试模型采用自动抽象，这降低了其复杂性，同时保留了过渡旅程可以检测到的错误类别。 一种用于设计验证的方法，包括生成设计的基于状态的测试模型，通过重新定时和锁定移除抽象所述测试模型; 并对抽象测试模型应用验证技术。 首先，使用最大外设重定时（MPR）的方法通过重新定时来最小化设计中的内部（非外围）锁存器的数量。 根据MPR方法，将内部锁存器重新定位到电路的周围。 随后，可以在测试模型中自动提取所有可重新定位到外围的锁存器。 验证技术可以包括模型检查，不变检查或使用从抽象测试模型生成的测试序列的引导模拟。

公开(公告)号：US06745160B1

公开(公告)日：2004-06-01

申请号：US09414815

申请日：1999-10-08

申请人： Pranav Ashar ,  Anand Raghunathan ,  Subhrajit Bhattacharya ,  Aarti Gupta

发明人： Pranav Ashar ,  Anand Raghunathan ,  Subhrajit Bhattacharya ,  Aarti Gupta

IPC分类号： G06F1750

CPC分类号： G06F17/504

摘要： A method of checking correctness of scheduling of a circuit where a schedule for the circuit is obtained from a behavioral description. The method comprising extracting loop invariants to determine a sufficient set of acyclic threads when loops are present, performing symbolic simulation to extract the above loop invariants, and proving equivalence of the acyclic threads. Systems, computer systems and computer program products that incorporate the techniques of verification and correctness checking according to the present invention have also been disclosed.

摘要翻译： 一种检查电路调度的正确性的方法，其中从行为描述获得电路的调度。 该方法包括提取循环不变量以在存在循环时确定足够的非循环线程集合，执行符号仿真以提取上述循环不变量，以及证明非循环线程的等价性。 还公开了结合根据本发明的验证和正确性检查技术的系统，计算机系统和计算机程序产品。

公开(公告)号：US06728665B1

公开(公告)日：2004-04-27

申请号：US09693979

申请日：2000-10-23

申请人： Aarti Gupta ,  Zijiang Yang ,  Pranav Ashar

发明人： Aarti Gupta ,  Zijiang Yang ,  Pranav Ashar

IPC分类号： G06F710

CPC分类号： G06F17/504

摘要： A method of performing image or pre-image computation for a system is disclosed. The method comprises representing the system by a finite state model; representing state sets using Binary Decision Diagrams (BDDs); performing a satisfiabilty checking (SAT) based backtrack search algorithm, wherein, the SAT decomposes the search over an entire solution space into multiple sub-problems, and wherein a BDD-based image computation is used to solve each sub-problem by enumerating multiple solutions from the solution space. Further, a method for pruning a search space in a SAT procedure is disclosed. The method comprises using BDD Bounding against an implicit disjunction or conjunction of a given set of BDDs; continuing search if a partial assignment of variables satisfies the implicit disjunction or conjunction, and backtracking if a partial assignment of variables does not satisfy the implicit disjunction or conjunction.

摘要翻译： 公开了一种用于系统执行图像或预图像计算的方法。 该方法包括通过有限状态模型表示系统; 使用二进制决策图（BDD）表示状态集; 执行基于可靠性检查（SAT）的回溯搜索算法，其中，SAT将整个解空间的搜索分解成多个子问题，并且其中使用基于BDD的图像计算来通过枚举多个解决方案来解决每个子问题 从解决方案空间。 此外，公开了一种在SAT过程中修剪搜索空间的方法。 该方法包括使用BDD边界抵抗一组给定的BDD的隐式分离或连接; 如果变量的部分分配满足隐式分离或连接，并且如果变量的部分分配不满足隐式分离或连接，则继续搜索。

公开(公告)号：US06662323B1

公开(公告)日：2003-12-09

申请号：US09425886

申请日：1999-10-25

申请人： Pranav Ashar ,  Aarti Gupta

发明人： Pranav Ashar ,  Aarti Gupta

IPC分类号： G01R3128

CPC分类号： G01R31/31835 ,  G01R31/31707 ,  G01R31/318502

摘要： A fast error diagnosis system and process for combinational verification is described. The system and process localizes error sites in a combinational circuit implementation that has been shown to be inequivalent to its specification. In the typical case, it is not possible to identify the error location exactly. The invention uses a diagnosis strategy of gradually increasing the level of detail in the analysis algorithm to ultimately derive a small list of potential error sites in a short time. The invention combines the use of simulation, Binary Decision Diagrams, and Boolean satisfiability in a novel way to achieve the goal. The previous approaches have been limited in that they have either been constrained to a specific error model unlike the present invention, or they are inefficient in comparison to the present invention. The present invention allows for the final set of error sites derived to be small, where that set contains the actual error sites, and is derived in a reasonable amount of time.

摘要翻译： 描述了用于组合验证的快速错误诊断系统和过程。 系统和过程将组合电路实现中的错误位置定位，这已被证明与其规范不符。 在典型情况下，不可能准确地识别错误位置。 本发明采用逐步提高分析算法细节水平的诊断策略，最终在短时间内得到潜在的误差点列表。 本发明以一种新颖的方式结合了仿真，二进制决策图和布尔可满足性的使用来实现目标。 以前的方法受到限制，因为它们已经被限制到与本发明不同的特定误差模型，或者它们与本发明相比是低效的。 本发明允许导出的最终的错误站点集合很小，其中该集合包含实际的错误站点，并且在合理的时间量内导出。