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

31. 发明授权

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.
摘要翻译：用于执行验证的方法包括：为设计接收设计和构建包含表示一个或多个变量的一个或多个节点的中间二进制判定图集。通过将第一个胖子变量设置为一个初始值，对由一个或多个节点表示的一个或多个变量中的第一个胖子变量执行第一个分解，并且对该中间二进制判定图集执行第一个共同构想相对于使用主值的逆的一个或多个节点来生成第一辅因子二进制决策图集。对相对于一个或多个节点设置的中间二进制判定图，使用主值来生成第二共有二元决策图集，执行第二共同构想，并且通过评估第二构成二进制的属性来执行设计的验证决策图集。

32. 发明授权

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元决策表示的并集描述逻辑函数，报告联合。

33. 发明授权

US09063807B2 Method and structure for provably fair random number generator 有权
标题翻译：可靠公允的随机数发生器的方法和结构
公开(公告)号：US09063807B2
公开(公告)日：2015-06-23
申请号：US13594253
申请日：2012-08-24
申请人： Krishnan Kunjunny Kailas , Brian Chan Monwai , Viresh Paruthi
发明人： Krishnan Kunjunny Kailas , Brian Chan Monwai , Viresh Paruthi
IPC分类号： G06F7/58 , G06F13/14
CPC分类号： G06F7/58 , G06F13/14
摘要： A random number generator includes a fairness checker and correction module that ensures that a complete random sequence within a predetermined period of time will be output by the random number generator.
摘要翻译：随机数生成器包括公平校验器和校正模块，其确保在随机数发生器内将在预定时间段内的完整随机序列输出。

34. 发明授权

US08756543B2 Verifying data intensive state transition machines related application 失效
标题翻译：验证数据密集型状态转换机相关应用
公开(公告)号：US08756543B2
公开(公告)日：2014-06-17
申请号：US13097171
申请日：2011-04-29
申请人： Viresh Paruthi , Peter Anthony Sandon , Jun Sawada
发明人： Viresh Paruthi , Peter Anthony Sandon , Jun Sawada
IPC分类号： G06F9/455 , G06F17/50
CPC分类号： G06F17/504 , G06F9/4498 , G06F17/5022
摘要： A method, system, and computer program product for verification of a state transition machine (STM) are provided in the illustrative embodiments. The STM representing the operation of a circuit configured to perform a computation is received. A segment of the STM is selected from a set of segments of the STM. A set of properties of the segment is determined. The set of properties is translated into a hardware description to form a translation. The segment is verified by verifying whether all relationships between a pre-condition and a post condition in the translation hold true for any set of inputs and any initial state of a hardware design under test. A verification result for the segment is generated. Verification results for each segment in the set of segments are combined to generate a verification result for the STM.
摘要翻译：在说明性实施例中提供了用于验证状态转换机（STM）的方法，系统和计算机程序产品。接收表示被配置为执行计算的电路的操作的STM。从STM的一组段中选择STM的一段。确定该段的一组属性。该属性集被翻译成硬件描述以形成一个翻译。通过验证翻译中的前提条件和后期条件之间的所有关系是否适用于任何一组输入以及所测试的硬件设计的任何初始状态来验证该段。生成段的验证结果。组合段中每个段的验证结果，以生成STM的验证结果。

35. 发明授权

