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

11. 发明申请

US20100138805A9 Method and System for Building Binary Decision Diagrams Efficiently in a Structural Network Representation of a Digital Circuit 有权
标题翻译：在数字电路的结构网络表示中有效构建二进制决策图的方法和系统
公开(公告)号：US20100138805A9
公开(公告)日：2010-06-03
申请号：US11963325
申请日：2007-12-21
申请人： Viresh Paruthi , Christian Jacobi , Geert Janssen , Jiazhao Xu , Kai Oliver Weber
发明人： Viresh Paruthi , Christian Jacobi , Geert Janssen , Jiazhao Xu , Kai Oliver Weber
IPC分类号： G06F17/50
CPC分类号： G06F17/30958 , G06F17/504 , Y10S707/99942
摘要： A method, system and computer program product for building decision diagrams efficiently in a structural network representation of a digital circuit using a dynamic resource constrained and interleaved depth-first-search and modified breadth-first-search schedule is disclosed. The method includes setting a first size limit for a first set of one or more m-ary decision representations describing a logic function and setting a second size limit for a second set of one or more m-ary decision representations describing a logic function. The first set of m-ary decision representations of the logic function is then built with one of the set of a depth-first technique or a breadth-first technique until the first size limit is reached, and a second set of m-ary decision representations of the logic function is built with the other technique until the second size limit is reached. In response to determining that a union of first set and the second set of m-ary decision representations do not describe the logic function, the first and second size limits are increased, and the steps of building the first and second set are repeated. In response to determining that the union of the first set of m-ary decision representations and the second set of m-ary decision representations describe the logic function, the union is reported.
摘要翻译：公开了一种用于在使用动态资源约束和交织的深度优先搜索和修改的宽度优先搜索时间表的数字电路的结构网络表示中有效地构建决策图的方法，系统和计算机程序产品。该方法包括：对描述逻辑功能的一个或多个多元决策表示的第一集合设置第一大小限制，并为描述逻辑功能的一个或多个虚拟决策表示的第二组设置第二大小限制。然后，利用深度优先技术或宽度优先技术的集合之一构建逻辑功能的第一组m元决定表示，直到达到第一大小限制，并且第二组m元决定使用其他技术构建逻辑功能的表示，直到达到第二个大小限制。响应于确定第一集合和第二组m元决定表示的并集不描述逻辑函数，增加第一和第二大小限制，并且重复构建第一集合和第二集合的步骤。响应于确定第一组m元决策表示和第二组m元决策表示的并集描述逻辑函数，报告联合。

12. 发明申请

US20090164966A1 Method and System for Building Binary Decision Diagrams Efficiently in a Structural Network Representation of a Digital Circuit 有权
公开(公告)号：US20090164966A1
公开(公告)日：2009-06-25
申请号：US11963325
申请日：2007-12-21
申请人： Viresh Paruthi , Christian Jacobi , Geert Janssen , Jiazhao Xu , Kai Oliver Weber
发明人： Viresh Paruthi , Christian Jacobi , Geert Janssen , Jiazhao Xu , Kai Oliver Weber
IPC分类号： G06F17/50
CPC分类号： G06F17/30958 , G06F17/504 , Y10S707/99942
摘要： A method, system and computer program product for building decision diagrams efficiently in a structural network representation of a digital circuit using a dynamic resource constrained and interleaved depth-first-search and modified breadth-first-search schedule is disclosed. The method includes setting a first size limit for a first set of one or more m-ary decision representations describing a logic function and setting a second size limit for a second set of one or more m-ary decision representations describing a logic function. The first set of m-ary decision representations of the logic function is then built with one of the set of a depth-first technique or a breadth-first technique until the first size limit is reached, and a second set of m-ary decision representations of the logic function is built with the other technique until the second size limit is reached. In response to determining that a union of first set and the second set of m-ary decision representations do not describe the logic function, the first and second size limits are increased, and the steps of building the first and second set are repeated. In response to determining that the union of the first set of m-ary decision representations and the second set of m-ary decision representations describe the logic function, the union is reported.

