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

1. 发明授权

US08086429B2 Predicate-based compositional minimization in a verification environment 失效
标题翻译：在验证环境中基于谓词的组合最小化
公开(公告)号：US08086429B2
公开(公告)日：2011-12-27
申请号：US12168469
申请日：2008-07-07
申请人： Jason R. Baumgartner , Hari Mony , Viresh Paruthi , Fadi A. Zaraket
发明人： Jason R. Baumgartner , Hari Mony , Viresh Paruthi , Fadi A. Zaraket
IPC分类号： G06F17/50 , G06F7/44
CPC分类号： G06F17/504
摘要： A system for performing verification includes a means for: importing a design netlist containing component(s), computing output function(s) for the component(s), generating output equivalent state set(s) from the output function(s), identifying next-state function(s) for the component(s), means for producing image equivalent state set(s) for the next-state function(s), means for classifying output-and-image equivalent state set(s) for the image equivalent state set(s) and the output equivalent state set(s), getting a preimage from the next-state function(s) and the output-and-image equivalent state(s) to generate a preimage of the output-and-image equivalent state(s), partitioning over original state(s) of the component(s), and equivalent class input set(s) of the component(s). Moreover, the system includes a means for: selecting input representative(s) of the equivalent input set(s), forming an input map from the input representative(s), synthesizing the input map, and injecting the input map back into the netlist to generate a modified netlist.
摘要翻译：用于执行验证的系统包括用于：导入包含组件的设计网表，计算组件的计算输出功能，从输出功能生成输出等效状态集合的装置，识别用于组件的下一状态功能，用于产生用于下一状态功能的图像等价状态集合的装置，用于对用于下一状态功能的输出和图像等效状态集合进行分类的装置图像等效状态集合和输出等效状态集合，从下一状态函数获得预图像和输出和图像等效状态以生成输出的前图像，以及图像等效状态，对组件的原始状态进行分区，以及组件的等效类输入集合。此外，该系统包括一种装置，用于：选择等效输入组的输入代表，从输入代表形成输入图，合成输入图，并将输入图反映回网表中以生成修改的网表。

2. 发明申请

US20080270086A1 PREDICATE-BASED COMPOSITIONAL MINIMIZATION IN A VERIFICATION ENVIRONMENT 失效
标题翻译：验证环境中基于预测的组合最小化
公开(公告)号：US20080270086A1
公开(公告)日：2008-10-30
申请号：US12168469
申请日：2008-07-07
申请人： Jason R. Baumgartner , Hari Mony , Viresh Paruthi , Fadi A. Zaraket
发明人： Jason R. Baumgartner , Hari Mony , Viresh Paruthi , Fadi A. Zaraket
IPC分类号： G06F17/50
CPC分类号： G06F17/504
摘要： A system for performing verification includes a means for: importing a design netlist containing component(s), computing output function(s) for the component(s), generating output equivalent state set(s) from the output function(s), identifying next-state function(s) for the component(s), means for producing image equivalent state set(s) for the next-state function(s), means for classifying output-and-image equivalent state set(s) for the image equivalent state set(s) and the output equivalent state set(s), getting a preimage from the next-state function(s) and the output-and-image equivalent state(s) to generate a preimage of the output-and-image equivalent state(s), partitioning over original state(s) of the component(s), and equivalent class input set(s) of the component(s). Moreover, the system includes a means for: selecting input representative(s) of the equivalent input set(s), forming an input map from the input representative(s), synthesizing the input map, and injecting the input map back into the netlist to generate a modified netlist.
摘要翻译：用于执行验证的系统包括用于：导入包含组件的设计网表，计算组件的计算输出功能，从输出功能生成输出等效状态集合的装置，识别用于组件的下一状态功能，用于产生用于下一状态功能的图像等价状态集合的装置，用于对用于下一状态功能的输出和图像等效状态集合进行分类的装置图像等效状态集合和输出等效状态集合，从下一状态函数获得预图像和输出和图像等效状态以生成输出的前图像，以及图像等效状态，对组件的原始状态进行分区，以及组件的等效类输入集合。此外，该系统包括一种装置，用于：选择等效输入组的输入代表，从输入代表形成输入图，合成输入图，并将输入图反映回网表中以生成修改的网表。

3. 发明授权

US07437690B2 Method for predicate-based compositional minimization in a verification environment 失效
标题翻译：在验证环境中基于谓词的组合最小化方法
公开(公告)号：US07437690B2
公开(公告)日：2008-10-14
申请号：US11249937
申请日：2005-10-13
申请人： Jason R. Baumgartner , Hari Mony , Viresh Paruthi , Fadi A. Zaraket
发明人： Jason R. Baumgartner , Hari Mony , Viresh Paruthi , Fadi A. Zaraket
IPC分类号： G06F17/50
CPC分类号： G06F17/504
摘要： A method for performing verification includes importing a design netlist containing one or more components and computing one or more output functions for the one or more components. One or more output equivalent state sets are generated from the one or more output functions and one or more next-state functions for the one or more components are identified. One or more image equivalent state sets for the one or more next-state functions are produced and one or more output-and-image equivalent state sets are classified for the one or more image equivalent state sets and the one or more output equivalent state sets. One or more input representatives of the one or more equivalent input sets are selected and an input map is formed from the one or more input representatives. The input map is synthesized and injected back into the netlist to generate a modified netlist.
摘要翻译：执行验证的方法包括导入包含一个或多个组件的设计网表，并计算一个或多个组件的一个或多个输出功能。从一个或多个输出功能产生一个或多个输出等效状态集合，并且识别一个或多个组件的一个或多个下一个状态功能。产生用于一个或多个下一状态函数的一个或多个图像等效状态集合，并且对于一个或多个图像等效状态集合和一个或多个输出等效状态集合分类一个或多个输出和图像等效状态集合。选择一个或多个等效输入集合的一个或多个输入代表，并且从一个或多个输入代表形成输入映射。输入图合成并注入网表以生成修改的网表。

