公开(公告)号：US20060248484A1

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

申请号：US11105611

申请日：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 preserving constraints is disclosed. The method comprises receiving an initial design including one or more targets, one or more primary inputs, one or more constraints and one or more state elements. A cut of the initial design including one or more cut gates, and a relation of one or more values producible to the one or more cut gates in terms of the one or more primary inputs and the one or more state elements is computed. The relation is constrained to force one or more constraint gates representing the one or more constraints to evaluate to a forced valuation, and one or more dead-end states of the constraints are identified. The inverse of the dead-end states is applied as don't cares to simplify the relation and the simplified relation is synthesized to form a first gate set. An abstracted design is from the first gate set and verification is performed on the abstracted design to generate verification results.

摘要翻译： 公开了一种用于保护约束的方法，系统和计算机程序产品。 该方法包括接收包括一个或多个目标，一个或多个主要输入，一个或多个约束和一个或多个状态元素的初始设计。 计算包括一个或多个切割门的初始设计的切割，以及关于一个或多个主要输入和一个或多个状态元素的可生产到一个或多个切割门的一个或多个值的关系。 该关系被限制为强制表示一个或多个约束的一个或多个约束门来评估强制估价，并且识别约束的一个或多个死端状态。 应用死端状态的倒数不需要简化关系，并且简化的关系被合成以形成第一门集。 抽象设计来自第一个门集，并对抽象设计进行验证，以生成验证结果。

公开(公告)号：US20060248482A1

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

申请号：US11105617

申请日：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 preserving critical inputs is disclosed. The method comprises receiving an initial design including one or more primary inputs which cannot be eliminated, one or more primary inputs which can be eliminated, one or more targets, and one or more state elements. A cut of said initial design including one or more cut gates is identified, and a relation of one or more values producible to said one or more cut gates in terms of said one or more primary inputs which cannot be eliminated, said one or more primary inputs which can be eliminated and said one or more state elements is computed. Said relation is synthesized to form a gate set, and an abstracted design is formed from said gate set. Verification is performed on said abstracted design to generate verification results.

摘要翻译： 公开了一种用于保护关键输入的方法，系统和计算机程序产品。 该方法包括接收初始设计，其包括不能被消除的一个或多个主要输入，可被消除的一个或多个主要输入，一个或多个目标以及一个或多个状态元素。 识别包括一个或多个切割门的所述初始设计的切割，以及根据所述一个或多个主要输入而不能被消除的一个或多个可生产到所述一个或多个切割门的值的关系，所述一个或多个主要 可以消除的输入和所述一个或多个状态元素被计算。 所述关系被合成以形成栅极集合，并且从所述栅极集合形成抽象设计。 对所述抽象设计进行验证以产生验证结果。

公开(公告)号：US20060190869A1

公开(公告)日：2006-08-24

申请号：US11050606

申请日：2005-02-03

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

发明人： Jason Baumgartner ,  Robert 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）来执行穷尽的可满足性搜索。

公开(公告)号：US20060190868A1

公开(公告)日：2006-08-24

申请号：US11050592

申请日：2005-02-03

申请人： Jason Baumgartner ,  Christian Jacobi ,  Viresh Paruthi ,  Kai Weber

发明人： Jason Baumgartner ,  Christian Jacobi ,  Viresh Paruthi ,  Kai Weber

IPC分类号： G06F17/50

CPC分类号： G06F17/504

摘要： A method for verifying a design through symbolic simulation is disclosed. The method comprises creating one or more binary decision diagram variables for one or more inputs in a design containing one or more state variables and building a binary decision diagram for a first node of one or more nodes of the design. A binary decision diagram for the initial state function of one or more state variables of the design is generated and the design is subsequently initialized. Binary decisions diagrams for one or more constraints are synthesized. A set of constraint values is accumulated over time by combining the binary decision diagrams for the one or more constraints with a set of previously generated binary decision diagrams for a set of constraints previously used in one or more previous time-steps. A binary decision diagram for the next state function of the one or more state variables in the design is constructed in the presence of the constraints. The one or more state variables in the design are updated by propagating the binary decision diagram for the next state function to the one or more state variables and a set of binary decision diagrams for the one or more targets in the presence of the one or more constraints is calculated. The set of binary decision diagrams for one or more targets is constrained and the design is verified by determining whether the one or more targets were hit.

