专利快速检索-快速检索全球专利，免费商用专利数据库-IPRDB

1. 发明授权

US08015523B2 Method and system for sequential netlist reduction through trace-containment 有权
标题翻译：通过跟踪容纳进行顺序网表缩减的方法和系统
公开(公告)号：US08015523B2
公开(公告)日：2011-09-06
申请号：US12392278
申请日：2009-02-25
申请人： Jason R. Baumgartner , Robert L. Kanzelman , Hari Mony , Viresh Paruthi
发明人： Jason R. Baumgartner , Robert L. Kanzelman , Hari Mony , Viresh Paruthi
IPC分类号： G06F17/50 , G06F9/455
CPC分类号： G06F17/505 , G06F17/504
摘要： Methods and systems are provided for sequential netlist reduction through trace-containment for a circuitry design netlist by first identifying a cut of the netlist and enumerating a set of mismatch traces. Perform time-bounded unfolding of a cofactored version of the cut to reflect the sequential cofactor for a specific input i and temporal uncorrelation constraints for the set of inputs ‘J’. Determine whether there is trace containment by performing equivalence checking with respect to the cut of the netlist under temporal uncorrelation constraints for the set of inputs ‘J’. In response to detecting trace containment, simplify the netlist by merging the input ‘i’ to a constant.
摘要翻译：提供方法和系统，用于通过电路设计网表的跟踪容纳来顺序的网表减少，首先识别网表的剪切并列举一组不匹配的跟踪。执行切片的辅助版本的时间限制展开，以反映特定输入i的顺序辅因子和输入集合J'的时间非相关约束。通过对输入集合J'的时间不相关约束执行相对于网表的切分的等价性检查来确定是否存在跟踪容纳。响应检测跟踪容纳，通过将输入'i'合并为常数来简化网表。

2. 发明申请

US20100269077A1 Trace Containment Detection of Combinational Designs via Constraint-Based Uncorrelated Equivalence Checking 有权
标题翻译：通过基于约束的不相关等价检查的组合设计的跟踪遏制检测
公开(公告)号：US20100269077A1
公开(公告)日：2010-10-21
申请号：US12425095
申请日：2009-04-16
申请人： Jason R. Baumgartner , Robert L. Kanzelman , Hari Mony , Viresh Paruthi
发明人： Jason R. Baumgartner , Robert L. Kanzelman , Hari Mony , Viresh Paruthi
IPC分类号： G06F9/45
CPC分类号： G06F17/504
摘要： Methods and systems are provided for producing more efficient digital circuitry designs by identifying trace-containment for a sequential circuitry design netlist through the use of constraint-based uncorrelated equivalence checking. A set of candidate input netlist sets n1 and n2 is first uncorrelated and then submitted for equivalence checking. Mismatches discovered during the equivalence checking are avoided by imposing constraint to the input set until discovering an equivalency relationship between the input sets n1 and n2.
摘要翻译：提供了方法和系统，用于通过使用基于约束的不相关等价检查来识别顺序电路设计网表的跟踪容纳来产生更有效的数字电路设计。一组候选输入网表集n1和n2首先不相关，然后提交用于等价检查。在等效检查期间发现的不匹配通过对输入集施加约束来避免，直到发现输入集n1和n2之间的等价关系。

3. 发明授权

US07552407B2 Method and system for performing target enlargement in the presence of constraints 失效
标题翻译：在存在约束的情况下执行目标放大的方法和系统
公开(公告)号：US07552407B2
公开(公告)日：2009-06-23
申请号：US12036093
申请日：2008-02-22
申请人： Jason R. Baumgartner , Robert L. Kanzelman , Hari Mony , Viresh Paruthi
发明人： Jason R. Baumgartner , Robert L. Kanzelman , Hari Mony , Viresh Paruthi
IPC分类号： G06F17/50 , G06F9/45 , G06F7/60
CPC分类号： G06F17/504
摘要： A method for performing verification is disclosed. The method includes receiving a design, including one or one or more targets, one or more constraints, one or more registers and one or more inputs. A first function of one of the one or more targets over the one or more registers and the one or more inputs is computed. A second function of one or more of the one or more constraints over the one or more registers and the one or more inputs is computed. The inputs of the first function and the second function are existentially quantified. A bounded analysis is performed to determine if the one of the one or more targets may be hit while adhering to the constraints. A preimage of the inputs of the first function and a preimage of the inputs of the second function is existentially quantified to create a synthesizable preimage. The synthesizable preimage is simplified and synthesized to create an enlarged target. Verification of the enlarged target is performed.
摘要翻译：公开了一种用于执行验证的方法。该方法包括接收包括一个或多个目标，一个或多个约束，一个或多个寄存器和一个或多个输入的设计。计算一个或多个寄存器中的一个或多个目标之一和一个或多个输入的第一函数。计算一个或多个寄存器和一个或多个输入中的一个或多个约束中的一个或多个的第二函数。第一功能和第二功能的输入被存在量化。执行有界分析以确定一个或多个目标中的一个是否可以在遵守约束的情况下被击中。存在量化第一函数的输入和第二函数的输入的前像的前像，以创建可合成的前像。可合成的前像被简化和合成，以创建一个扩大的目标。执行放大目标的验证。

