利索-全球专利检索

  1. 登录
  2. 注册

搜索结果

72 条记录 (耗时 0.025 秒)

    System for combinational equivalence checking
    1.
    发明授权
    System for combinational equivalence checking 失效
    组合等价检查系统

    公开(公告)号：US6026222A

    公开(公告)日：2000-02-15

    申请号：US997551

    申请日：1997-12-23

    申请人： Aarti Gupta ,  Pranav N Ashar

    发明人： Aarti Gupta ,  Pranav N Ashar

    IPC分类号： H01L21/822 ,  G06F17/50 ,  H01L21/66 ,  H01L27/04

    CPC分类号： G06F17/504

    摘要： A computer system, computer program product, and method for solving a combinational logic verification problem with respect to two combinational circuits includes Boolean SAT checking integrated with binary decision diagrams (BDD) use. A fanout partition of a miter circuit formed from the two combinational circuits is reduced to BDD form, while the fanin partition is represented by SAT clauses. As SAT solutions are evaluated, variables in the cutset between the fanout and fanin partitions are assigned values. In a preferred embodiment, each assignment to a cutset variable is checked against an onset of the BDD prior to continuing with SAT solution seeking.

    摘要翻译： 一种计算机系统，计算机程序产品和用于解决两个组合电路组合逻辑验证问题的方法，包括与二进制决策图（BDD）使用集成的布尔SAT检查。 由两个组合电路形成的斜角电路的扇出分区减少为BDD形式，而扇形分区由SAT子句表示。 在评估SAT解决方案时，扇出分区和扇区分区之间的变量将分配值。 在优选实施例中，在继续SAT求解之前，针对BDD的开始来检查对切片变量的每个分配。

    Method for using complete-1-distinguishability for FSM equivalence checking
    2.
    发明授权
    Method for using complete-1-distinguishability for FSM equivalence checking 失效
    用于FSM等价性检查的完整1可区分性的方法

    公开(公告)号：US6035109A

    公开(公告)日：2000-03-07

    申请号：US847952

    申请日：1997-04-22

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

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

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

    CPC分类号： G06F17/504

    摘要： The Complete-1-Distinguishability (C-1-D) property is used for simplifying FSM verification. This property eliminates the need for a traversal of the product machine for the implementation machine and the specification machine. Instead, a much simpler check suffices. This check consists of first obtaining a 1-equivalence mapping between the states of the two machines, and then checking that it is a bisimulation relation. The C-1-D property can be used directly on specifications for which it naturally holds. This property can be enforced on arbitrary FSMs by exposing some of the latch outputs as pseudo-primary outputs during synthesis and verification. In this sense, the synthesis/verification methodology provides another point in the tradeoff curve between constraints-on-synthesis versus complexity-of-verification.

    摘要翻译： 完整的1分辨率（C-1-D）属性用于简化FSM验证。 该特性不需要对实施机器和规格机器的产品机器进行遍历。 相反，一个更简单的检查就足够了。 该检查包括首先在两台机器的状态之间获得1等效映射，然后检查它是否是双向关系。 C-1-D属性可以直接用于其自然拥有的规格。 通过在合成和验证期间将某些锁存输出作为伪主输出，可以在任意的FSM上强制实现该属性。 在这个意义上，综合/验证方法在合成约束与验证复杂度之间的权衡曲线中提供了另一个要点。

    System and method for monotonic partial order reduction
    5.
    发明授权
    System and method for monotonic partial order reduction 有权
    用于单调部分阶次降低的系统和方法

    公开(公告)号：US08381226B2

    公开(公告)日：2013-02-19

    申请号：US12367140

    申请日：2009-02-06

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

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

    IPC分类号： G06F11/36

    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求解器在并发程序的探索期间动态添加约束，以确保模型检查的准单调性。

    Scope Bounding with Automated Specification Inference for Scalable Software Model Checking
    6.
    发明申请
    Scope Bounding with Automated Specification Inference for Scalable Software Model Checking 有权
    可扩展软件模型检查自动规范推理范围

    公开(公告)号：US20120151449A1

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

    申请号：US13314738

    申请日：2011-12-08

    申请人： Naoto Maeda ,  Franjo Ivancic ,  Sriram Sankaranarayanan ,  Aarti Gupta

    发明人： Naoto Maeda ,  Franjo Ivancic ,  Sriram Sankaranarayanan ,  Aarti Gupta

    IPC分类号： G06F9/44

    CPC分类号： G06F8/74 ,  G06F11/3604

    摘要： A scalable, computer implemented method for finding subtle flaws in software programs. The method advantageously employs 1) scope bounding which limits the size of a generated model by excluding deeply-nested function calls, where the scope bounding vector is chosen non-monotonically, and 2) automatic specification inference which generates constraints for functions through the effect of a light-weight and scalable global analysis. Advantageously, scalable software model checking is achieved while at the same time finding more bugs.

    摘要翻译： 一种可扩展的计算机实现的方法，用于在软件程序中发现微妙的缺陷。 该方法有利地采用1）范围界限，其通过排除深嵌套的函数调用来限制所生成的模型的大小，其中范围界限向量被非单调地选择，以及2）自动规范推理，其通过效应来产生功能的约束 轻量级和可扩展的全球分析。 有利地，实现可扩展的软件模型检查，同时发现更多的错误。

    Partial order reduction using guarded independence relations
    7.
    发明授权
    Partial order reduction using guarded independence relations 有权
    使用守卫的独立关系减少部分秩序

    公开(公告)号：US08176496B2

    公开(公告)日：2012-05-08

    申请号：US12181665

    申请日：2008-07-29

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

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

    IPC分类号： G06F9/44 ,  G06F9/46 ,  G06F9/50

    CPC分类号： G06F9/44589 ,  G06F11/3608

    摘要： A system and method for conducting symbolic partial order reduction for concurrent systems includes determining a guarded independence relation which includes transitions from different threads that are independent for a set of states, when a condition or predicate holds. Partial order reduction is performed using the guarded independence relation to permit automatic pruning of redundant thread interleavings when the guarded independence condition holds.

    摘要翻译： 用于对并发系统进行符号部分顺序减少的系统和方法包括：当条件或谓词成立时，确定包括对于一组状态是独立的不同线程的转移的被保护的独立关系。 当保护的独立性条件成立时，使用保护的独立关系执行部分顺序减少以允许冗余线程交织的自动修剪。

    INTEGRATING INTERVAL CONSTRAINT PROPAGATION WITH NONLINEAR REAL ARITHMETIC
    8.
    发明申请
    INTEGRATING INTERVAL CONSTRAINT PROPAGATION WITH NONLINEAR REAL ARITHMETIC 有权
    用非线性实数算法来整合间隔约束传播

    公开(公告)号：US20110173148A1

    公开(公告)日：2011-07-14

    申请号：US12966710

    申请日：2010-12-13

    申请人： MALAY K. GANAI ,  Sicun Gao ,  Franjo Ivancic ,  Aarti Gupta

    发明人： MALAY K. GANAI ,  Sicun Gao ,  Franjo Ivancic ,  Aarti Gupta

    IPC分类号： G06N5/02

    CPC分类号： G06N5/003

    摘要： A system and method for deciding the satisfiability of a non-linear real decision problem is disclosed. Linear and non-linear constraints associated with the problem are separated. The feasibility of the linear constraints is determined using a linear solver. The feasibility of the non-linear constraints is determined using a non-linear solver which employs interval constraint propagation. The interval solutions obtained from the non-linear solver are validated using the linear solver. If the solutions cannot be validated, linear constraints are learned to refine a search space associated with the problem. The learned constraints and the non-linear constraints are iteratively solved using the non-linear solver until either a feasible solution is obtained or no solution is possible.

    摘要翻译： 公开了一种用于确定非线性真实决策问题的可满足性的系统和方法。 与问题相关联的线性和非线性约束是分开的。 使用线性求解器确定线性约束的可行性。 使用采用间隔约束传播的非线性求解器来确定非线性约束的可行性。 使用线性求解器验证从非线性求解器获得的间隔解。 如果解决方案无法验证，则学习线性约束来优化与问题相关联的搜索空间。 使用非线性求解器迭代地求解所学习的约束和非线性约束，直到获得可行解或者不可能得到解。

    Computer implemented method of high-level synthesis for the efficient verification of computer software
    9.
    发明授权
    Computer implemented method of high-level synthesis for the efficient verification of computer software 失效
    计算机实现高级综合的方法，有效验证计算机软件

    公开(公告)号：US07743352B2

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

    申请号：US11689906

    申请日：2007-03-22

    申请人： Malay Ganai ,  Aarti Gupta

    发明人： Malay Ganai ,  Aarti Gupta

    IPC分类号： G07F17/50

    CPC分类号： G06F17/504

    摘要： Verification friendly models for SAT-based formal verification are generated from a given high-level design wherein during construction the following guidelines are enforced: 1) No re-use of functional units and registers; 2) Minimize the use of muxes and sharing; 3) Reduce the number of control steps; 4) Avoid pipelines; 5) Chose functional units from “verification friendly” library; 6) Re-use operations; 7) Perform property-preserving slicing; 8) Support “assume” and “assert” in the language specification; and 8) Use external memory modules instead of register arrays.

    摘要翻译： 从给定的高级设计生成基于SAT的形式验证的验证友好模型，其中在施工期间执行以下准则：1）不重复使用功能单元和寄存器; 2）最小化使用复用和共享; 3）减少控制步骤的数量; 4）避免管道; 5）从“验证友好”库中选择功能单位; 6）重用操作; 7）进行维护保养切片; 8）在语言规范中支持“假设”和“断言”; 和8）使用外部存储器模块而不是寄存器阵列。

    Property specific testbench generation framework for circuit design validation by guided simulation
    10.
    发明授权
    Property specific testbench generation framework for circuit design validation by guided simulation 失效
    通过引导模拟进行电路设计验证的属性特定测试平台生成框架

    公开(公告)号：US06975976B1

    公开(公告)日：2005-12-13

    申请号：US09693976

    申请日：2000-10-23

    申请人： Albert E. Casavant ,  Aarti Gupta ,  Pranav Ashar

    发明人： Albert E. Casavant ,  Aarti Gupta ,  Pranav Ashar

    IPC分类号： G01R31/28 ,  G01R31/3183 ,  G06F17/50

    CPC分类号： G01R31/318314 ,  G01R31/318357 ,  G01R31/318364 ,  G06F17/5022

    摘要： Simulation continues to be the primary technique for functional validation of designs. It is important that simulation vectors be effective in targeting the types of bugs designers expect to find rather than some generic coverage metrics. The focus of this work is to generate property-specific testbenches that are targeted either at proving the correctness of a property or at finding a bug. It is based on performing property-specific analysis on iteratively less abstract models of the design in order to obtain interesting paths in the form of a Witness Graph, which is then targeted during simulation of the entire design. This testbench generation framework will form an integral part of a comprehensive verification system currently being developed.

    摘要翻译： 仿真仍然是设计功能验证的主要技术。 重要的是，模拟向量有效地针对设计人员期望找到的错误类型，而不是某些通用覆盖度量。 这项工作的重点是生成属性特定的测试台，其目标是证明属性的正确性或发现错误。 它基于对迭代较少的抽象设计模型进行属性特定分析，以便以仿真图形式获得有趣的路径，然后在模拟整个设计过程中进行目标。 该测试平台生成框架将构成当前正在开发的综合验证系统的组成部分。