13. 发明申请

US20090164965A1 Method and System for Building Binary Decision Diagrams Efficiently in a Structural Network Representation of a Digital Circuit 有权
标题翻译：在数字电路的结构网络表示中有效构建二进制决策图的方法和系统
公开(公告)号：US20090164965A1
公开(公告)日：2009-06-25
申请号：US11963267
申请日：2007-12-21
申请人： Viresh Paruthi , Christian Jacobi , Geert Janssen , Jiazhao Xu , Kai Oliver Weber
发明人： Viresh Paruthi , Christian Jacobi , Geert Janssen , Jiazhao Xu , Kai Oliver Weber
IPC分类号： G06F17/50
CPC分类号： G06F17/30958 , G06F17/504 , Y10S707/99942
摘要： A method, system and computer program product for building decision diagrams efficiently in a structural network representation of a digital circuit using a dynamic resource constrained and interleaved depth-first-search and modified breadth-first-search schedule is disclosed. The method includes setting a first size limit for a first set of one or more m-ary decision representations describing a logic function and setting a second size limit for a second set of one or more m-ary decision representations describing a logic function. The first set of m-ary decision representations of the logic function is then built with one of the set of a depth-first technique or a breadth-first technique until the first size limit is reached, and a second set of m-ary decision representations of the logic function is built with the other technique until the second size limit is reached. In response to determining that a union of first set and the second set of m-ary decision representations do not describe the logic function, the first and second size limits are increased, and the steps of building the first and second set are repeated. In response to determining that the union of the first set of m-ary decision representations and the second set of m-ary decision representations describe the logic function, the union is reported.
摘要翻译：公开了一种用于在使用动态资源约束和交织的深度优先搜索和修改的宽度优先搜索时间表的数字电路的结构网络表示中有效地构建决策图的方法，系统和计算机程序产品。该方法包括：对描述逻辑功能的一个或多个多元决策表示的第一集合设置第一大小限制，并为描述逻辑功能的一个或多个虚拟决策表示的第二组设置第二大小限制。然后，利用深度优先技术或宽度优先技术的集合之一构建逻辑功能的第一组m元决定表示，直到达到第一大小限制，并且第二组m元决定使用其他技术构建逻辑功能的表示，直到达到第二个大小限制。响应于确定第一集合和第二组m元决定表示的并集不描述逻辑函数，增加第一和第二大小限制，并且重复构建第一集合和第二集合的步骤。响应于确定第一组m元决策表示和第二组m元决策表示的并集描述逻辑函数，报告联合。

14. 发明授权

US07363603B2 Method and system for case-splitting on nodes in a symbolic simulation framework 有权
标题翻译：符号仿真框架中节点分割的方法和系统
公开(公告)号：US07363603B2
公开(公告)日：2008-04-22
申请号：US11225651
申请日：2005-09-13
申请人： Christian Jacobi , Geert Janssen , Viresh Paruthi , Kai Oliver Weber
发明人： Christian Jacobi , Geert Janssen , Viresh Paruthi , Kai Oliver Weber
IPC分类号： G06F9/45 , G06F17/50
CPC分类号： G06F17/504
摘要： A method for performing verification includes receiving a design and building for the design an intermediate binary decision diagram set containing one or more nodes representing one or more variables. A first case-splitting is performed upon a first fattest variable from among the one or more variables represented by the one or more nodes by setting the first fattest variable to a primary value, and a first cofactoring is performed upon the intermediate binary decision diagram set with respect to the one or more nodes using an inverse of the primary value to generate a first cofactored binary decision diagram set. A second cofactoring is performed upon the intermediate binary decision diagram set with respect to the one or more nodes using the primary value to generate a second cofactored binary decision diagram set, and verification of the design is performed by evaluating a property of the second cofactored binary decision diagram set.
摘要翻译：用于执行验证的方法包括：为设计接收设计和构建包含表示一个或多个变量的一个或多个节点的中间二进制判定图集。通过将第一个胖子变量设置为一个初始值，对由一个或多个节点表示的一个或多个变量中的第一个胖子变量执行第一个分解，并且对该中间二进制判定图集执行第一个共同构想相对于使用主值的逆的一个或多个节点来生成第一辅因子二进制决策图集。对相对于一个或多个节点设置的中间二进制判定图，使用主值来生成第二共有二元决策图集，执行第二共同构想，并且通过评估第二构成二进制的属性来执行设计的验证决策图集。

