公开(公告)号：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.

公开(公告)号：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.

摘要翻译： 公开了一种用于执行电子设计验证的方法，系统和计算机程序产品。 该方法包括接收包括第一目标组，主要输入集和包括一个或多个寄存器的第一寄存器组的设计。 生成设计的二进制决策图分析。 使用第一目标集合和主要输入集合的二进制判定图分析来生成所选寄存器的一个或多个下一个状态的递归提取。 递归提取被分解以产生第二目标集合，并且验证第二目标集合。

公开(公告)号：US07322017B2

公开(公告)日：2008-01-22

申请号：US11011245

申请日：2004-12-14

申请人： 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.

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

公开(公告)号：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.

摘要翻译： 公开了一种用于执行验证的方法，系统和计算机程序产品。 创建包含第一个目标的初始设计网表的第一个抽象，并将其指定为当前抽象，并且当前抽象由可选深度展开。 使用可满足性求解器验证复合目标，并且响应于确定验证步骤已经击中复合目标，检查反例以识别要被断言的第一目标的一个或多个原因。 通过检查反例来构建一个或多个细化对，并通过组合细化对构建第二个抽象。 选择一个或多个学习子句和一个或多个第二抽象和第二抽象的不变量作为当前抽象。 目前的抽象是用可满足性求解器来验证的。

公开(公告)号：US20060248481A1

公开(公告)日：2006-11-02

申请号：US11105616

申请日：2005-04-14

申请人： Jason Baumgartner ,  Geert Janssen ,  Hari Mony ,  Viresh Paruthi

发明人： Jason Baumgartner ,  Geert Janssen ,  Hari Mony ,  Viresh Paruthi

IPC分类号： G06F17/50

CPC分类号： G06F17/5045

摘要： A method, system and computer program product for reversing effects of reparameterization is disclosed. The method comprises receiving an original design, an abstracted design, and a first trace over the abstracted design. One or more conditional values are populated into the first trace over the abstracted design, and a k-step satisfiability check is cast to obtain a second trace. One or more calculated values are concatenated to an initial gate set in the second trace with one or more established values to a generated subset of the initial design in the abstracted trace to form a new trace, and one or more effects of a reparameterization are reversed by returning the new trace over the initial design.

摘要翻译： 公开了一种用于逆参数化反转效果的方法，系统和计算机程序产品。 该方法包括接收原始设计，抽象设计和抽象设计的第一个跟踪。 一个或多个条件值通过抽象设计填充到第一个跟踪中，并且转换k阶可满足性检查以获得第二个跟踪。 一个或多个计算值被连接到具有一个或多个已建立值的第二个跟踪中的初始门集合到抽象跟踪中的初始设计的生成子集以形成新的跟踪，并且重新参数化的一个或多个效果被反转 通过在初始设计中返回新的轨迹。

公开(公告)号：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简化模式，并且根据第一简化模式执行简化初始设计以生成缩减 设计包含减少数量的异或门。 确定缩减设计的尺寸是否小于初始设计的尺寸，并且响应于确定减小的设计的尺寸小于初始设计的尺寸，初始设计被替换为 减少设计。

公开(公告)号：US20060206842A1

公开(公告)日：2006-09-14

申请号：US11077331

申请日：2005-03-10

申请人： 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 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.

摘要翻译： 公开了一种用于在存在约束的情况下执行重新定时的方法，系统和计算机程序产品。 该方法包括接收包含一个或多个目标和一个或多个约束的初始设计，并将一个或多个约束和一个或多个目标列举到重定时门组中。 从初始设计构建重新定时图，并在重新定时图上获得重新定时解决方案。 重新定时解决方案被归一化。 来自重新定时图的一个或多个重新定时延迟被传播到初始设计，并且通过使用约束满足分析来确认初始设计，以确定在满足一个或多个约束的情况下是否可以命中一个或多个目标。

公开(公告)号：US20050188337A1

公开(公告)日：2005-08-25

申请号：US10782673

申请日：2004-02-19

申请人： Jason Baumgartner ,  Robert Kanzelman ,  Hari Mony ,  Viresh Paruthi

发明人： Jason Baumgartner ,  Robert Kanzelman ,  Hari Mony ,  Viresh Paruthi

IPC分类号： G06F17/50

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”逻辑来简化对应确定。 意味着逻辑表示第二设计中的节点达到与第一设计的验证结果相反的状态的条件。

公开(公告)号：US07996800B2

公开(公告)日：2011-08-09

申请号：US12055692

申请日：2008-03-26

申请人： Jason Raymond Baumgarter ,  Robert Lowell Kanzelman ,  Hari Mony ,  Viresh Paruthi

发明人： Jason Raymond Baumgarter ,  Robert Lowell Kanzelman ,  Hari Mony ,  Viresh Paruthi

IPC分类号： G06F17/50

CPC分类号： G06F17/504

摘要： System and software for verifying that a model of an integrated circuit satisfies its specification includes performing a sequence of at least one sequential transformation on a sequential model of the integrated circuit to produce a simplified sequential model of the integrated circuit. Thereafter, the simplified sequential model is unfolded for N time steps to create a combinational representation of the design. A sequence of at least one combinational transformation algorithms is then performed on the unfolded design to produce a simplified unfolded model. Finally, an exhaustive search algorithm is performed on the simplified unfolded model. The sequence of sequential transformations may include a sequential redundancy removal (SRR) algorithm and/or another sequential algorithm such as a retiming transformation. The combinational transformations may include a combinational redundancy removal algorithm or a logic re-encoding algorithm. The exhaustive search includes performing an exhaustive satisfiability search by propagating a binary decision diagram (BDD) through the netlist.

摘要翻译： 用于验证集成电路的模型满足其规范的系统和软件包括在集成电路的顺序模型上执行至少一个顺序变换的序列以产生集成电路的简化的顺序模型。 此后，简化的顺序模型展开N个时间步骤以创建设计的组合表示。 然后在展开的设计上执行至少一个组合变换算法的序列以产生简化的展开模型。 最后，对简化的展开模型进行详尽的搜索算法。 顺序变换的顺序可以包括顺序冗余删除（SRR）算法和/或诸如重定时变换的其他顺序算法。 组合变换可以包括组合冗余删除算法或逻辑重新编码算法。 详尽的搜索包括通过网表传播二进制决策图（BDD）来执行穷尽的可满足性搜索。

公开(公告)号：US07882459B2

公开(公告)日：2011-02-01

申请号：US11944668

申请日：2007-11-26

申请人： 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 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简化模式，并且执行根据第一简化模式的初始设计的简化以生成缩减设计 。 确定减小设计的尺寸是否小于初始设计的尺寸，并且响应于确定减小的设计的尺寸小于初始设计的尺寸，初始设计被替换为简化的设计 。