摘要翻译： 公开了一种通过符号仿真验证设计的方法。 该方法包括为包含一个或多个状态变量的设计中的一个或多个输入创建一个或多个二进制决策图变量，以及为设计的一个或多个节点的第一节点构建二进制决策图。 生成设计的一个或多个状态变量的初始状态函数的二进制决策图，随后初始化设计。 合成一个或多个约束的二进制决策图。 通过将一个或多个约束的二进制判定图与先前在一个或多个先前时间步骤中使用的一组约束的先前生成的二进制决策图的组合来累积一组约束值。 设计中一个或多个状态变量的下一个状态函数的二进制决策图是在有约束的情况下构建的。 设计中的一个或多个状态变量通过将下一个状态函数的二进制决策图传播到一个或多个状态变量和一个或多个目标的存在下的一个或多个目标的一组二进制决策图来更新 计算约束。 用于一个或多个目标的二进制决策图集被约束，并且通过确定一个或多个目标是否被击中来验证设计。

公开(公告)号：US20060047680A1

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

申请号：US10926587

申请日：2004-08-26

申请人： Viresh Paruthi ,  Christian Jacobi ,  Geert Janssen ,  Jiazhao Xu ,  Kai Weber

发明人： Viresh Paruthi ,  Christian Jacobi ,  Geert Janssen ,  Jiazhao Xu ,  Kai Weber

IPC分类号： G06F7/00

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

公开(公告)号：US06993734B2

公开(公告)日：2006-01-31

申请号：US10371002

申请日：2003-02-20

申请人： Jason Raymond Baumgartner ,  Hari Mony ,  Viresh Paruthi ,  Mark Allen Williams

发明人： Jason Raymond Baumgartner ,  Hari Mony ,  Viresh Paruthi ,  Mark Allen Williams

IPC分类号： G06F17/50 ,  G06F9/45

CPC分类号： G06F17/5022

摘要： The disclosed design verification system includes a verification engine to model the operation of an integrated circuit and to assess the model's adherence to a property during N time steps of its operation. The value of N is recorded and propagated. The propagated value of N is used to reduce resources expended during subsequent analysis of the integrated circuit by ignoring the model's adherence to the property during the early stages of subsequent analysis (during time steps less than N). The system may include a diameter estimator that identifies a value of N beyond which subsequent modeling of the integrated circuit produces no new states. Property checking is ignored during states having a time step value greater than the estimated diameter.

摘要翻译： 所公开的设计验证系统包括验证引擎，用于对集成电路的操作进行建模，并且在其操作的N个时间步骤期间评估模型对属性的遵守性。 N的值被记录和传播。 N的传播值用于通过忽略模型在后续分析的早期阶段（在小于N的时间步长期间）对属性的依赖性来减少在后续分析集成电路期间消耗的资源。 系统可以包括识别N的值的直径估计器，超过该值，集成电路的后续建模不产生新的状态。 在具有大于估计直径的时间步长值的状态下，属性检查被忽略。

公开(公告)号：US20130198705A1

公开(公告)日：2013-08-01

申请号：US13360083

申请日：2012-01-27

申请人： Gradus (Geert) Janssen ,  Luis Lastras-Montano ,  Alexey Y. Lvov ,  Viresh Paruthi ,  Robert Shadowen ,  Barry M. Trager ,  Shmuel Winograd ,  Ali El-Zein

发明人： Gradus (Geert) Janssen ,  Luis Lastras-Montano ,  Alexey Y. Lvov ,  Viresh Paruthi ,  Robert Shadowen ,  Barry M. Trager ,  Shmuel Winograd ,  Ali El-Zein

