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

1. 发明申请

US20080104559A1 Method and System for Enhanced Verification Through Structural Target Decomposition 审中-公开
标题翻译：通过结构目标分解增强验证的方法和系统
公开(公告)号：US20080104559A1
公开(公告)日：2008-05-01
申请号：US11969761
申请日：2008-01-04
申请人： Jason Baumgartner , Robert Kanzelman , Hari Mony , Viresh Paruthi
发明人： Jason Baumgartner , Robert Kanzelman , Hari Mony , Viresh Paruthi
IPC分类号： G06F17/50
CPC分类号： G06F17/5045 , G06F17/504
摘要： A method, system and computer program product for performing verification of an electronic design is disclosed. The method includes receiving a design, wherein the design includes a first target set and a first register set including one or more registers. A structural product extraction is formed from one or more targets from the first target set and the structural product extraction is recursed for one or more next-state functions of a subset of the one or more registers. A sum-of-products form is recursed from the structural product extraction for one or more next-state functions of a subset of the one or more registers and a product-of-sums form of a result of the second recursing is decomposed to generate a decomposition of the product-of-sums form. The decomposition of the product-of-sums form is synthesized into a second target set and a subset of the second target set to recursively decompose is chosen. In response to the subset of the second target set being nonempty, the first target set is recursively decomposed and, in response to the second target set being empty, verification is applied to the second target set.
摘要翻译：公开了一种用于执行电子设计验证的方法，系统和计算机程序产品。该方法包括接收设计，其中该设计包括第一目标组和包括一个或多个寄存器的第一寄存器组。从第一目标集合的一个或多个目标形成结构性产品提取，并且针对一个或多个寄存器的子集的一个或多个下一个状态函数递归结构乘积提取。从一个或多个寄存器的子集的一个或多个下一个状态函数的结构性产品提取中递归产生积和形式，并且将第二次递归的结果的乘积形式分解生成产品总和形式的分解。求和形式的分解被合成为第二目标集合，并且选择第二目标集合的递归分解的子集。响应于第二目标集合的子集是非空的，第一目标集被递归地分解，并且响应于第二目标集合为空，将验证应用于第二目标集合。

2. 发明申请

US20080104558A1 Method and System for Enhanced Verification Through Structural Target Decomposition 审中-公开
公开(公告)号：US20080104558A1
公开(公告)日：2008-05-01
申请号：US11969741
申请日：2008-01-04
申请人： Jason Baumgartner , Robert Kanzelman , Hari Mony , Viresh Paruthi
发明人： Jason Baumgartner , Robert Kanzelman , Hari Mony , Viresh Paruthi
IPC分类号： G06F17/50
CPC分类号： G06F17/5045 , G06F17/504
摘要： A method, system and computer program product for performing verification of an electronic design is disclosed. The method includes receiving a design, wherein the design includes a first target set and a first register set including one or more registers. A structural product extraction is formed from one or more targets from the first target set and the structural product extraction is recursed for one or more next-state functions of a subset of the one or more registers. A sum-of-products form is recursed from the structural product extraction for one or more next-state functions of a subset of the one or more registers and a product-of-sums form of a result of the second recursing is decomposed to generate a decomposition of the product-of-sums form. The decomposition of the product-of-sums form is synthesized into a second target set and a subset of the second target set to recursively decompose is chosen. In response to the subset of the second target set being nonempty, the first target set is recursively decomposed and, in response to the second target set being empty, verification is applied to the second target set.

3. 发明申请