15. 发明授权

US07340473B2 Method and system for building binary decision diagrams efficiently in a structural network representation of a digital circuit 有权
标题翻译：在数字电路的结构网络表示中有效构建二进制决策图的方法和系统
公开(公告)号：US07340473B2
公开(公告)日：2008-03-04
申请号：US10926587
申请日：2004-08-26
申请人： Viresh Paruthi , Christian Jacobi , Geert Janssen , Jiazhao Xu , Kai Oliver Weber
发明人： Viresh Paruthi , Christian Jacobi , Geert Janssen , Jiazhao Xu , Kai Oliver Weber
IPC分类号： G06F17/50
CPC分类号： G06F17/30958 , G06F17/504 , Y10S707/99942
摘要： A method, system and computer program product for building decision diagrams efficiently in a structural network representation of a digital circuit using a dynamic resource constrained and interleaved depth-first-search and modified breadth-first-search schedule is disclosed. The method includes setting a first size limit for a first set of one or more m-ary decision representations describing a logic function and setting a second size limit for a second set of one or more m-ary decision representations describing a logic function. The first set of m-ary decision representations of the logic function is then built with one of the set of a depth-first technique or a breadth-first technique until the first size limit is reached, and a second set of m-ary decision representations of the logic function is built with the other technique until the second size limit is reached. In response to determining that a union of first set and the second set of m-ary decision representations do not describe the logic function, the first and second size limits are increased, and the steps of building the first and second set are repeated. In response to determining that the union of the first set of m-ary decision representations and the second set of m-ary decision representations describe the logic function, the union is reported.
摘要翻译：公开了一种用于在使用动态资源约束和交织的深度优先搜索和修改的宽度优先搜索时间表的数字电路的结构网络表示中有效地构建决策图的方法，系统和计算机程序产品。该方法包括：对描述逻辑功能的一个或多个多元决策表示的第一集合设置第一大小限制，并为描述逻辑功能的一个或多个虚拟决策表示的第二组设置第二大小限制。然后，利用深度优先技术或宽度优先技术的集合之一构建逻辑功能的第一组m元决定表示，直到达到第一大小限制，并且第二组m元决定使用其他技术构建逻辑功能的表示，直到达到第二个大小限制。响应于确定第一集合和第二组m元决定表示的并集不描述逻辑函数，增加第一和第二大小限制，并且重复构建第一集合和第二集合的步骤。响应于确定第一组m元决策表示和第二组m元决策表示的并集描述逻辑函数，报告联合。

16. 发明授权

US07788615B2 Computer program product for verification using reachability overapproximation 失效
标题翻译：使用可达性过近似的验证计算机程序产品
公开(公告)号：US07788615B2
公开(公告)日：2010-08-31
申请号：US11938612
申请日：2007-11-12
申请人： Jason Raymond Baumgartner , Hari Mony , Viresh Paruthi , Jiazhao Xu
发明人： Jason Raymond Baumgartner , Hari Mony , Viresh Paruthi , Jiazhao Xu
IPC分类号： G06F17/50 , G06F9/45
CPC分类号： G06F17/504
摘要： A method, system and computer program product for verifying that a design conforms to a desired property is disclosed. The method comprises receiving a design, a first initial state of the design, and a property for verification with respect to the design. The first initial state of the design is expanded to create a superset of the first initial state containing one or more states reachable from the first initial state of the design. A superset is synthesized to define a second initial state of the design. Application of the superset to the design is overapproximated through cutpoint insertion into the superset to obtain a modified superset, and the property is verified with reference to the modified superset.
摘要翻译：公开了一种用于验证设计符合期望属性的方法，系统和计算机程序产品。该方法包括接收设计，设计的第一初始状态和关于设计的验证的属性。设计的第一初始状态被扩展以创建包含从设计的第一初始状态可访问的一个或多个状态的第一初始状态的超集。合成超集以定义设计的第二初始状态。超设计对设计的应用通过将切入点插入到超集中来获得修改后的超集，并且参考修改后的超集来验证该属性。

