Jasper Design Automation, Inc.

Cadence Design Systems, Inc.

Esilicon Corporation

Elastix Corporation

Tempus Fugit, Inc.

Vigyan Singhal

Chung-Wah Norris Ip

Howard Wong-Toi

Joseph E Higgins

Lawrence Loh

Emre Tuncer

Jordi Cortadella

Soe Myint

Adnan Aziz

Jerry R Burch

Luciano Lavagno

Yann Alain Antonioli

Brajesh Arora

Alok N Singh

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.

Variability-aware scheme for high-performance asynchronous circuit voltage regulation

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.

Extracting, visualizing, and acting on inconsistencies between a circuit design and its abstraction

Variability-aware scheme for asynchronous circuit initialization

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.

Managing formal verification complexity of designs with multiple related counters

Managing formal verification complexity of designs with counters

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.

System and method for measuring progress for formal verification of a design using analysis region

The present invention is directed to a system and a method for verifying properties of a circuit model while providing information to help the user manually modify a design analysis region and/or environmental constraints. While conventional systems attempt to substantially automate the entire formal verification process, the present invention iteratively provides information to the user about the cost and effect of changes to the environmental constraints and the analysis region. This information enables the user to weigh the effectiveness and efficiency of one or more modifications to the design analysis area and/or to the environmental constraints (assumptions). The information provided to the user can help a user compare a variety of alternative modifications in order to select the modifications that are efficient and effective. In addition, the information can provide alternatives along with the cost and effect of each alternative to the user who otherwise did not identify these alternatives, thus the invention can help the user by identifying suggestions that the user may not have otherwise considered. The present invention then receives information from the user to modify the design analysis area and/or the environmental constraints and will analyze the design with these modified parameters.

System and method for identifying design efficiency and effectiveness parameters for verifying properties of a circuit model

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.

Trace based method for design navigation

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.

System and method for guiding and optimizing formal verification for a circuit design

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.

Method for verifying properties of a circuit model

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.

Method for rapidly determining the functional equivalence between two circuit models

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 ( ) a divide-and-conquer approach, ( ) by a competitive approach in which many independent attempts are made to solve the same check, or ( ) by allocating more resources to solve the difficult check.

Method for determining the functional equivalence between two circuit models in a distributed computing environment

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.

Method and system for combinational verification having tight integration of verification techniques

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 &ldquo;don't care&rdquo; conditions.

Growing community of inventors

Fremont, CA, United States of America

Vigyan Singhal