公开(公告)号：US06308299B1

公开(公告)日：2001-10-23

申请号：US09118199

申请日：1998-07-17

申请人： Jerry R. Burch ,  Vigyan Singhal

发明人： Jerry R. Burch ,  Vigyan Singhal

IPC分类号： G06F1750

CPC分类号： G06F17/504

摘要： A method and system for combinational verification tightly integrates multiple verification methods. The present invention performs random simulation on the inputs of two combinational netlists. The nets within the netlists are described as BDDs and divided into classes of cutpoint candidates based upon the signatures produced by the random simulation. Cutpoint candidates within each class are resolved to determine whether the candidates are equivalent. If the nets are likely to be equivalent, BDD composition is performed on the nets. Otherwise, SAT-based analysis is performed on the nets. If either method fails to resolve the cutpoints within an allocated amount of time or resources, then the other method is invoked and information learned by the first method is passed to the second method to assist in the resolution. This process repeats until the cutpoint candidates are resolved. If the cutpoint resolution produces a true negative, then the candidate classes are refined by performing directed simulation on the inputs of the netlists using the witness to the true negative generated by the cutpoint resolution. This directed simulation produces new candidate classes that are resolved as described above. If, after the cutpoint classes are refined, the outputs are in a different class, then the netlists are unequal. If a false negative is found after the cutpoints are resolved, a new cutpoint is created. If the outputs are in the current class, then the two netlists are equal. Otherwise, the cutpoints are further resolved as described above.

摘要翻译： 组合验证的方法和系统将多种验证方法相结合。 本发明对两个组合网表的输入进行随机模拟。 网表中的网络被描述为BDD，并且基于随机模拟产生的签名被划分成等级的候选点。 解决每个类别中的切入点候选人，以确定候选人是否等同。 如果网络可能相当，BDD组合就在网络上执行。 否则，在网络上执行基于SAT的分析。 如果任一方法无法在分配的时间或资源中解析切点，则调用另一种方法，并将第一种方法学习的信息传递给第二种方法以协助解析。 这个过程重复，直到临界点被解决。 如果切点分辨率产生真正的负数，则通过使用对切分点分辨率产生的真实负数的证人对网表的输入执行定向模拟来改进候选类。 该定向仿真产生如上所述解析的新候选类。 如果在精简分类后，输出处于不同的类，那么网表不平等。 如果在切割点解决后发现假阴性，则会创建一个新的切点。 如果输出在当前类中，则两个网表相等。 否则，如上所述进一步解析切点。

公开(公告)号：US06247163B1

公开(公告)日：2001-06-12

申请号：US09172708

申请日：1998-10-13

申请人： Jerry R. Burch ,  Vigyan Singhal

发明人： Jerry R. Burch ,  Vigyan Singhal

IPC分类号： G06F1560

CPC分类号： G06F17/504

摘要： A method and system of latch mapping for performing combinational equivalence checking on a specification and an implementation of a circuit that does not depend on signal names or circuit structure to determine the latch mapping. First, every latch is mapped to every other latch. Then, the resulting mapping is refined until it is semi-inductive. The refinement is performed by randomly producing a state that satisfies the mapping and applying a random input vector to the circuits. The resulting mappings are iteratively compared and new input vectors are applied to the circuits until the greatest fixed point of the refinement is found. Then, it is determined whether the greatest fixed point of refinement forces output equality. If the greatest fixed point does not force output equality, then a bug in a combinational block of the implementation is localized through an interactive procedure. If the greatest fixed point does force output equality, then it is determined whether it also satisfies a reset condition. If implementation latches are not mapped together, then conformance with the reset condition is guaranteed. Otherwise, conformance can be guaranteed only if the implementation latches mapped together are assumed to have the same value in the reset state. The method and system is also extended to cover ternary latch mappings having “don't care” conditions.

摘要翻译： 一种锁存映射的方法和系统，用于对不依赖于信号名称或电路结构的电路的规范和实现进行组合等价检查，以确定锁存器映射。 首先，每个锁存器映射到每隔一个锁存器。 然后，所得到的映射被改进，直到它是半归纳。 通过随机产生满足映射并将随机输入向量应用于电路的状态来进行细化。 迭代地比较所得到的映射，并且将新的输入向量应用于电路，直到发现细化的最大定点。 然后，确定最大固定点的精确力是否输出相等。 如果最大的固定点不强制输出相等，那么实现的组合块中的错误通过交互式过程进行本地化。 如果最大的固定点强制输出相等，则确定它是否也满足复位条件。 如果实现锁存器未映射到一起，则保证符合复位条件。 否则，只有在映射到一起的实现锁存器在复位状态下被假定为具有相同的值时，才能保证一致性。 该方法和系统也被扩展到覆盖具有“无关紧要”条件的三进制锁存器映射。