US08397189B2 Model checking in state transition machine verification 有权
标题翻译：状态转换机器验证中的模型检查
公开(公告)号：US08397189B2
公开(公告)日：2013-03-12
申请号：US13097193
申请日：2011-04-29
申请人： Viresh Paruthi , Peter Anthony Sandon , Jun Sawada
发明人： Viresh Paruthi , Peter Anthony Sandon , Jun Sawada
IPC分类号： G06F9/455
CPC分类号： G06F17/504
摘要： A method, system, and computer program product for improved model checking for verification of a state transition machine (STM) are provided. A hardware design under test and a property to be verified are received. A level (k) of induction proof needed for the verification is determined. A circuit representation of the property using the hardware design under test for k base cases is configured for checking that the circuit representation holds true for the property for each of the k base cases, and for testing an induction without hypothesis by testing whether the property holds true after k clock cycles starting from a randomized state, where induction without hypothesis is performed by omitting a test whether the property holds true for the next cycle after the property holds for k successive cycles. The induction proof of the property using the hardware design under test by induction without hypothesis is produced.
摘要翻译：提供了一种用于改进状态转换机（STM）验证的模型检查的方法，系统和计算机程序产品。收到被测试的硬件设计和待验证的属性。确定验证所需的感应等级（k）。配置用于k个基本情况的使用被测硬件设计的属性的电路表示被配置用于检查电路表示对于每个k个基本情况的属性是否成立，以及通过测试属性是否保持来测试没有假设的感应在从随机化状态开始的k个时钟周期之后为真，其中通过省略在k个连续循环的该属性成立后的下一个周期的属性是否成立的情况下执行无假设的诱导。产生使用通过没有假设的感应的被测硬件设计的属性的感应证明。

36. 发明申请

US20120096204A1 Formal Verification of Random Priority-Based Arbiters Using Property Strengthening and Underapproximations 失效
标题翻译：使用属性加强和不足近似的随机优先级仲裁员的正式验证
公开(公告)号：US20120096204A1
公开(公告)日：2012-04-19
申请号：US12906495
申请日：2010-10-18
申请人： Gadiel Auerbach , Fady Copty , David J. Levitt , Viresh Paruthi
发明人： Gadiel Auerbach , Fady Copty , David J. Levitt , Viresh Paruthi
IPC分类号： G06F13/37
CPC分类号： G06F13/364
摘要： A mechanism is provide for formally verifying random priority-based arbiters. A determination is made as to whether a random priority-based arbiter is blocking one of a set of output ports or a set of input ports. Responsive to the first predetermined time period expiring before the processor determines whether the random priority-based arbiter is blocking, a determination is made as to whether the random priority-based arbiter is blocking one of the set of output ports or the set of input ports within a second predetermined time period using the random seed and at least one of property strengthening or underapproximation. Responsive to the processor determining that the random priority-based arbiter satisfies a non-blocking specification such that not one of the set of output ports or the set of input ports is blocked within the second predetermined time period, the random priority-based arbiter is validated as satisfying the non-blocking specification.
摘要翻译：提供了一种正式验证随机优先级仲裁器的机制。确定随机优先级仲裁器是否阻塞一组输出端口或一组输入端口中的一个。响应于在处理器确定基于随机优先级的仲裁器是否阻塞之前到期的第一预定时间段，确定基于随机优先级的仲裁器是否阻塞该组输出端口或输入端口组中的一个在第二预定时间段内使用所述随机种子和性能加强或不足近似中的至少一种。响应于所述处理器确定所述基于随机优先级的仲裁器满足非阻塞规范，使得所述一组输出端口或所述一组输入端口中的一个在所述第二预定时间段内被阻止，所述基于随机优先级的仲裁器是验证满足非阻塞规范。

37. 发明授权

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）库形成顺序逻辑表示。然后，顺序逻辑表示被转换成门级顺序逻辑表示。在变换之后，基于门级顺序逻辑表示验证软件系统。验证后，输出软件系统的验证结果。

38. 发明授权

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

39. 发明申请

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

40. 发明授权

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.
摘要翻译：公开了一种用于验证设计符合期望属性的方法，系统和计算机程序产品。该方法包括接收设计，设计的第一初始状态和关于设计的验证的属性。设计的第一初始状态被扩展以创建包含从设计的第一初始状态可访问的一个或多个状态的第一初始状态的超集。合成超集以定义设计的第二初始状态。超设计对设计的应用通过将切入点插入到超集中来获得修改后的超集，并且参考修改后的超集来验证该属性。

你已经成功收藏专利！

检索式保存成功!

IPRDB

热门服务

关于我们

友情链接

联系方式