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

11. 发明申请

US20090138837A1 System and Method for Sequential Equivalence Checking for Asynchronous Verification 有权
标题翻译：用于异步验证的顺序等价检查的系统和方法
公开(公告)号：US20090138837A1
公开(公告)日：2009-05-28
申请号：US11945465
申请日：2007-11-27
申请人： Jason R. Baumgartner , Yee Ja , Hari Mony , Viresh Paruthi , Barinjato Ramanandray
发明人： Jason R. Baumgartner , Yee Ja , Hari Mony , Viresh Paruthi , Barinjato Ramanandray
IPC分类号： G06F17/50
CPC分类号： G06F17/504
摘要： A system and method for performing sequential equivalence checking for asynchronous verification are provided. A first model of the integrated circuit design is provided that has additional logic in it to reflect the possible variance in behavior of the asynchronous crossings. A second model of the integrated circuit design is provided that does not have this asynchronous behavior logic but instead correlates to the simplest synchronous model that is usually used for non-asynchronous functional verification tasks. Sequential equivalence checking is performed to verify that the two models are input/output equivalent. In order to address non-uniform arrival times of bus strands, logic is provided for identifying bus strands that have transitioning bits, determining a representative delay for these strands, comparing the representative delays for all of the bus strands to determine the maximum delay for the entire bus, and applying this maximum delay to one of the models.
摘要翻译：提供了用于执行用于异步验证的顺序等同性检查的系统和方法。提供了集成电路设计的第一个模型，其具有额外的逻辑，以反映异步交叉的行为的可能方差。提供了集成电路设计的第二个模型，其不具有该异步行为逻辑，而是与通常用于非异步功能验证任务的最简单的同步模型相关联。执行顺序等价检查以验证两个模型是输入/输出等效的。为了解决总线链路的不均匀到达时间，提供了用于识别具有转换位的总线串的逻辑，确定这些线的代表性延迟，比较所有总线线的代表性延迟，以确定整个总线，并将这个最大延迟应用于其中一个模型。

12. 发明授权

US07373624B2 Method and system for performing target enlargement in the presence of constraints 有权
标题翻译：在存在约束的情况下执行目标放大的方法和系统
公开(公告)号：US07373624B2
公开(公告)日：2008-05-13
申请号：US11225672
申请日：2005-09-13
申请人： 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.
摘要翻译：公开了一种用于执行验证的方法。该方法包括接收包括一个或多个目标，一个或多个约束，一个或多个寄存器和一个或多个输入的设计。计算一个或多个寄存器中的一个或多个目标之一和一个或多个输入的第一函数。计算一个或多个寄存器和一个或多个输入中的一个或多个约束中的一个或多个的第二函数。第一功能和第二功能的输入被存在量化。执行有界分析以确定一个或多个目标中的一个是否可以在遵守约束的情况下被击中。存在量化第一函数的输入和第二函数的输入的前像的前像，以创建可合成的前像。可合成的前像被简化和合成，以创建一个扩大的目标。执行放大目标的验证。

13. 发明授权

US07315996B2 Method and system for performing heuristic constraint simplification 失效
标题翻译：执行启发式约束简化的方法和系统
公开(公告)号：US07315996B2
公开(公告)日：2008-01-01
申请号：US11232764
申请日：2005-09-22
申请人： 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 reparameterization 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.
摘要翻译：公开了一种用于执行验证的方法。该方法包括选择第一计算机设计约束以简化并应用结构重新参数化以简化第一计算机设计约束。响应于确定第一计算机设计约束不被消除，第一计算机设计约束被设置为等于约束的死端状态。响应于确定第一计算机设计约束的目标和死端状态的组合等于目标和第一计算机设计约束的结构前图像的组合，创建第一计算机设计约束的结构预图像第一个计算机设计约束，第一个计算机设计约束被设置为等于结构前像。

14. 发明授权

US08589837B1 Constructing inductive counterexamples in a multi-algorithm verification framework 失效
标题翻译：在多算法验证框架中构建归纳反例
公开(公告)号：US08589837B1
公开(公告)日：2013-11-19
申请号：US13455839
申请日：2012-04-25
申请人： Jason R. Baumgartner , Michael L. Case , Robert L. Kanzelman , Hari Mony
发明人： Jason R. Baumgartner , Michael L. Case , Robert L. Kanzelman , Hari Mony
IPC分类号： G06F17/50
CPC分类号： G06F17/505 , G06F17/504
摘要： A computer-implemented method simplifies a netlist, verifies the simplified netlist using induction, and remaps resulting inductive counterexamples via inductive trace lifting within a multi-algorithm verification framework. The method includes: a processor deriving a first unreachable state information that can be utilized to simplify the netlist; performing a simplification of the netlist utilizing the first unreachable state information; determining whether the first unreachable state information can be inductively proved on an original version of the netlist; and in response to the first unreachable state information not being inductively provable on the original netlist: projecting the first unreachable state information to a minimal subset; and adding the projected unreachable state information as an invariant to further constrain a child induction process. Adding the projected state information as an invariant ensures that any resulting induction counterexamples can be mapped to valid induction counterexamples on the original netlist before undergoing the simplification.
摘要翻译：计算机实现的方法简化网表，使用归纳验证简化的网表，并通过多算法验证框架内的归纳跟踪提升重新生成归纳反例。该方法包括：处理器导出可用于简化网表的第一不可达状态信息; 利用第一不可达状态信息来执行网表的简化; 确定在网表的原始版本上是否可以感应地证明第一不可达状态信息; 并且响应于在原始网表上不被感应地证明的第一不可达状态信息：将第一不可达状态信息投射到最小子集; 并且将预测的不可达状态信息添加为不变量以进一步约束儿童归纳过程。将投影状态信息添加为不变量确保在进行简化之前，任何导致的归因反例可以映射到原始网表上的有效归纳反例。