公开(公告)号：US07895552B1

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

申请号：US11092994

申请日：2005-03-28

申请人： Vigyan Singhal ,  Soe Myint ,  Chung-Wah Norris Ip ,  Howard Wong-Toi

发明人： Vigyan Singhal ,  Soe Myint ,  Chung-Wah Norris Ip ,  Howard Wong-Toi

IPC分类号： G06F17/50

CPC分类号： G06F17/504

摘要： In the field of functional verification of digital designs in systems that use an abstraction for portions of a circuit design to perform the verification proof, a tool is described for resolving inconsistencies between the design and abstractions for the design. The tool provides information to a user about intermediate steps in the verification process. In response, the user may provide insight about the design to allow the tool to adjust the verification analysis of the design. The information provided to the user, including possible conflicts between the design and its abstractions, may include visualization techniques to facilitate the user's understating of any inconsistencies.

摘要翻译： 在使用电路设计部分的抽象来执行验证证明的系统中的数字设计的功能验证领域中，描述了用于解决设计和设计抽象之间不一致的工具。 该工具向用户提供有关验证过程中的中间步骤的信息。 作为响应，用户可以提供关于设计的洞察，以允许工具调整设计的验证分析。 提供给用户的信息，包括设计与其抽象之间可能的冲突，可能包括可视化技术，以便于用户低估任何不一致之处。

公开(公告)号：US20090119631A1

公开(公告)日：2009-05-07

申请号：US12265657

申请日：2008-11-05

申请人： Jordi Cortadella ,  Vigyan Singhal ,  Emre Tuncer

发明人： Jordi Cortadella ,  Vigyan Singhal ,  Emre Tuncer

IPC分类号： G06F17/50

CPC分类号： H03L7/00 ,  G06F17/505 ,  G06F2217/14 ,  H03K19/20

摘要： A system for automatically transforming a given synchronous circuit description into an equivalent and provably correct desynchronized circuit description. Included in the automated transformation are techniques for synthesizing a variability-aware controller using a two-phase protocol, techniques for synthesizing a variability-aware controller using gated clocks and testability circuits, techniques for synthesizing a variability-aware controller optimized for performance, techniques for initializing the synthesized controller, techniques for dynamically minimizing power requirements, and techniques for interfacing the desynchronized circuit with external synchronous circuits. Also disclosed are techniques for implementing a system for automatically transforming a synchronous circuit description into an equivalent and provably correct desynchronized circuit description within the context of an electronic design automation design flow. Exemplary circuits used in the application of the aforementioned techniques are provided. Application of mathematical models and techniques used for proving equivalence between the input description and the resulting desynchronized circuit are presented and explained.

摘要翻译： 用于将给定的同步电路描述自动变换为等效且可证明的正确的非同步电路描述的系统。 包括在自动变换中的技术是使用两相协议合成可变性感知控制器的技术，使用门控时钟和可测试性电路合成可变性感知控制器的技术，用于合成针对性能优化的可变性感知控制器的技术 初始化合成控制器，用于动态最小化功率需求的技术，以及将失步电路与外部同步电路接口的技术。 还公开了用于实现用于在电子设计自动化设计流程的上下文中将同步电路描述自动变换为等同且可证明的正确的不同步电路描述的系统的技术。 提供了在上述技术的应用中使用的示例性电路。 介绍并解释了用于证明输入描述和所得到的非同步电路之间等价性的数学模型和技术的应用。

公开(公告)号：US20090116597A1

公开(公告)日：2009-05-07

申请号：US12265620

申请日：2008-11-05

申请人： Jordi Cortadella ,  Vigyan Singhal ,  Emre Tuncer ,  Luciano Lavagno

发明人： Jordi Cortadella ,  Vigyan Singhal ,  Emre Tuncer ,  Luciano Lavagno

IPC分类号： H04B1/00 ,  H04L7/00

CPC分类号： H03L7/00 ,  G06F17/505 ,  G06F2217/14 ,  H03K19/20