US20080072186A1 Method and System for Reduction of AND/OR Subexpressions in Structural Design Representations 有权
标题翻译：用于减少结构设计表示中的AND / OR子表达式的方法和系统
公开(公告)号：US20080072186A1
公开(公告)日：2008-03-20
申请号：US11944668
申请日：2007-11-26
申请人： Jason Baumgartner , Robert Kanzelman , Hari Mony , Viresh Paruthi
发明人： Jason Baumgartner , Robert Kanzelman , Hari Mony , Viresh Paruthi
IPC分类号： G06F17/50
CPC分类号： G06F17/505
摘要： A method, system and computer program product for reducing subexpressions in structural design representations containing AND and OR gates are disclosed. The method comprises receiving an initial design, in which the initial design represents an electronic circuit, containing an AND gate. A first simplification mode for the initial design from a set of applicable simplification modes is selected, wherein said simplification mode is an AND/OR simplification mode, and a simplification of the initial design according to the first simplification mode is performed to generate a reduced design. 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 the size of the initial design, the initial design is replaced with the reduced design.
摘要翻译：公开了一种用于减少包含AND和OR门的结构设计表示中的子表达式的方法，系统和计算机程序产品。该方法包括接收初始设计，其中初始设计表示包含与门的电子电路。选择用于从一组适用的简化模式进行初始设计的第一简化模式，其中所述简化模式是AND / OR简化模式，并且执行根据第一简化模式的初始设计的简化以生成缩减设计。确定减小设计的尺寸是否小于初始设计的尺寸，并且响应于确定减小的设计的尺寸小于初始设计的尺寸，初始设计被替换为简化的设计。

4. 发明申请

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

5. 发明申请

US20060190873A1 Exploiting suspected redundancy for enhanced design verification 失效
标题翻译：利用疑似冗余来增强设计验证
公开(公告)号：US20060190873A1
公开(公告)日：2006-08-24
申请号：US11054904
申请日：2005-02-10
申请人： Jason Baumgartner , Robert Kanzelman , Hari Mony , Viresh Paruthi
发明人： Jason Baumgartner , Robert Kanzelman , Hari Mony , Viresh Paruthi
IPC分类号： G06F17/50
CPC分类号： G06F17/504
摘要： A verification method foe an integrated circuit includes identifying an equivalence class including a set of candidate gates suspected of exhibiting equivalent behavior and identifying one of the candidate gates as a representative gate for the equivalence class. Equivalence gates of an XOR gate are sourced by the representative gate and a candidate gate. A speculatively reduced netlist is generated by replacing the representative gate as the source gate for edges sourced by a candidate gate in the original design. The speculatively reduced netlist is then used either to verify formally the equivalence of the gates by applying a plurality of transformation engines to the speculatively reduced netlist or to perform incomplete search and, if none of the equivalence gates is asserted during the incomplete search, any verification results derived from the incomplete search can be applied to the original model.
摘要翻译：一种集成电路的验证方法包括识别包括一组疑似表现出等效行为的候选门的等价类，并将候选门之一识别为等价类的代表门。异或门的等效门由代表门和候选门提供。通过将原始设计中的代表门替换为候选门的边缘的源极来产生推测缩小的网表。然后，推测性减少的网表用于通过将多个转换引擎应用于推测性减少的网表或执行不完全搜索来正式验证门的等效性，并且如果在不完全搜索期间没有等价门被断言，则任何验证从不完全搜索得到的结果可以应用于原始模型。

6. 发明申请

US20080091386A1 Method and System for Reduction of XOR/XNOR Subexpressions in Structural Design Representations 有权
标题翻译：减少XOR / XNOR子表达式在结构设计表示中的方法和系统
公开(公告)号：US20080091386A1
公开(公告)日：2008-04-17
申请号：US11955152
申请日：2007-12-12
申请人： Jason Baumgartner , Robert Kanzelman , Hari Mony , Viresh Paruthi
发明人： Jason Baumgartner , Robert 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简化模式，并且根据第一简化模式执行简化初始设计以生成缩减设计包含减少数量的异或门。确定缩减设计的尺寸是否小于初始设计的尺寸，并且响应于确定缩减设计的尺寸小于初始设计的尺寸，初始设计被替换为减少设计。

7. 发明申请

