-
31.发明授权Method and system for enhanced verification by closely coupling a structural overapproximation algorithm and a structural satisfiability solver 有权通过紧密耦合结构过近似算法和结构可满足性求解器来增强验证的方法和系统公开(公告)号：US07356792B2
公开(公告)日：2008-04-08
申请号：US11340477
申请日：2006-01-26
IPC分类号： G06F17/50
CPC分类号： G06F17/504
摘要： A method, system and computer program product for performing verification are disclosed. A first abstraction of an initial design netlist containing a first target is created and designated as a current abstraction, and the current abstraction is unfolded by a selectable depth. A composite target is verified using a satisfiability solver, and in response to determining that the verifying step has hit the composite target, a counterexample to is examined to identify one or more reasons for the first target to be asserted. One or more refinement pairs are built by examining the counterexample, and a second abstraction is built by composing the refinement pairs. One or more learned clauses and one or more invariants to the second abstraction and the second abstraction is chosen as the current abstraction. The current abstraction is verified with the satisfiability solver.
摘要翻译： 公开了一种用于执行验证的方法，系统和计算机程序产品。 创建包含第一个目标的初始设计网表的第一个抽象，并将其指定为当前抽象，并且当前抽象由可选深度展开。 使用可满足性求解器验证复合目标，并且响应于确定验证步骤已经击中复合目标，检查反例以识别要被断言的第一目标的一个或多个原因。 通过检查反例来构建一个或多个细化对，并通过组合细化对构建第二个抽象。 选择一个或多个学习子句和一个或多个第二抽象和第二抽象的不变量作为当前抽象。 目前的抽象是用可满足性求解器来验证的。
-
公开(公告)号：US08201115B2
公开(公告)日：2012-06-12
申请号：US12191635
申请日：2008-08-14
CPC分类号： G06F17/505
摘要： A method, system, and computer program product for reducing the size of a logic network design, prior to verification of the logic network design. The method includes eliminating registers to reduce the size of the logic network design; thereby, increasing the speed and functionality of the verification process, and decreasing the size of the logic network design. The system identifies one or more compatible resubstitutions of a selected register, wherein the compatible resubstitution expresses the selected register as one or more pre-existing registers of fixed initial state. The resubstitutions are refined utilizing design invariants. When one more resubstitutions are preformed, the system eliminates the selected registers to reduce the size of the logic network design. As a result of the resubstitution process, a logic network design of reduced size is generated.
摘要翻译： 在验证逻辑网络设计之前，用于减小逻辑网络设计大小的方法，系统和计算机程序产品。 该方法包括消除寄存器以减小逻辑网络设计的大小; 从而增加验证过程的速度和功能，并减小逻辑网络设计的大小。 系统识别所选择的寄存器的一个或多个兼容的重新配置，其中兼容重新配置将所选择的寄存器表示为一个或多个预先存在的固定初始状态的寄存器。 利用设计不变量来改进重组。 当再进行一次重新配置时，系统将删除所选择的寄存器以减小逻辑网络设计的大小。 作为重新配置处理的结果，生成尺寸减小的逻辑网络设计。
-
公开(公告)号：US08037085B2
公开(公告)日：2011-10-11
申请号：US12129976
申请日：2008-05-30
CPC分类号： G06F17/504
摘要： A method for performing verification includes selecting a first set containing a seed register and adding to a second set a result of a subtraction of a fanout of the first set from a fanin of the first set. A third set is rendered equal to a result of a subtraction of a fanin of the second set from a fanout of the second set, and whether a combination of the first set and the third set is equivalent to the first set is determined. In response to determining that the combination of the first set and the second set is not equivalent to the first set, a min-cut of the first set and the second set containing a minimal set of predicates between a first component and the logic to which the component fans out, wherein the logic is bordered by the second set is returned.
摘要翻译： 一种用于执行验证的方法包括：选择包含种子寄存器的第一集合，并且从第一组的扇区中减去第一组的扇出结果，向第二组添加结果。 第三组被赋予等于从第二组的扇出中减去第二组的扇形的结果，以及第一组和第三组的组合是否等同于第一组的结果。 响应于确定第一集合和第二集合的组合不等同于第一集合，第一集合和第二集合的最小化包含第一组件和逻辑之间的最小一组谓词 组件风扇出来，其中返回逻辑与第二组相邻的逻辑。
-
公开(公告)号：US07996803B2
公开(公告)日：2011-08-09
申请号：US12362513
申请日：2009-01-30
IPC分类号： G06F17/50
CPC分类号： G06F17/504
摘要： A method, system and computer program product for automated use of uninterpreted functions in sequential equivalence checking. A first netlist and a second netlist may be received and be included in an original model, and from the original model, logic to be abstracted may be determined. A condition for functional consistency may be determined, and an abstract model may be created by replacing the logic with abstracted logic using one or more uninterpreted functions. One or more functions may be performed on the abstract model. For example, the one or more functions may include one or more of a bounded model checking (BMC) algorithm, an interpolation algorithm, a Boolean satisfiability-based analysis algorithm, and a binary decision diagram (BDD) based reachability analysis algorithm, among others.
摘要翻译： 一种在顺序等效性检查中自动使用未解释函数的方法，系统和计算机程序产品。 可以接收第一网表和第二网表并将其包括在原始模型中，并且可以从原始模型中确定要抽象的逻辑。 可以确定功能一致性的条件，并且可以通过使用一个或多个未解释函数替换具有抽象逻辑的逻辑来创建抽象模型。 抽象模型可以执行一个或多个功能。 例如，一个或多个功能可以包括有界模型检查（BMC）算法，插值算法，基于布尔可满足性的分析算法和基于二进制决策图（BDD）的可达性分析算法等中的一个或多个 。
-
35.发明授权Enhanced verification by closely coupling a structural overapproximation algorithm and a structural satisfiability solver 有权通过紧密耦合结构过近似算法和结构可满足性求解器来增强验证公开(公告)号：US07917884B2
公开(公告)日：2011-03-29
申请号：US12013191
申请日：2008-01-11
IPC分类号： G06F17/50
CPC分类号： G06F17/504
摘要： A method, system and computer program product for performing verification are disclosed. A first abstraction of an initial design netlist containing a first target is created and designated as a current abstraction, and the current abstraction is unfolded by a selectable depth. A composite target is verified using a satisfiability solver, and in response to determining that the verifying step has hit the composite target, a counterexample to is examined to identify one or more reasons for the first target to be asserted. One or more refinement pairs are built by examining the counterexample, and a second abstraction is built by composing the refinement pairs. One or more learned clauses and one or more invariants to the second abstraction and the second abstraction is chosen as the current abstraction. The current abstraction is verified with the satisfiability solver.
摘要翻译： 公开了一种用于执行验证的方法，系统和计算机程序产品。 创建包含第一个目标的初始设计网表的第一个抽象，并将其指定为当前抽象，并且当前抽象由可选深度展开。 使用可满足性求解器验证复合目标，并且响应于确定验证步骤已经击中复合目标，检查反例以识别要被断言的第一目标的一个或多个原因。 通过检查反例来构建一个或多个细化对，并通过组合细化对构建第二个抽象。 选择一个或多个学习子句和一个或多个第二抽象和第二抽象的不变量作为当前抽象。 目前的抽象是用可满足性求解器来验证的。
-
公开(公告)号：US07793242B2
公开(公告)日：2010-09-07
申请号：US11940711
申请日：2007-11-15
IPC分类号： G06F17/50
CPC分类号： G06F17/504
摘要： A method for performing verification is disclosed. The method includes selecting a first computer-design constraint for simplification and applying structural reparamaterization to simplify the first computer-design constraint. In response to determining that the first computer-design constraint is not eliminated, the first computer-design constraint is set equal to a dead-end state of the constraint. A structural preimage of the first computer-design constraint is created, in response to determining that a combination of a target and the dead-end state of the first computer-design constraint is equal to a combination of the target and the structural preimage of the first computer-design constraint, the first computer-design constraint is set equal to the structural preimage.
摘要翻译： 公开了一种用于执行验证的方法。 该方法包括选择第一计算机设计约束以简化并应用结构化重新定位以简化第一计算机设计约束。 响应于确定第一计算机设计约束不被消除，第一计算机设计约束被设置为等于约束的死端状态。 响应于确定第一计算机设计约束的目标和死端状态的组合等于目标和第一计算机设计约束的结构前图像的组合，创建第一计算机设计约束的结构预图像 第一个计算机设计约束，第一个计算机设计约束被设置为等于结构前像。
-
37.发明申请Method and System for Enhanced Verification By Closely Coupling a Structural Satisfiability Solver and Rewriting Algorithms 失效通过紧密耦合结构可靠性求解器和重写算法来增强验证的方法和系统公开(公告)号：US20090094563A1
公开(公告)日：2009-04-09
申请号：US12332191
申请日：2008-12-10
IPC分类号： G06F17/50
CPC分类号： A61F13/472 , A61F13/202 , A61F13/2051 , A61F13/206 , A61F13/2065 , A61F13/2068 , G06F8/72
摘要： A method, system and computer program product are disclosed. The method includes initializing a first variable to limit a rewrite time for rewrite operations with respect to an initial design by a rewriting module, a second variable to limit a time for satisfiability solver operations with respect to said initial design by a satisfiability solver module and a third variable to limit a maximum number of rewrite iterations with respect to said initial design. A timer is called to track said rewrite time and a local logic rewriting operation is run on said initial design with said rewrite module. In response to determining that all of all targets for said initial design netlist are not solved, whether a rewrite time is expired is determined. In response to determining that said rewrite time is not expired, AND refactoring is run. In response to determining that said rewrite time is not expired, XOR refactoring is run.
摘要翻译： 公开了一种方法，系统和计算机程序产品。 该方法包括：初始化第一变量以限制由重写模块相对于初始设计的重写操作的重写时间;第二变量，用于通过可满足性求解器模块限制相对于所述初始设计的可满足性求解器操作的时间;以及 第三变量以限制相对于所述初始设计的最大重写迭代次数。 调用定时器以跟踪所述重写时间，并且利用所述重写模块在所述初始设计上运行本地逻辑重写操作。 响应于确定所有初始设计网表的所有目标未被解决，确定重写时间是否到期。 响应于确定所述重写时间未过期，并且运行重构。 响应于确定所述重写时间未过期，运行XOR重构。
-
38.发明申请METHOD AND SYSTEM FOR PERFORMING MINIMIZATION OF INPUT COUNT DURING STRUCTURAL NETLIST OVERAPPROXIMATION 失效用于在结构化网络列表过载预测期间执行最小化输入计数的方法和系统公开(公告)号：US20080307372A1
公开(公告)日：2008-12-11
申请号：US12047361
申请日：2008-03-13
IPC分类号： G06F17/50
CPC分类号： G06F17/504
摘要： A method for performing verification is disclosed. The method includes selecting a set of gates to add to a first localization netlist and forming a refinement netlist. A min-cut is computed with sinks having one or more gates in the refinement netlist and sources comprising one or more inputs of an original netlist and one or more registers registers of the original netlist which are not part of the refinement netlist. A final localized netlist is obtained by adding one or more gates to the refinement netlist to grow the refinement netlist until reaching one or more cut-gates of the min-cut.
摘要翻译： 公开了一种用于执行验证的方法。 该方法包括选择一组门以添加到第一定位网表并形成细化网表。 使用在细化网表中具有一个或多个门的信宿和包括原始网表的一个或多个输入和不属于细化网表的原始网表的一个或多个寄存器寄存器的源来计算最小值。 通过将一个或多个门添加到细化网表来获得最终的本地化网表，以增加细化网表，直到达到最小切割的一个或多个切割点。
-
39.发明授权Method and system for performing utilization of traces for incremental refinement in coupling a structural overapproximation algorithm and a satisfiability solver 有权用于在结合过度近似算法和可满足性求解器的耦合中执行增量细化的跟踪的方法和系统公开(公告)号：US07448005B2
公开(公告)日：2008-11-04
申请号：US11340534
申请日：2006-01-26
IPC分类号： G06F17/50
CPC分类号： G06F17/504
摘要： A method, system and computer program product for performing verification are disclosed. The method includes creating and designating as a current abstraction a first abstraction of an initial design netlist containing a first target and unfolding the current abstraction by a selectable depth. A composite target is verified, using a satisfiability solver and, in response to determining that the verifying step has hit the composite target, a counterexample is examined to identify one or more reasons for the first target to be asserted. One or more refinement pairs are built by examining the counterexample and a second abstraction is built by composing the refinement pairs. A new target is built over one or more cutpoints in the first abstraction that is asserted when the one or more cutpoints assume values in the counterexample, and the new target is verified with the satisfiability solver.
摘要翻译： 公开了一种用于执行验证的方法，系统和计算机程序产品。 该方法包括创建和指定作为当前抽象的包含第一目标的初始设计网表的第一抽象并且通过可选深度展开当前抽象。 使用可满足性求解器来验证复合目标，并且响应于确定验证步骤已经达到复合目标，检查反例以识别要被断言的第一目标的一个或多个原因。 通过检查反例来构建一个或多个细化对，通过组合细化对构建第二个抽象。 当一个或多个切点在反例中假定值时，第一个抽象中的一个或多个切点建立一个新目标，并且使用可满足性求解器验证新目标。
-
40.发明申请公开(公告)号：US20080235637A1
公开(公告)日：2008-09-25
申请号：US12047189
申请日：2008-06-09
申请人： JASON R. BAUMGARTNER , Geert Janssen , Hari Mony , Viresh Paruthi
发明人： JASON R. BAUMGARTNER , Geert Janssen , Hari Mony , Viresh Paruthi
IPC分类号： G06F17/50
CPC分类号： G06F17/5045
摘要： A method, system, and computer program product for preserving critical inputs. According to an embodiments of the present invention, an initial design including one or more primary inputs which cannot be eliminated, one or more primary inputs which can be eliminated, one or more targets, and one or more state elements are received. A cut of said initial design including one or more cut gates is identified, and a relation of one or more values producible to said one or more cut gates in terms of said one or more primary inputs which cannot be eliminated, said one or more primary inputs which can be eliminated and said one or more state elements is computed. Said relation is synthesized to form a gate set, and an abstracted design is formed from said gate set. Verification is performed on said abstracted design to generate verification results.
摘要翻译： 一种用于保存关键输入的方法，系统和计算机程序产品。 根据本发明的实施例，接收包括不能被消除的一个或多个主要输入，可以被消除的一个或多个主要输入，一个或多个目标以及一个或多个状态元素的初始设计。 识别包括一个或多个切割门的所述初始设计的切割，以及根据所述一个或多个主要输入而不能被消除的一个或多个可生产到所述一个或多个切割门的值的关系，所述一个或多个主要 可以消除的输入和所述一个或多个状态元素被计算。 所述关系被合成以形成栅极集合，并且从所述栅极集合形成抽象设计。 对所述抽象设计进行验证以产生验证结果。
-
-
-
-
-
-
-
-
-
搜索结果
175 条记录 (耗时 0.033 秒)