IPC分类号： G06F17/50

CPC分类号： G06F17/504

摘要： In one exemplary embodiment of the invention, a method includes: receiving a first description for a circuit whose operation over a plurality of inputs is to be verified; receiving a second description for expected behavior of the circuit, where the expected behavior in the second description is expressed as a set of algebraic systems of multivariable polynomials over at least one Galois field; applying at least one computational algebraic geometry technique to a combination of the first description and the second description to determine whether the circuit is verified, where verification of the circuit confirms that at least one output obtained based on the first description corresponds to at least one expected value based on the expected behavior expressed in the second description; and outputting an indication as to whether the circuit is verified.

摘要翻译： 在本发明的一个示例性实施例中，一种方法包括：接收对要对其进行验证的多个输入的操作的电路的第一描述; 接收对所述电路的预期行为的第二描述，其中所述第二描述中的预期行为被表示为在至少一个伽罗瓦域上的多变量多项式的代数系统集合; 将至少一个计算代数几何技术应用于第一描述和第二描述的组合以确定电路是否被验证，其中电路的验证确认基于第一描述获得的至少一个输出对应于至少一个预期的 基于在第二描述中表达的预期行为的价值; 并且输出关于电路是否被验证的指示。

公开(公告)号：US20120278774A1

公开(公告)日：2012-11-01

申请号：US13097193

申请日：2011-04-29

申请人： Viresh Paruthi ,  Peter Anthony Sandon ,  Jun Sawada

发明人： Viresh Paruthi ,  Peter Anthony Sandon ,  Jun Sawada

IPC分类号： G06F17/50

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个连续循环的该属性成立后的下一个周期的属性是否成立的情况下执行无假设的诱导。 产生使用通过没有假设的感应的被测硬件设计的属性的感应证明。

公开(公告)号：US08185852B2

公开(公告)日：2012-05-22

申请号：US12047361

申请日：2008-03-13

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

摘要： A method for performing verification is disclosed. The method includes selecting a set of gates to add to a first localization netlist and forming a refinement netlist. A min-cut is computed with sinks having one or more gates in the refinement netlist and sources comprising one or more inputs of an original netlist and one or more registers registers of the original netlist which are not part of the refinement netlist. A final localized netlist is obtained by adding one or more gates to the refinement netlist to grow the refinement netlist until reaching one or more cut-gates of the min-cut.

摘要翻译： 公开了一种用于执行验证的方法。 该方法包括选择一组门以添加到第一定位网表并形成细化网表。 使用在细化网表中具有一个或多个门的信宿和包括原始网表的一个或多个输入和不属于细化网表的原始网表的一个或多个寄存器寄存器的源来计算最小值。 通过将一个或多个门添加到细化网表来获得最终的本地化网表，以增加细化网表，直到达到最小切割的一个或多个切割点。

公开(公告)号：US08042075B2

公开(公告)日：2011-10-18

申请号：US12410962

申请日：2009-03-25

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

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

IPC分类号： G06F9/45 ,  G06F9/455 ,  G06F17/50

CPC分类号： G06F17/5022

摘要： Methods, systems and computer products are provided for reducing the design size of an integrated circuit while preserving the behavior of the design with respect to verification results. A multiplexer is inserted at the gate being analyzed, and the multiplexer selector is controlled to provide a predetermined output for one frame at the point being analyzed. It is then determined whether the circuit remains equivalent during application of the predetermined output in order to decide whether the gate being analyzed is a candidate for replacement.

摘要翻译： 提供了方法，系统和计算机产品，用于减少集成电路的设计尺寸，同时保持设计相对于验证结果的行为。 在被分析的门处插入复用器，并且多路复用器选择器被控制以在被分析的点处为一帧提供预定的输出。 然后在应用预定输出期间确定电路是否保持等效，以便确定被分析的门是否是替换候选。