17. 发明授权

US07367002B2 Method and system for parametric reduction of sequential designs 有权
标题翻译：顺序设计参数化减少的方法和系统
公开(公告)号：US07367002B2
公开(公告)日：2008-04-29
申请号：US11105615
申请日：2005-04-14
申请人： Jason Raymond Baumgartner , Geert Janssen , Hari Mony , Viresh Paruthi
发明人： Jason Raymond Baumgartner , Geert Janssen , Hari Mony , Viresh Paruthi
IPC分类号： G06F17/50 , G06F9/45
CPC分类号： G06F17/5045 , G06F17/504
摘要： A method, system and computer program product for performing parametric reduction of sequential designs. According to an embodiment of the present invention, the method includes receiving an initial design including one or more primary inputs, one or more targets, and one or more state elements. A cut of the initial design including one or more cut gates is identified, and a relation of one or more values producible to the one or more cut gates in terms of the one or more primary inputs and the one or more state elements is computed. The relation is synthesized to form a gate set, and an abstracted design is formed from the gate set. Verification is performed on the abstracted design to generate verification results.
摘要翻译：一种用于执行顺序设计的参数化减少的方法，系统和计算机程序产品。根据本发明的实施例，该方法包括接收包括一个或多个主要输入，一个或多个目标以及一个或多个状态元素的初始设计。识别包括一个或多个切割门的初始设计的切割，并且计算在一个或多个主要输入和一个或多个状态元素方面可生产到一个或多个切割门的一个或多个值的关系。该关系被合成以形成一个栅极集合，并且从栅极集合形成抽象的设计。对抽象设计进行验证以生成验证结果。

18. 发明授权

US07350179B2 Method for improved synthesis of binary decision diagrams with inverted edges and quantifiable as well as nonquantifiable variables 有权
标题翻译：用于改进具有反向边缘和可量化以及不可量化变量的二进制决策图的合成的方法
公开(公告)号：US07350179B2
公开(公告)日：2008-03-25
申请号：US11105618
申请日：2005-04-14
申请人： Jason Raymond Baumgartner , Geert Janssen , Hari Mony , Viresh Paruthi
发明人： Jason Raymond Baumgartner , Geert Janssen , Hari Mony , Viresh Paruthi
IPC分类号： G06F17/50
CPC分类号： G06F17/5045
摘要： A method, system and computer program product for performing synthesis of representations is disclosed. The method comprises receiving a representation of a relation and building a gate representing an OR function of one or more selected parent paths into a node of said representation of said relation. A synthesized gate for said gate representing said OR function and synthesis of a set of representations of relations by iterating said building step and said creating step over one or more variables in said representation of said relation is performed to accumulate a synthesized gate set, which synthesized gate set is returned.
摘要翻译：公开了一种用于执行表示的综合的方法，系统和计算机程序产品。该方法包括接收关系的表示，并且构建表示一个或多个所选父路径的OR函数的门到所述关系的所述表示的节点中。执行表示所述OR函数的所述门的合成门，并且通过在所述关系的所述表示中迭代所述构建步骤和所述创建步骤对一个或多个变量进行迭代来合成关系表示集合，以累加合成门集合，其合成返回门组。

19. 发明授权