US20080072185A1 Method and System for Reduction of AND/OR Subexpressions in Structural Design Representations 有权
公开(公告)号：US20080072185A1
公开(公告)日：2008-03-20
申请号：US11944663
申请日：2007-11-26
申请人： Jason Baumgartner , Robert Kanzelman , Hari Mony , Viresh Paruthi
发明人： Jason Baumgartner , Robert Kanzelman , Hari Mony , Viresh Paruthi
IPC分类号： G06F17/50
CPC分类号： G06F17/505
摘要： A method, system and computer program product for reducing subexpressions in structural design representations containing AND and OR gates are disclosed. The method comprises receiving an initial design, in which the initial design represents an electronic circuit, containing an AND gate. A first simplification mode for the initial design from a set of applicable simplification modes is selected, wherein said simplification mode is an AND/OR simplification mode, and a simplification of the initial design according to the first simplification mode is performed to generate a reduced design. 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 the size of the initial design, the initial design is replaced with the reduced design.

8. 发明申请

US20080052648A1 METHOD AND SYSTEM FOR ENCHANCED VERIFICATION THROUGH BINARY DECISION DIAGRAM-BASED TARGET DECOMPOSITION 有权
标题翻译：通过二进制决策图目标分解进行加强验证的方法和系统
公开(公告)号：US20080052648A1
公开(公告)日：2008-02-28
申请号：US11848356
申请日：2007-08-31
申请人： Jason Baumgartner , Robert Kanzelman , Hari Mony , Viresh Paruthi
发明人： Jason Baumgartner , Robert Kanzelman , Hari Mony , Viresh Paruthi
IPC分类号： G06F17/50
CPC分类号： G06F17/504
摘要： A method, system and computer program product for performing verification of an electronic design is disclosed. The method includes receiving a design, including a first target set, a primary input set, and a first register set comprising one or more registers. A binary decision diagram analysis of the design is generated. A recursive extraction of one or more next states of selected registers is generated using the binary decision diagram analysis of the first target set and the primary input set. The recursive extraction is decomposed to generate a second target set, and the second target set is verified.
摘要翻译：公开了一种用于执行电子设计验证的方法，系统和计算机程序产品。该方法包括接收包括第一目标组，主要输入集和包括一个或多个寄存器的第一寄存器组的设计。生成设计的二进制决策图分析。使用第一目标集合和主要输入集合的二进制判定图分析来生成所选寄存器的一个或多个下一个状态的递归提取。递归提取被分解以产生第二目标集合，并且验证第二目标集合。

9. 发明申请

US20070174798A1 Method and system for enhanced verification by closely coupling a structural overapproximation algorithm and a structural satisfiability solver 有权
标题翻译：通过紧密耦合结构过近似算法和结构可满足性求解器来增强验证的方法和系统
公开(公告)号：US20070174798A1
公开(公告)日：2007-07-26
申请号：US11340477
申请日：2006-01-26
申请人： Jason Baumgartner , Robert Kanzelman , Hari Mony , Viresh Paruthi
发明人： Jason Baumgartner , Robert 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.
摘要翻译：公开了一种用于执行验证的方法，系统和计算机程序产品。创建包含第一个目标的初始设计网表的第一个抽象，并将其指定为当前抽象，并且当前抽象由可选深度展开。使用可满足性求解器验证复合目标，并且响应于确定验证步骤已经击中复合目标，检查反例以识别要被断言的第一目标的一个或多个原因。通过检查反例来构建一个或多个细化对，并通过组合细化对构建第二个抽象。选择一个或多个学习子句和一个或多个第二抽象和第二抽象的不变量作为当前抽象。目前的抽象是用可满足性求解器来验证的。

10. 发明申请

US20060230366A1 Method and system for reduction of XOR/XNOR subexpressions in structural design representations 失效
标题翻译：在结构设计表示中减少XOR / XNOR子表达式的方法和系统
公开(公告)号：US20060230366A1
公开(公告)日：2006-10-12
申请号：US11086720
申请日：2005-03-22
申请人： Jason Baumgartner , Robert Kanzelman , Hari Mony , Viresh Paruthi
发明人： Jason Baumgartner , Robert 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

热门服务

关于我们

友情链接

联系方式