15. 发明授权

US08407641B2 Logic design verification techniques for liveness checking with retiming 有权
标题翻译：重新定义活动检查的逻辑设计验证技术
公开(公告)号：US08407641B2
公开(公告)日：2013-03-26
申请号：US13436196
申请日：2012-03-30
申请人： Jason R. Baumgartner , Gabor Bobok , Paul Joseph Roessler , Mark Allen Williams
发明人： Jason R. Baumgartner , Gabor Bobok , Paul Joseph Roessler , Mark Allen Williams
IPC分类号： G06F9/455 , G06F17/50
CPC分类号： G06F17/5031 , G06F17/504 , G06F2217/84
摘要： A technique for verification of a retimed logic design using liveness checking includes assigning a liveness gate to a liveness property for an original netlist and assigning a fairness gate to a fairness constraint for the original netlist. In this case, the fairness gate is associated with the liveness gate and is asserted for at least one time-step during any valid behavioral loop associated with the liveness gate. The original netlist is retimed, using a retiming engine, to provide a retimed netlist. The liveness and fairness gates of the retimed netlist are retimed such that a lag of the fairness gate is no greater than a lag of the liveness gate. Verification analysis is then performed on the retimed netlist. Finally, when the verification analysis yields a valid counter-example trace for the retimed netlist, a liveness violation for the original netlist is returned.
摘要翻译：用于使用活动检查验证重新定时逻辑设计的技术包括将活跃门分配给原始网表的活动属性，并将公平门分配给原始网表的公平约束。在这种情况下，公平门与活跃门相关联，并且在与活跃门相关联的任何有效行为循环期间被断言至少一个时间步长。使用重新定时引擎重新计算原始网表，以提供重新定时的网表。重新定义的网表的活跃和公平的门被重新定位，使得公平门的滞后不大于活跃门的滞后。然后在重新定时的网表上进行验证分析。最后，当验证分析为重新定时的网表产生有效的对照示例时，返回原始网表的活动违反。

16. 发明授权

US08307313B2 Minimizing memory array representations for enhanced synthesis and verification 有权
标题翻译：最小化存储器阵列表示，以增强综合和验证
公开(公告)号：US08307313B2
公开(公告)日：2012-11-06
申请号：US12775607
申请日：2010-05-07
申请人： Jason R. Baumgartner , Michael L. Case , Robert L. Kanzelman , Hari Mony
发明人： Jason R. Baumgartner , Michael L. Case , Robert L. Kanzelman , Hari Mony
IPC分类号： G06F17/50 , G06F9/455 , G06F15/16
CPC分类号： G06F17/505
摘要： Mechanisms are provided in a design environment for minimizing memory array representations for enhanced synthesis and verification. The design environment comprises one mechanism to compress the width of arrays using disconnected pin information. The design environment comprises another mechanism to simplify the enable conditions of array ports using “don't care” computations. The design environment comprises yet another mechanism to reduce address pins from an array through analysis of limitations of readable addresses.
摘要翻译：在用于最小化存储器阵列表示以用于增强的合成和验证的设计环境中提供机制。设计环境包括使用断开的引脚信息压缩阵列宽度的一种机制。设计环境包括使用无关心计算简化阵列端口使能条件的另一种机制。设计环境包括通过分析可读地址的限制来减少地址引脚从阵列的另一机制。

17. 发明授权

