Jasper Design Automation, Inc.

Synopsys, Inc.

Soe Myint

Chung-Wah Norris Ip

Lawrence Loh

Vigyan Singhal

Howard Wong-Toi

Rajarshi Mukherjee

Dhiraj Goswami

Ngai Ngai William Hung

Methods and apparatuses are described for identifying inconsistent constraints. During operation, a system can receive a set of constraints, wherein each constraint is defined over one or more random variables from a set of random variables. If an inconsistency or conflict is detected while solving the set of constraints, the system can identify a phase in a series of phases of the constraint solver where the inconsistency was detected. The system can then try to solve different subsets of the set of constraints to identify smaller subsets of the set of constraints that contain the inconsistency. When the system tries to solve a subset of the set of constraints, the system can determine whether or not an inconsistency is detected in the identified phase while solving the subset of the set of constraints. Next, the system can report the smallest subset of inconsistent constraints that was found to a user.

Identifying inconsistent constraints

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

A system and method for identifying, for a selected signal, those signals whose value is relevantly determined based upon a value of the selected signal, where a set of signals to be examined is identified as those signals that satisfy one or more of the following criteria: (1) they are RTL load signals of the selected signal, (2) they are RTL load signals that are also in an analysis region, (3) they are RTL load signals within the analysis region that also contribute to a proof target, and/or 4) they are RTL load signals that contribute to the proof target. In one embodiment of the present invention the selected signal at a selected time step relevantly determines a target signal at an associated time step if one of the following items is true: (1) if the value of the selected signal at the selected time step changes (from 0 to 1 or from 1 to 0), the value of the target signal must change, or (2) if the value of the selected signal does not change, the value of the target signal at its associated time step cannot change regardless of how the rest of the inputs to the logic driving the target signal changes. Another embodiment of the present invention, the selected signal at the selected time step relevantly determines a target signal at an associated time step if the value of the selected signal at the selected time step were different then the value of the target signal at the associated time step would be different.

System and method for determining and identifying signals that are relevantly determined by a selected signal in a circuit design

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.

Growing community of inventors

Santa Clara, CA, United States of America

Soe Myint