US07093218B2 Incremental, assertion-based design verification 失效
标题翻译：增量，断言为基础的设计验证
公开(公告)号：US07093218B2
公开(公告)日：2006-08-15
申请号：US10782673
申请日：2004-02-19
申请人： Jason Raymond Baumgartner , Robert Lowell Kanzelman , Hari Mony , Viresh Paruthi
发明人： Jason Raymond Baumgartner , Robert Lowell Kanzelman , Hari Mony , Viresh Paruthi
IPC分类号： G06F17/50 , G06F19/00
CPC分类号： G06F17/5022
摘要： A design verification system includes a first verification engine to model the operation of a first design of an integrated circuit to obtain verification results including the model's adherence to a property during N time steps of its operation, proofs that one or more verification targets can be reached, and verification coverage results for targets that are not reached. A correspondence engine determines the functional correspondence between the first design and a second design of the integrated circuit. Functional correspondence, if demonstrated, enables reuse of the first engine's verification results to reduce resources expended during subsequent analysis of the second design. The correspondence determination may be simplified using a composite model of the integrated circuit having “implies” logic in lieu of “EXOR” logic. The implies logic indicates conditions in which a node in the second design achieves a state that is contrary to the verification results for the first design.
摘要翻译：设计验证系统包括第一验证引擎，用于建模集成电路的第一设计的操作，以获得包括模型在其操作的N个时间步骤期间对属性的遵守性的验证结果，证明可以达到一个或多个验证目标，以及未达到的目标的验证覆盖率结果。通信引擎确定集成电路的第一设计和第二设计之间的功能对应关系。如果证明功能对应关系，则能够重新使用第一引擎的验证结果，以减少后续第二次设计分析中花费的资源。可以使用具有“暗示”逻辑的集成电路的复合模型来代替“EXOR”逻辑来简化对应确定。意味着逻辑表示第二设计中的节点达到与第一设计的验证结果相反的状态的条件。

20. 发明授权

US07831937B2 Method and system for reduction of XOR/XNOR subexpressions in structural design representations 有权
标题翻译：在结构设计表示中减少XOR / XNOR子表达式的方法和系统
公开(公告)号：US07831937B2
公开(公告)日：2010-11-09
申请号：US11955112
申请日：2007-12-12
申请人： Jason Raymond Baumgartner , Robert Lowell Kanzelman , Hari Mony , Viresh Paruthi
发明人： Jason Raymond Baumgartner , Robert Lowell Kanzelman , Hari Mony , Viresh Paruthi
IPC分类号： G06F17/50
CPC分类号： G06F17/505
摘要： A method, system and computer program product for reducing XOR/XNOR subexpressions in structural design representations are disclosed. The method includes receiving an initial design, in which the initial design represents an electronic circuit containing an XOR gate. A first simplification mode for the initial design is selected from a set of applicable simplification modes, wherein the first simplification mode is an XOR/XNOR simplification mode, and a simplification of the initial design is performed according to the first simplification mode to generate a reduced design containing a reduced number of XOR gates. Whether a size of the reduced design is less than a size of the initial design is determined, and, in response to determining that the size of the reduced design is less than a the size of the initial design, the initial design is replaced with the reduced design.
摘要翻译：公开了一种用于在结构设计表示中减少XOR / XNOR子表达式的方法，系统和计算机程序产品。该方法包括接收初始设计，其中初始设计表示包含XOR门的电子电路。从一组适用的简化模式中选择用于初始设计的第一简化模式，其中第一简化模式是XOR / XNOR简化模式，并且根据第一简化模式执行简化初始设计以生成缩减设计包含减少数量的异或门。确定缩减设计的尺寸是否小于初始设计的尺寸，并且响应于确定减小的设计的尺寸小于初始设计的尺寸，初始设计被替换为减少设计。

你已经成功收藏专利！

检索式保存成功!

IPRDB

热门服务

关于我们

友情链接

联系方式