US08255848B2 Logic design verification techniques for liveness checking with retiming 有权
标题翻译：重新定义活动检查的逻辑设计验证技术
公开(公告)号：US08255848B2
公开(公告)日：2012-08-28
申请号：US12394560
申请日：2009-02-27
申请人： Jason R. Baumgartner , Gabor Bobok , Paul Joseph Roessler , Mark Allen Williams
发明人： Jason R. Baumgartner , Gabor Bobok , Paul Joseph Roessler , Mark Allen Williams
IPC分类号： G06F9/455 , G06F17/50
CPC分类号： G06F17/5031 , G06F17/504 , G06F2217/84
摘要： A technique for verification of a retimed logic design using liveness checking includes assigning a liveness gate to a liveness property for an original netlist and assigning a fairness gate to a fairness constraint for the original netlist. In this case, the fairness gate is associated with the liveness gate and is asserted for at least one time-step during any valid behavioral loop associated with the liveness gate. The original netlist is retimed, using a retiming engine, to provide a retimed netlist. The liveness and fairness gates of the retimed netlist are retimed such that a lag of the fairness gate is no greater than a lag of the liveness gate. Verification analysis is then performed on the retimed netlist. Finally, when the verification analysis yields a valid counter-example trace for the retimed netlist, a liveness violation for the original netlist is returned.
摘要翻译：用于使用活动检查验证重新定时逻辑设计的技术包括将活跃门分配给原始网表的活动属性，并将公平门分配给原始网表的公平约束。在这种情况下，公平门与活跃门相关联，并且在与活跃门相关联的任何有效行为循环期间被断言至少一个时间步长。使用重新定时引擎重新计算原始网表，以提供重新定时的网表。重新定义的网表的活跃和公平的门被重新定位，使得公平门的滞后不大于活跃门的滞后。然后在重新定时的网表上进行验证分析。最后，当验证分析为重新定时的网表产生有效的对照示例时，返回原始网表的活动违反。

18. 发明授权

US08201118B2 Method and system for dynamic automated hint generation for enhanced reachability analysis 有权
标题翻译：用于增强可达性分析的动态自动提示生成方法和系统
公开(公告)号：US08201118B2
公开(公告)日：2012-06-12
申请号：US12475494
申请日：2009-05-30
申请人： Jason R. Baumgartner , Paul J. Roessler , Mark A. Williams , Jiazhao Xu
发明人： Jason R. Baumgartner , Paul J. Roessler , Mark A. Williams , Jiazhao Xu
IPC分类号： G06F17/50
CPC分类号： G06F17/504
摘要： Methods and systems are provided for dynamically generating a hint set for enhanced reachability analysis in a sequential circuitry design that is represented by a Binary Decision Diagram (BDD). After determining a ranking of the BDD variables, they are sorted in the order of the ranking. The ranking is used to select some of the variables for use in creating hints for more efficiently performing the reachability analysis in a creating an equivalent sequential circuitry design.
摘要翻译：提供了方法和系统，用于在由二进制决策图（BDD）表示的顺序电路设计中动态生成用于增强可达性分析的提示集。在确定BDD变量的排名之后，按照排名的顺序进行排序。排名被用于选择一些用于创建提示的变量，以在创建等效的顺序电路设计中更有效地执行可达性分析。

19. 发明授权

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.
摘要翻译：公开了一种用于执行验证的方法。该方法包括选择一组门以添加到第一定位网表并形成细化网表。使用在细化网表中具有一个或多个门的信宿和包括原始网表的一个或多个输入和不属于细化网表的原始网表的一个或多个寄存器寄存器的源来计算最小值。通过将一个或多个门添加到细化网表来获得最终的本地化网表，以增加细化网表，直到达到最小切割的一个或多个切割点。

20. 发明申请

US20120054701A1 Optimal Correlated Array Abstraction 有权
标题翻译：最优相关数组抽象
公开(公告)号：US20120054701A1
公开(公告)日：2012-03-01
申请号：US12871962
申请日：2010-08-31
申请人： Jason R. Baumgartner , Michael L. Case , Robert L. Kanzelman , Hari Mony
发明人： Jason R. Baumgartner , Michael L. Case , Robert L. Kanzelman , Hari Mony
IPC分类号： G06F17/50 , G06F9/455
CPC分类号： G06F17/504
摘要： Mechanisms are provided for refining an abstraction of a netlist for verification or synthesis of an integrated circuit design. The mechanisms receive an abstracted netlist corresponding to an original netlist of the integrated circuit design. The mechanisms determine elements already present in the abstracted netlist and refine the abstracted netlist by expanding the abstracted netlist to include additional elements that are correlated with the elements already present in the abstracted netlist to thereby generate a refined abstracted netlist. In addition, the mechanisms utilize the refined abstracted netlist to perform at least one of verification or synthesis of the integrated circuit design.
摘要翻译：提供了用于改进用于验证或综合集成电路设计的网表的抽象的机制。这些机制接收到与集成电路设计的原始网表相对应的抽象网表。这些机制确定已经存在于抽象网表中的元素，并通过扩展抽象网表来改进抽象网表，以包括与抽象网表中已经存在的元素相关联的附加元素，从而生成精简抽象网表。另外，这些机制利用精简的抽象网表来执行集成电路设计的验证或合成中的至少一个。

你已经成功收藏专利！

检索式保存成功!

IPRDB

热门服务

关于我们

友情链接

联系方式