-
21.发明授权公开(公告)号：US08086429B2
公开(公告)日：2011-12-27
申请号：US12168469
申请日：2008-07-07
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.
摘要翻译： 用于执行验证的系统包括用于：导入包含组件的设计网表，计算组件的计算输出功能，从输出功能生成输出等效状态集合的装置，识别 用于组件的下一状态功能，用于产生用于下一状态功能的图像等价状态集合的装置，用于对用于下一状态功能的输出和图像等效状态集合进行分类的装置 图像等效状态集合和输出等效状态集合，从下一状态函数获得预图像和输出和图像等效状态以生成输出的前图像，以及 图像等效状态，对组件的原始状态进行分区，以及组件的等效类输入集合。 此外，该系统包括一种装置，用于：选择等效输入组的输入代表，从输入代表形成输入图，合成输入图，并将输入图反映回网表中 以生成修改的网表。
-
22.发明申请System and Method for Sequential Equivalence Checking for Asynchronous Verification 有权用于异步验证的顺序等价检查的系统和方法公开(公告)号：US20090138837A1
公开(公告)日：2009-05-28
申请号：US11945465
申请日：2007-11-27
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.
摘要翻译： 提供了用于执行用于异步验证的顺序等同性检查的系统和方法。 提供了集成电路设计的第一个模型，其具有额外的逻辑，以反映异步交叉的行为的可能方差。 提供了集成电路设计的第二个模型，其不具有该异步行为逻辑，而是与通常用于非异步功能验证任务的最简单的同步模型相关联。 执行顺序等价检查以验证两个模型是输入/输出等效的。 为了解决总线链路的不均匀到达时间，提供了用于识别具有转换位的总线串的逻辑，确定这些线的代表性延迟，比较所有总线线的代表性延迟，以确定 整个总线，并将这个最大延迟应用于其中一个模型。
-
23.发明授权Method and system for performing target enlargement in the presence of constraints 有权在存在约束的情况下执行目标放大的方法和系统公开(公告)号：US07373624B2
公开(公告)日：2008-05-13
申请号：US11225672
申请日：2005-09-13
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.
摘要翻译： 公开了一种用于执行验证的方法。 该方法包括接收包括一个或多个目标，一个或多个约束，一个或多个寄存器和一个或多个输入的设计。 计算一个或多个寄存器中的一个或多个目标之一和一个或多个输入的第一函数。 计算一个或多个寄存器和一个或多个输入中的一个或多个约束中的一个或多个的第二函数。 第一功能和第二功能的输入被存在量化。 执行有界分析以确定一个或多个目标中的一个是否可以在遵守约束的情况下被击中。 存在量化第一函数的输入和第二函数的输入的前像的前像，以创建可合成的前像。 可合成的前像被简化和合成，以创建一个扩大的目标。 执行放大目标的验证。
-
公开(公告)号：US07315996B2
公开(公告)日：2008-01-01
申请号：US11232764
申请日：2005-09-22
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.
摘要翻译： 公开了一种用于执行验证的方法。 该方法包括选择第一计算机设计约束以简化并应用结构重新参数化以简化第一计算机设计约束。 响应于确定第一计算机设计约束不被消除，第一计算机设计约束被设置为等于约束的死端状态。 响应于确定第一计算机设计约束的目标和死端状态的组合等于目标和第一计算机设计约束的结构前图像的组合，创建第一计算机设计约束的结构预图像 第一个计算机设计约束，第一个计算机设计约束被设置为等于结构前像。
-
公开(公告)号：US07475370B2
公开(公告)日：2009-01-06
申请号：US11938656
申请日：2007-11-12
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.
摘要翻译： 公开了一种用于验证设计符合期望属性的方法，系统和计算机程序产品。 该方法包括接收设计，设计的第一初始状态和关于设计的验证的属性。 设计的第一初始状态被扩展以创建包含从设计的第一初始状态可访问的一个或多个状态的第一初始状态的超集。 合成超集以定义设计的第二初始状态。 超设计对设计的应用通过将切入点插入到超集中来获得修改后的超集，并且参考修改后的超集来验证该属性。
-
公开(公告)号：US20080256499A1
公开(公告)日：2008-10-16
申请号：US12164781
申请日：2008-06-30
IPC分类号： G06F17/50
CPC分类号： G06F17/504
摘要： A method for generating a constraint for generating a constraint for use in the verification of an integrated circuit design includes identifying a target in a netlist (N) of the design and creating an overapproximate abstraction (N′) of the netlist. A space state (S′) is created by enumerating the states of N′ from which the identified target may be asserted. A constraint space C′ is then derived from the state space S′, where C′ is the logical complement of S′. The process is repeated for multiple selected targets and the constraint spaces from each iteration are logically ANDed. Creating an overapproximate abstraction may include replacing a sequential gate with a random gate. Identifying a sequential gate may include selecting a target in the netlist, performing underapproximate verification of the target, and, if a spurious failure occurs, selecting a gate further down the fanin chain of the currently selected gate.
摘要翻译： 用于生成用于生成用于集成电路设计的验证的约束的约束的方法包括识别所述设计的网表（N）中的目标并且创建所述网表的过近似抽象（N'）。 通过枚举从其识别出的目标可以被断言的N'的状态来创建空间状态（S'）。 然后从状态空间S'导出约束空间C'，其中C'是S'的逻辑补码。 对于多个选定的目标重复该过程，并且来自每个迭代的约束空间被逻辑地进行AND。 创建过近似抽象可能包括用随机门替换顺序门。 识别顺序门可以包括选择网表中的目标，执行目标的近似不正确的验证，并且如果发生虚假故障，则选择进一步向下沿当前选择的门的扇形链的门。
-
公开(公告)号：US20080066031A1
公开(公告)日：2008-03-13
申请号：US11938656
申请日：2007-11-12
申请人： Jason Baumgartner , Hari Mony , Viresh Paruthi , Jiazhao Xu
发明人： Jason Baumgartner , Hari Mony , Viresh Paruthi , Jiazhao Xu
IPC分类号： G06F17/50
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.
摘要翻译： 公开了一种用于验证设计符合期望属性的方法，系统和计算机程序产品。 该方法包括接收设计，设计的第一初始状态和关于设计的验证的属性。 设计的第一初始状态被扩展以创建包含从设计的第一初始状态可访问的一个或多个状态的第一初始状态的超集。 合成超集以定义设计的第二初始状态。 超设计对设计的应用通过将切入点插入到超集中来获得修改后的超集，并且参考修改后的超集来验证该属性。
-
公开(公告)号：US20080052650A1
公开(公告)日：2008-02-28
申请号：US11938612
申请日：2007-11-12
申请人： Jason Baumgartner , Hari Mony , Viresh Paruthi , Jiazhao Xu
发明人： Jason Baumgartner , Hari Mony , Viresh Paruthi , Jiazhao Xu
IPC分类号： G06F17/50
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.
摘要翻译： 公开了一种用于验证设计符合期望属性的方法，系统和计算机程序产品。 该方法包括接收设计，设计的第一初始状态和关于设计的验证的属性。 设计的第一初始状态被扩展以创建包含从设计的第一初始状态可访问的一个或多个状态的第一初始状态的超集。 合成超集以定义设计的第二初始状态。 超设计对设计的应用通过将切入点插入到超集中来获得修改后的超集，并且参考修改后的超集来验证该属性。
-
公开(公告)号：US07203915B2
公开(公告)日：2007-04-10
申请号：US11077331
申请日：2005-03-10
IPC分类号： G06F17/50
CPC分类号： G06F17/504
摘要： A method, system and computer program product for performing retiming in the presence of constraints are disclosed. The method comprises receiving an initial design containing one or more targets and one or more constraints and enumerating the one or more constraints and the one or more targets into a retiming gate set. A retiming graph is constructed from the initial design, and a retiming solution is obtained on the retiming graph. The retiming solution is normalized. One or more retiming lags from the retiming graph are propagated to the initial design, and the initial design is verified by using a constraint-satisfying analysis to determine whether the one or more targets may be hit while the one or more constraints are satisfied.
摘要翻译： 公开了一种用于在存在约束的情况下执行重新定时的方法，系统和计算机程序产品。 该方法包括接收包含一个或多个目标和一个或多个约束的初始设计，并将一个或多个约束和一个或多个目标列举到重定时门组中。 从初始设计构建重新定时图，并在重新定时图上获得重新定时解决方案。 重新定时解决方案被归一化。 来自重新定时图的一个或多个重新定时延迟被传播到初始设计，并且通过使用约束满足分析来确认初始设计，以确定在满足一个或多个约束的情况下是否可以命中一个或多个目标。
-
公开(公告)号：US20070074136A1
公开(公告)日：2007-03-29
申请号：US11236451
申请日：2005-09-27
申请人： Jason Baumgartner , Hari Mony , Viresh Paruthi , Jiazhao Xu
发明人： Jason Baumgartner , Hari Mony , Viresh Paruthi , Jiazhao Xu
IPC分类号： G06F17/50
CPC分类号： G06F17/504
摘要： A method for generating a constraint for use in the verification of an integrated circuit design includes identifying a target in a netlist (N) of the design and creating an overapproximate abstraction (N′) of the netlist. A space state (S′) is created by enumerating the states of N′ from which the identified target may be asserted. A constraint space C′ is then derived from the state space S′, where C′ is the logical complement of S′. The process is repeated for multiple selected targets and the constraint spaces from each iteration are logically ANDed. Creating an overapproximate abstraction may include replacing a sequential gate with a random gate. Identifying a sequential gate may include selecting a target in the netlist, performing underapproximate verification of the target, and, if a spurious failure occurs, selecting a gate further down the fanin chain of the currently selected gate.
摘要翻译： 一种用于生成用于验证集成电路设计的约束的方法包括识别设计的网表（N）中的目标并创建网表的过近似抽象（N'）。 通过枚举从其识别出的目标可以被断言的N'的状态来创建空间状态（S'）。 然后从状态空间S'导出约束空间C'，其中C'是S'的逻辑补码。 对于多个选定的目标重复该过程，并且来自每个迭代的约束空间被逻辑地进行AND。 创建过近似抽象可能包括用随机门替换顺序门。 识别顺序门可以包括选择网表中的目标，执行目标的近似不正确的验证，并且如果发生虚假故障，则选择进一步向下沿当前选择的门的扇形链的门。
-
-
-
-
-
-
-
-
-
搜索结果
175 条记录 (耗时 0.021 秒)