4. 发明授权

US08141048B2 Sequential encoding for relational analysis (SERA) of a software model 有权
标题翻译：软件模型的关系分析（SERA）的顺序编码
公开(公告)号：US08141048B2
公开(公告)日：2012-03-20
申请号：US11677652
申请日：2007-02-22
申请人： Jason R. Baumgartner , Ali S. El-Zein , Viresh Paruthi , Fadi A. Zaraket
发明人： Jason R. Baumgartner , Ali S. El-Zein , Viresh Paruthi , Fadi A. Zaraket
IPC分类号： G06F9/44 , G06F9/455
CPC分类号： G06F8/43
摘要： A method of verifying a software system includes receiving a description of a software system described utilizing a high-level modeling language, and responsive thereto, parsing the description and constructing an abstract syntax graph. The abstract syntax graph is transformed into a sequential logic representation of the software system. The sequential logic representation is formed by reference to a Hardware Description Language (HDL) library. Then, the sequential logic representation is transformed into a gate-level sequential logic representation. Following the transforming, the software system is verified based upon the gate-level sequential logic representation. Following verification, results of verification of the software system are output.
摘要翻译：验证软件系统的方法包括接收使用高级建模语言描述的软件系统的描述，并且响应于此，解析描述并构造抽象语法图。抽象语法图被转换成软件系统的顺序逻辑表示。通过参考硬件描述语言（HDL）库形成顺序逻辑表示。然后，顺序逻辑表示被转换成门级顺序逻辑表示。在变换之后，基于门级顺序逻辑表示验证软件系统。验证后，输出软件系统的验证结果。

5. 发明申请

US20080209389A1 Method, System and Program Product Supporting Sequential Encoding for Relational Analysis (SERA) of a Software Model 有权
标题翻译：方法，系统和程序产品支持软件模型的关系分析（SERA）的顺序编码
公开(公告)号：US20080209389A1
公开(公告)日：2008-08-28
申请号：US11677652
申请日：2007-02-22
申请人： Jason R. Baumgartner , Ali S. El-Zein , Viresh Paruthi , Fadi A. Zaraket
发明人： Jason R. Baumgartner , Ali S. El-Zein , Viresh Paruthi , Fadi A. Zaraket
IPC分类号： G06F9/44
CPC分类号： G06F8/43
摘要： A method of verifying a software system includes receiving a description of a software system described utilizing a high-level modeling language, and responsive thereto, parsing the description and constructing an abstract syntax graph. The abstract syntax graph is transformed into a sequential logic representation of the software system, and following the transforming, the software system is verified based upon the sequential logic representation. Following verification, results of verification of the software system are output.
摘要翻译：验证软件系统的方法包括接收使用高级建模语言描述的软件系统的描述，并且响应于此，解析描述并构造抽象语法图。抽象语法图被转换为软件系统的顺序逻辑表示，并且在变换之后，基于顺序逻辑表示验证软件系统。验证后，输出软件系统的验证结果。

6. 发明授权

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'合并为常数来简化网表。

7. 发明申请

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之间的等价关系。

8. 发明授权

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.
摘要翻译：公开了一种用于执行验证的方法。该方法包括接收包括一个或多个目标，一个或多个约束，一个或多个寄存器和一个或多个输入的设计。计算一个或多个寄存器中的一个或多个目标之一和一个或多个输入的第一函数。计算一个或多个寄存器和一个或多个输入中的一个或多个约束中的一个或多个的第二函数。第一功能和第二功能的输入被存在量化。执行有界分析以确定一个或多个目标中的一个是否可以在遵守约束的情况下被击中。存在量化第一函数的输入和第二函数的输入的前像的前像，以创建可合成的前像。可合成的前像被简化和合成，以创建一个扩大的目标。执行放大目标的验证。

9. 发明申请

US20080201128A1 Method and System for Performing Ternary Verification 有权
标题翻译：执行三元验证的方法和系统
公开(公告)号：US20080201128A1
公开(公告)日：2008-08-21
申请号：US11675698
申请日：2007-02-16
申请人： Jason R. Baumgartner , Hari Mony , Viresh Paruthi , Matyas A. Sustik
发明人： Jason R. Baumgartner , Hari Mony , Viresh Paruthi , Matyas A. Sustik
IPC分类号： G06F17/50
CPC分类号： G06F17/505 , G06F17/5022
摘要： A method and system for performing ternary verification is disclosed. Initially, a ternary model is generated from a binary model of a logic circuit design. The pairings used to encode the ternary model are then recorded. Next, the number of the recorded gate pairings is reduced by removing all invalid gate pairings. A ternary verification is performed on the ternary model having a reduced number of gate pairings.
摘要翻译：公开了一种用于执行三元验证的方法和系统。最初，从逻辑电路设计的二进制模型生成三元模型。然后记录用于对三元模型进行编码的配对。接下来，通过去除所有无效的门对配对来减少所记录的门对配对数。对具有减少数量的门对配对的三元模型进行三进制验证。

10. 发明申请

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。网表的输入的最大深度值随后被用作网表的深度。此深度用于定义约束求解的滑动窗口的宽度。

你已经成功收藏专利！

检索式保存成功!

IPRDB

热门服务

关于我们

友情链接

联系方式