4. 发明申请

US20080195992A1 System and Method for Generating Constraint Preserving Testcases in the Presence of Dead-End Constraints 有权
标题翻译：在死端约束存在下生成约束保存测试箱的系统和方法
公开(公告)号：US20080195992A1
公开(公告)日：2008-08-14
申请号：US11673298
申请日：2007-02-09
申请人： Jason R. Baumgartner , Robert L. Kanzelman , Hari Mony , Viresh Paruthi
发明人： Jason R. Baumgartner , Robert L. Kanzelman , Hari Mony , Viresh Paruthi
IPC分类号： G06F17/50
CPC分类号： G06F17/5022
摘要： A system and method for generating constraint preserving testcases in the presence of dead-end constraints are provided. A balance between precision and computational expense in generating the testcases is achieved by establishing a sliding window of constraint solving for a selected number of K time-steps in the future from a current time-step. The testcases solve for the constraints for the next K time-steps at every state of a netlist instead of just trying to solve the constraint for the present time-step. K is determined by determining, for each input, either a minimum length path depth or maximum length depth path from the input to the constraint. The largest depth value for the inputs to the netlist is then utilized as the depth for the netlist. This depth then is used to define the width of the sliding window of constraint solving.
摘要翻译：提供了一种用于在存在死区约束的情况下生成约束保留测试用例的系统和方法。在生成测试用例时，精度和计算费用之间的平衡是通过从当前时间步骤中为将来选定数量的K个时间步骤建立一个约束求解滑动窗口来实现的。测试用例解决了网表的每个状态下的下一个K时间步长的约束，而不是仅仅尝试解决当前时间步长的约束。通过为每个输入确定从输入到约束的最小长度路径深度或最大长度深度路径来确定K。网表的输入的最大深度值随后被用作网表的深度。此深度用于定义约束求解的滑动窗口的宽度。

5. 发明授权

US07398488B2 Trace equivalence identification through structural isomorphism detection with on the fly logic writing 有权
标题翻译：通过结构同构检测跟踪逻辑写作的跟踪等价识别
公开(公告)号：US07398488B2
公开(公告)日：2008-07-08
申请号：US11383770
申请日：2006-05-17
申请人： Jason R. Baumgartner , Robert L. Kanzelman , Hari Mony , Viresh Paruthi
发明人： Jason R. Baumgartner , Robert L. Kanzelman , Hari Mony , Viresh Paruthi
IPC分类号： G06F17/50
CPC分类号： G06F17/504
摘要： A method for performing trace equivalent identification by structural isomorphism detection, the method comprising: synthesizing a first netlist into a second netlist, the second netlist including two-input AND gates, inversions, inputs, constants, and registers; constructing a third netlist, the third netlist being a pseudo-canonical netlist that uses calls to algorithms for constructing a netlist for gate g1 and for constructing a netlist for gate g2, where g1 and g2 are gates; and performing an isomorphism check of gates g1 and g2.
摘要翻译：一种用于通过结构同构检测来执行跟踪等价识别的方法，所述方法包括：将第一网表合成到第二网表中，所述第二网表包括双输入与门，反转，输入，常数和寄存器; 构造第三网表，第三网表是伪规范网表，其使用对算法的调用来构造门g 1的网表，并且用于构造门g 2的网表，其中g 1和g 2是门; 并执行门g 1和g 2的同构检查。

6. 发明申请