摘要： A system for automatically transforming a given synchronous circuit description into an equivalent and provably correct desynchronized circuit description. Included in the automated transformation are techniques for synthesizing a variability-aware controller using a two-phase protocol, techniques for synthesizing a variability-aware controller using gated clocks and testability circuits, techniques for synthesizing a variability-aware controller optimized for performance, techniques for initializing the synthesized controller, techniques for dynamically minimizing power requirements, and techniques for interfacing the desynchronized circuit with external synchronous circuits. Also disclosed are techniques for implementing a system for automatically transforming a synchronous circuit description into an equivalent and provably correct desynchronized circuit description within the context of an electronic design automation design flow. Exemplary circuits used in the application of the aforementioned techniques are provided. Application of mathematical models and techniques used for proving equivalence between the input description and the resulting desynchronized circuit are presented and explained.

摘要翻译： 用于将给定的同步电路描述自动变换为等效且可证明的正确的非同步电路描述的系统。 包括在自动变换中的技术是使用两相协议合成可变性感知控制器的技术，使用门控时钟和可测试性电路合成可变性感知控制器的技术，用于合成针对性能优化的可变性感知控制器的技术 初始化合成控制器，用于动态最小化功率需求的技术，以及将失步电路与外部同步电路接口的技术。 还公开了用于实现用于在电子设计自动化设计流程的上下文中将同步电路描述自动变换为等同且可证明的正确的不同步电路描述的系统的技术。 提供了在上述技术的应用中使用的示例性电路。 介绍并解释了用于证明输入描述和所得到的非同步电路之间等价性的数学模型和技术的应用。

公开(公告)号：US20090115469A1

公开(公告)日：2009-05-07

申请号：US12265571

申请日：2008-11-05

申请人： Jordi Cortadella ,  Vigyan Singhal ,  Emre Tuncer

发明人： Jordi Cortadella ,  Vigyan Singhal ,  Emre Tuncer

IPC分类号： H03L7/00

CPC分类号： H03L7/00 ,  G06F17/505 ,  G06F2217/14 ,  H03K19/20

摘要： A system for automatically transforming a given synchronous circuit description into an equivalent and provably correct desynchronized circuit description. Included in the automated transformation are techniques for synthesizing a variability-aware controller using a two-phase protocol, techniques for synthesizing a variability-aware controller using gated clocks and testability circuits, techniques for synthesizing a variability-aware controller optimized for performance, techniques for initializing the synthesized controller, techniques for dynamically minimizing power requirements, and techniques for interfacing the desynchronized circuit with external synchronous circuits. Also disclosed are techniques for implementing a system for automatically transforming a synchronous circuit description into an equivalent and provably correct desynchronized circuit description within the context of an electronic design automation design flow. Exemplary circuits used in the application of the aforementioned techniques are provided. Application of mathematical models and techniques used for proving equivalence between the input description and the resulting desynchronized circuit are presented and explained.

摘要翻译： 用于将给定的同步电路描述自动变换为等效且可证明的正确的非同步电路描述的系统。 包括在自动变换中的技术是使用两相协议合成可变性感知控制器的技术，使用门控时钟和可测试性电路合成可变性感知控制器的技术，用于合成针对性能优化的可变性感知控制器的技术 初始化合成控制器，用于动态最小化功率需求的技术，以及将失步电路与外部同步电路接口的技术。 还公开了用于实现用于在电子设计自动化设计流程的上下文中将同步电路描述自动变换为等同且可证明的正确的不同步电路描述的系统的技术。 提供了在上述技术的应用中使用的示例性电路。 介绍并解释了用于证明输入描述和所得到的非同步电路之间等价性的数学模型和技术的应用。

公开(公告)号：US07412674B1

公开(公告)日：2008-08-12

申请号：US11089851

申请日：2005-03-24

申请人： Vigyan Singhal ,  Brajesh Arora ,  Yann Antonioli

发明人： Vigyan Singhal ,  Brajesh Arora ,  Yann Antonioli

IPC分类号： G06F17/50

CPC分类号： G06F17/504

摘要： A method and apparatus for measuring the progress of a formal verification process using an analysis region, and measures the effectiveness of the current set of properties/requirements in verifying different portions of logic within the design. The present invention applies the concept of analysis region to analyze the properties/requirements for a design. The analysis region can be expanded or contracted either manually or automatically based upon the results of the analysis. The present invention generates a visual display that is available to the user that represents the amount of source code in the analysis region for a given property or multiple properties in comparison to the maximum possible analysis region. The present invention can display this information in a bar graph format, on a line-by-line basis for the source code and on a waveform display, for example.

