公开(公告)号：US06993730B1

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

申请号：US09758524

申请日：2001-01-10

申请人： Joseph E. Higgins ,  Vigyan Singhal ,  Adnan Aziz

发明人： Joseph E. Higgins ,  Vigyan Singhal ,  Adnan Aziz

IPC分类号： G06F17/50

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

摘要： This invention determines whether two circuit models have equivalent functionality. The method allows very fast comparison between two circuits taking advantage of previous work done. Whenever an apparatus associated with the method solves a problem, it stores information that learned during the solution of the problem, in a database. If the apparatus is presented with a new problem of determining equivalence between two portions of two circuits, it checks if it has seen sub-circuits similar to either of the two pieces before. If it has, it uses the knowledge cached during the previous checks to make the new check easier. Checking equivalence of two circuit models involves checking equivalence of many pairs of sub-parts. Even when the subsequent comparisons involve different circuits, it is possible to take advantage of the information acquired during previous equivalence checks.

摘要翻译： 本发明确定两个电路模型是否具有相同的功能。 该方法允许利用先前工作完成的两个电路之间的非常快速的比较。 每当与该方法相关联的装置解决问题时，它将在解决问题期间学习的信息存储在数据库中。 如果设备呈现出确定两个电路两部分之间的等效性的新问题，则检查它是否已经看到类似于之前的两个部分之一的子电路。 如果有的话，它会使用先前检查过程中缓存的知识来使新检查变得更容易。 检查两个电路模型的等效性涉及检查多对子部件的等效性。 即使随后的比较涉及不同的电路，也可以利用在先前的等价检查期间获得的信息。

公开(公告)号：US06611947B1

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

申请号：US09644767

申请日：2000-08-23

申请人： Joseph E. Higgins ,  Vigyan Singhal ,  Adnan Aziz

发明人： Joseph E. Higgins ,  Vigyan Singhal ,  Adnan Aziz

IPC分类号： G06F1750

CPC分类号： G06F17/504

摘要： This invention determines whether two logic level circuit models have equivalent functionality. The method allows difficult portions of the equivalent functionality check to be partitioned and concurrently solved in a distributed computing environment. This permits the user to use, in a scalable fashion, additional computing resources to rapidly solve difficult equivalent functionality checks. The method allows difficult checks to be solved using (1) a divide-and-conquer approach, (2) by a competitive approach in which many independent attempts are made to solve the same check, or (3) by allocating more resources to solve the difficult check.

摘要翻译： 本发明确定两个逻辑电平电路模型是否具有相同的功能。 该方法允许等同功能检查的困难部分在分布式计算环境中进行分区并同时解决。 这允许用户以可扩展的方式使用额外的计算资源来快速地解决困难的等效功能检查。 该方法允许使用（1）分治方法来解决困难的检查，（2）通过竞争方法，其中许多独立尝试来解决相同的检查，或者（3）通过分配更多的资源来解决 困难的检查。

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

公开(公告)号：US07137078B2

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

申请号：US10401315

申请日：2003-03-27

申请人： Vigyan Singhal ,  Joseph E. Higgins ,  Alok N. Singh

发明人： Vigyan Singhal ,  Joseph E. Higgins ,  Alok N. Singh

IPC分类号： G06F17/50

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

摘要： A highlighting system for use with electronic circuit design tools is provided for displaying signal waveforms and Register Transfer Logic (RTL) source code portions corresponding to a selected signal in the same window. The user selects a time and signal to be explored. Based on the selected time and signal, the values of all related signals are identified from a database generated by simulation of RTL source code. Nodes corresponding to the related signals are identified from a gate-level netlist corresponding to the RTL source code and the nodes responsible for the particular value of the selected signal at selected time are identified. The nodes are then mapped on to the RTL source code portions by a process of Instrumentation. The RTL source code portions so identified are then displayed. In particular, the portions of the RTL source code responsible for the particular value or transition in particular value of the signal at the selected time are highlighted.

摘要翻译： 提供了一种用于电子电路设计工具的突出显示系统，用于在同一窗口中显示对应于选定信号的信号波形和寄存器传输逻辑（RTL）源代码部分。 用户选择要探索的时间和信号。 根据所选择的时间和信号，从通过RTL源代码的仿真生成的数据库中识别所有相关信号的值。 从对应于RTL源代码的门级网表识别对应于相关信号的节点，并且识别在选定时间负责所选信号的特定值的节点。 然后通过Instrumentation的过程将节点映射到RTL源代码部分。 然后显示如此识别的RTL源代码部分。 特别地，突出显示负责特定值或在选定时间的信号的特定值转换的RTL源代码的部分。

公开(公告)号：US07065726B1

公开(公告)日：2006-06-20

申请号：US10606419

申请日：2003-06-26

申请人： Vigyan Singhal ,  Joseph E. Higgins ,  Chung-Wah Norris Ip ,  Howard Wong-Toi

发明人： Vigyan Singhal ,  Joseph E. Higgins ,  Chung-Wah Norris Ip ,  Howard Wong-Toi

IPC分类号： G06F17/50

CPC分类号： G06F17/504

摘要： The present invention is used for guiding formal verification of a circuit design in circuit simulation software to optimize the time required for verification of a circuit design. The invention modifies the analysis region being used for verification in order to optimize the time for verification. The invention allows for manual, semi-automatic, and automatic modification of the analysis region. The modification is done by either expanding or reducing the analysis region or by adding new rules as assumptions to the existing analysis region. The invention also uses the concept of an articulation point for modification of the analysis region. The modification of the analysis region is performed in a manner to optimize time and memory required for verification of the circuit design.

摘要翻译： 本发明用于指导电路仿真软件中电路设计的形式验证，以优化电路设计验证所需的时间。 本发明修改了用于验证的分析区域，以优化验证时间。 本发明允许分析区域的手动，半自动和自动修改。 修改是通过扩展或减少分析区域或通过添加新规则作为现有分析区域的假设来完成的。 本发明还使用用于修改分析区域的关节点的概念。 分析区域的修改以优化验证电路设计所需的时间和存储器的方式来执行。

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

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