公开(公告)号：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.

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

公开(公告)号：US08359578B2

公开(公告)日：2013-01-22

申请号：US12571476

申请日：2009-10-01

申请人： Chao Wang ,  Aarti Gupta ,  Swarat Chaudhuri ,  Yu Yang

发明人： Chao Wang ,  Aarti Gupta ,  Swarat Chaudhuri ,  Yu Yang

IPC分类号： G06F9/44

CPC分类号： G06F11/3612 ,  G06F11/3624 ,  G06F11/3636

摘要： A computer implemented method for the verification of concurrent software programs wherein the concurrent software program is partitioned into subsets named concurrent trace programs (CTPs) and each of the CTPs is evaluated using a satisfiability-based (SAT) symbolic analysis. By applying the SAT analysis to individual CTPs in isolation the symbolic analysis is advantageously more scalable and efficient.

摘要翻译： 一种用于验证并发软件程序的计算机实现方法，其中并发软件程序被划分为称为并发跟踪程序（CTP）的子集，并且使用基于可满足性（SAT）符号分析来评估每个CTP。 通过将SAT分析应用于独立的CTP，符号分析有利地更具可扩展性和高效性。

公开(公告)号：US08200474B2

公开(公告)日：2012-06-12

申请号：US12397696

申请日：2009-03-04

申请人： Chao Wang ,  Aarti Gupta

发明人： Chao Wang ,  Aarti Gupta

IPC分类号： G06F9/45

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.

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

公开(公告)号：US08005661B2

公开(公告)日：2011-08-23

申请号：US12116668

申请日：2008-05-07

申请人： Malay Ganai ,  Aarti Gupta

发明人： Malay Ganai ,  Aarti Gupta

IPC分类号： G06F9/45 ,  G06F9/455 ,  G06F7/60 ,  G06F12/00 ,  G06F13/00

CPC分类号： G06F11/3608 ,  G06F17/504

摘要： A computer implemented method for modeling and verifying concurrent systems which uses Satisfiability-Modulo Theory (SMT)-based Bounded Model Checking (BMC) to detect violations of safety properties such as data races. A particularly distinguishing aspect of our inventive method is that we do not introduce wait-cycles in our symbolic models for the individual threads, which are typically required for considering an interleaved execution of the threads. These wait-cycles are detrimental to the performance of BMC. Instead, we first create independent models for the different threads, and add inter-model constraints lazily, incrementally, and on-the-fly during BMC unrolling to capture the sequential consistency and synchronization semantics. We show that our constraints provide a sound and complete modeling with respect to the considered semantics. One benefit of our lazy modeling method is the reduction in the size of the BMC problem instances, thereby, improving the verification performance in both runtime and memory.

摘要翻译： 一种用于建模和验证并发系统的计算机实现方法，其使用基于可信性 - 模理论（SMT）的有界模型检查（BMC）来检测诸如数据竞赛之类的安全属性的违规。 我们的创造性方法的特别区别在于，我们不在针对各个线程的符号模型中引入等待周期，这通常是考虑线程的交错执行所需要的。 这些等待周期对BMC的性能是不利的。 相反，我们首先为不同的线程创建独立的模型，并在BMC展开期间懒洋洋地，逐步地和即时地添加模型间约束，以捕获顺序一致性和同步语义。 我们显示我们的约束提供了一个关于所考虑的语义的完整的建模。 我们的懒惰建模方法的一个好处是减少了BMC问题实例的大小，从而提高了运行时和内存中的验证性能。

公开(公告)号：US07926039B2

公开(公告)日：2011-04-12

申请号：US11692421

申请日：2007-03-28

申请人： Chao Wang ,  Zijiang Yang ,  Aarti Gupta

发明人： Chao Wang ,  Zijiang Yang ,  Aarti Gupta

IPC分类号： G06F9/44 ,  G06F9/45

CPC分类号： G06F9/44589

摘要： An improved method for automatically improving the precision of an extrapolation operator used, for example, in software program verification in connection with the static analysis and model checking of the software programs which rely on fix-point computation. In particular, a new extrapolation-with-care-set operator, together with a method for gradually increasing the precision of this operation by tightening the care set.

摘要翻译： 一种改进的方法，用于自动提高外推算子的精度，例如，在依赖于固定点计算的软件程序的静态分析和模型检查的软件程序验证中。 特别地，一种新的外推护理操作器，以及通过收紧护理套件逐渐增加该操作的精度的方法。

公开(公告)号：US07742907B2

公开(公告)日：2010-06-22

申请号：US10762499

申请日：2004-01-23

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

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

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

CPC分类号： G06F17/504

摘要： A method of obtaining a resolution-based proof of unsatisfiability using a SAT procedure for a hybrid Boolean constraint problem comprising representing constraints as a combination of clauses and interconnected gates. The proof is obtained as a combination of clauses, circuit gates and gate connectivity constraints sufficient for unsatisfiability.

摘要翻译： 使用针对混合布尔约束问题的SAT过程获得基于分辨率的不满足证明的方法，包括将约束表示为子句和互连门的组合。 证明是作为条件，电路门和门连接约束的组合获得的，足以满足不满足性。