Cadence Design Systems, Inc.

Vinaya Kumar Singh

Amir Lehavot

Axel Siegfried Scherer

Jose Barandiaran

Joezac John Zachariah

Tarun Garg

Ravi Prakash

Alok Jain

Kavita Ravi

Jun Yuan

Manpreet Singh Reehal

Pratik Mahajan

Akok Jain

Mohamad Shaved

The present disclosure relates to a method for avoiding deadends in a constrained simulation. The method may include analyzing a first deadend during a simulation and a first constraint of the simulation. The method may further include determining if the first constraint causes the first deadend. If the first constraint causes the first deadend, the method may also include defining a first lookahead constraint corresponding to the first constraint. The method may additionally include rerunning a first previous cycle in the simulation while adding the first lookahead constraint to the simulation.

Adaptive deadend avoidance in constrained simulation

An automated debugging method and system for over-constrained circuit verification environment are described. Useful information related to circuit evaluation and/or over-constrained event is collected and provided. The information may include: clock cycles at which an over-constrained event occurs; identification of a minimum subset of constraints that will cause an over-constrained event to occur; signal ports having an associated signal that can not switch between different signal states; whether a triggering signal event has occurred during the evaluation; indicating whether constraints in the evaluation are realizable, etc. Novel approaches for detecting and obtaining the useful information also are described.

Automated debugging method for over-constrained circuit verification environment

Automated debugging method and system for over-constrained circuit verification environment

Method for providing information associated with an over-constrained event in verification of a circuit design

Method for checking a status of a signal port to identify an over-constrained event

A method and system for implementing context aware synthesis of assertions is disclosed. The method and system for assertion synthesis includes converting an assertion formula to sequence implication form using semantic preserving rewrite rules, performing optimizations on the resulting formula to reduce the number of state-bits in a final FSM (Finite State Machine), and synthesizing the resulting formula to the final FSM using context aware sequence synthesis.

Method and system for implementing context aware synthesis of assertions

A method and system for handling assertion libraries in verification of a design are disclosed. The method and system include structuring and implementing at least one verification component in at least one of the assertion libraries with at least one standard assertion language supported by at least one verification tool, creating an assertion library element for a specific requirement for verification of the design without dependence on the at least one verification tool for the assertion library element, and resolving assertion status. With the disclosed method and system, visualization of assertion status at various levels of design hierarchy and at verification component level may be achieved, and implementing verification techniques may include optimization techniques during and/or after verification.

Method and system for handling assertion libraries in functional verification

Aspects of computing design invariants, by using approximate reachability analysis, include reducing the circuit model for verification and synthesis. Further included is computing invariants using approximate reachability analysis to optimize a circuit model by identifying a plurality of next states for a present state, the plurality of next states capable of being reached from the present state in one transition. The plurality of bits of the next states are compared with a plurality of bits of the present state, and each bit of the present state that is different from at least one next state is changed to variant.

Design optimization using approximate reachability analysis

The disclosure presents a formulation to support simulatable subset (also known as 'simple-subset') of a property specification language. This method is applicable for model checking and simulation. In this formulation, the 'simple-subset' is transformed to a set of basic formulas. Verification engines are required to support the basic formula only. The basic formula is a form of automata in the property specification language. This is called SERE implication. The efficiency of verification is dependent on size of automata. Miscellaneous opportunistic rules are applied to optimize SERE implication formulas.

Transformation of simple subset of PSL into SERE implication formulas for verification with model checking and simulation engines using semantic preserving rewrite rules

Growing community of inventors

Noida, India

Vinaya Kumar Singh