摘要翻译： 一种用于测量使用分析区域的形式验证过程的进度的方法和装置，并且测量在验证设计中的逻辑的不同部分的当前属性/要求集合的有效性。 本发明应用分析区域的概念来分析设计的性质/要求。 分析区域可以根据分析结果手动或自动扩展或收缩。 与最大可能分析区域相比，本发明生成可用于表示给定属性或多个属性的分析区域中的源代码量的用户的视觉显示。 例如，本发明可以以条形图格式，逐行显示源代码和波形显示。

公开(公告)号：US20090115503A1

公开(公告)日：2009-05-07

申请号：US12265585

申请日：2008-11-05

申请人： Jordi Cortadella ,  Vigyan Singhal ,  Emre Tuncer ,  Luciano Lavagno

发明人： Jordi Cortadella ,  Vigyan Singhal ,  Emre Tuncer ,  Luciano Lavagno

IPC分类号： G05F1/10

CPC分类号： H03L7/00 ,  G06F17/505 ,  G06F2217/14 ,  H03K19/20

摘要： A system for automatically transforming a given synchronous circuit description into an equivalent and provably correct desynchronized circuit description. Included in the automated transformation are techniques for synthesizing a variability-aware controller using a two-phase protocol, techniques for synthesizing a variability-aware controller using gated clocks and testability circuits, techniques for synthesizing a variability-aware controller optimized for performance, techniques for initializing the synthesized controller, techniques for dynamically minimizing power requirements, and techniques for interfacing the desynchronized circuit with external synchronous circuits. Also disclosed are techniques for implementing a system for automatically transforming a synchronous circuit description into an equivalent and provably correct desynchronized circuit description within the context of an electronic design automation design flow. Exemplary circuits used in the application of the aforementioned techniques are provided. Application of mathematical models and techniques used for proving equivalence between the input description and the resulting desynchronized circuit are presented and explained.

摘要翻译： 用于将给定的同步电路描述自动变换为等效且可证明的正确的非同步电路描述的系统。 包括在自动变换中的技术是使用两相协议合成可变性感知控制器的技术，使用门控时钟和可测试性电路合成可变性感知控制器的技术，用于合成针对性能优化的可变性感知控制器的技术 初始化合成控制器，用于动态最小化功率需求的技术，以及将失步电路与外部同步电路接口的技术。 还公开了用于实现用于在电子设计自动化设计流程的上下文中将同步电路描述自动变换为等同且可证明的正确的不同步电路描述的系统的技术。 提供了在上述技术的应用中使用的示例性电路。 介绍并解释了用于证明输入描述和所得到的非同步电路之间等价性的数学模型和技术的应用。

公开(公告)号：US07418678B1

公开(公告)日：2008-08-26

申请号：US10909099

申请日：2004-07-29

申请人： Chung-Wah N Ip ,  Lawrence Loh ,  Vigyan Singhal ,  Howard Wong-Toi

发明人： Chung-Wah N Ip ,  Lawrence Loh ,  Vigyan Singhal ,  Howard Wong-Toi

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

CPC分类号： G06F17/504 ,  G06F17/5022

摘要： A counter abstraction tool generates an abstraction model for one or more counters in a circuit design for use with a formal verification system. The tool detects the presence of a counter in a circuit design, identifies one or more special values for the counter, and creates an abstraction for the counter. The tool can automatically perform the abstraction, guide a user in configuring the appropriate abstraction for the counter, or perform a combination of automatic and manual abstraction. The tool may further accommodate related counters.

摘要翻译： 计数器抽象工具为电路设计中的一个或多个计数器生成抽象模型，以便与形式验证系统一起使用。 该工具检测电路设计中存在计数器，识别计数器的一个或多个特殊值，并为计数器创建抽象。 该工具可以自动执行抽象，指导用户配置计数器的适当抽象，或执行自动和手动抽象的组合。 该工具可以进一步容纳相关的计数器。

公开(公告)号：US07020856B2

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

申请号：US10389316

申请日：2003-03-14

申请人： Vigyan Singhal ,  Joseph E. Higgins

发明人： Vigyan Singhal ,  Joseph E. Higgins

IPC分类号： G06F17/50

CPC分类号： G06F17/504

摘要： Methodology for verifying properties of a circuit model in context of given environmental constraints is disclosed. Verification of a specified property is performed by analyzing only a portion of the circuit model. The present methodology is also directed towards reducing the computation time for verifying the specified property. Further, the present methodology allows the connection of an additional circuit model to the circuit model in a non-intrusive manner. The connection is made without making any modifications to the description of the circuit model. This permits the straightforward specification of related environmental constraints and properties, which makes it possible to verify correct behavior of complex interfaces.