US20080134113A1 Method and System for Enhanced Verification by Closely Coupling a Structural Overapproximation Algorithm and a Structural Satisfiability Solver 失效
标题翻译：通过紧密耦合结构过近似算法和结构满意度求解器来增强验证的方法和系统
公开(公告)号：US20080134113A1
公开(公告)日：2008-06-05
申请号：US12013163
申请日：2008-01-11
申请人： Jason R. Baumgartner , Robert L. Kanzelman , Hari Mony , Viresh Paruthi
发明人： Jason R. Baumgartner , Robert L. Kanzelman , Hari Mony , Viresh Paruthi
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.
摘要翻译：公开了一种用于执行验证的方法，系统和计算机程序产品。创建包含第一个目标的初始设计网表的第一个抽象，并将其指定为当前抽象，并且当前抽象由可选深度展开。使用可满足性求解器验证复合目标，并且响应于确定验证步骤已经击中复合目标，检查反例以识别要被断言的第一目标的一个或多个原因。通过检查反例来构建一个或多个细化对，并通过组合细化对构建第二个抽象。选择一个或多个学习子句和一个或多个第二抽象和第二抽象的不变量作为当前抽象。目前的抽象是用可满足性求解器来验证的。

7. 发明授权

US08185852B2 Performing minimization of input count during structural netlist overapproximation 失效
标题翻译：在结构化网表过度近似期间执行输入计数的最小化
公开(公告)号：US08185852B2
公开(公告)日：2012-05-22
申请号：US12047361
申请日：2008-03-13
申请人： Jason R. Baumgartner , Robert L. Kanzelman , Hari Mony , Viresh Paruthi
发明人： Jason R. Baumgartner , Robert L. Kanzelman , Hari Mony , Viresh Paruthi
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.
摘要翻译：公开了一种用于执行验证的方法。该方法包括选择一组门以添加到第一定位网表并形成细化网表。使用在细化网表中具有一个或多个门的信宿和包括原始网表的一个或多个输入和不属于细化网表的原始网表的一个或多个寄存器寄存器的源来计算最小值。通过将一个或多个门添加到细化网表来获得最终的本地化网表，以增加细化网表，直到达到最小切割的一个或多个切割点。

8. 发明授权

US08042075B2 Method, system and application for sequential cofactor-based analysis of netlists 有权
标题翻译：网表的顺序辅因子分析的方法，系统和应用
公开(公告)号：US08042075B2
公开(公告)日：2011-10-18
申请号：US12410962
申请日：2009-03-25
申请人： Jason R. Baumgartner , Robert L. Kanzelman , Hari Mony , Viresh Paruthi
发明人： Jason R. Baumgartner , Robert L. Kanzelman , Hari Mony , Viresh Paruthi
IPC分类号： G06F9/45 , G06F9/455 , G06F17/50
CPC分类号： G06F17/5022
摘要： Methods, systems and computer products are provided for reducing the design size of an integrated circuit while preserving the behavior of the design with respect to verification results. A multiplexer is inserted at the gate being analyzed, and the multiplexer selector is controlled to provide a predetermined output for one frame at the point being analyzed. It is then determined whether the circuit remains equivalent during application of the predetermined output in order to decide whether the gate being analyzed is a candidate for replacement.
摘要翻译：提供了方法，系统和计算机产品，用于减少集成电路的设计尺寸，同时保持设计相对于验证结果的行为。在被分析的门处插入复用器，并且多路复用器选择器被控制以在被分析的点处为一帧提供预定的输出。然后在应用预定输出期间确定电路是否保持等效，以便确定被分析的门是否是替换候选。

9. 发明授权

US07788616B2 Method and system for performing heuristic constraint simplification 失效
公开(公告)号：US07788616B2
公开(公告)日：2010-08-31
申请号：US11940755
申请日：2007-11-15
申请人： Jason R. Baumgartner , Robert L. Kanzelman , Hari Mony , Viresh Paruthi
发明人： Jason R. Baumgartner , Robert L. Kanzelman , Hari Mony , Viresh Paruthi
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.

10. 发明授权

US07478344B2 Method and system for enhanced verification by closely coupling a structural satisfiability solver and rewriting algorithms 失效
标题翻译：通过紧密耦合结构可满足性求解器和重写算法来增强验证的方法和系统
公开(公告)号：US07478344B2
公开(公告)日：2009-01-13
申请号：US11443906
申请日：2006-05-31
申请人： Jason R. Baumgartner , Robert L. Kanzelman , Hari Mony , Viresh Paruthi
发明人： Jason R. Baumgartner , Robert L. Kanzelman , Hari Mony , Viresh Paruthi
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 satsifability solver operations with respect to said initial design by a staisfiability 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重构。

你已经成功收藏专利！

检索式保存成功!

IPRDB

热门服务

关于我们

友情链接

联系方式