Intel Corporation

Cadence Design Systems, Inc.

Jasper Design Automation, Inc.

Ziyad Hanna

Habeeb Farah

John Moondanos

Zurab Khasidashvili

Rajeev Kumar Ranjan

Rajdeep Mukherjee

Benjamin Meng-Ching Chen

Ross M Weber

Lars Lundgren

Kathryn Drews Kranen

Asa Ben-Tzur

Carl Seger

Chung-Wah Norris Ip

Alexander Levin

Lawrence Loh

Ravi Prakash

Craig Franklin Deaton

Björn Håkan Hjort

Daher Kaiss

Per Anders M Franzén

Alexander Nadel

Amit Palti

Alexander Novakovsky

Shy Shyman

Per Anders M Franzen

The present disclosure relates to a method for use in a formal verification of an electronic design. Embodiments may include receiving, using a processor, a reference model including a software specification and an implementation model at a register transfer level. Embodiments may also include generating one or more invariants based upon, at least in part, the reference model, wherein generating one or more invariants includes applying a semantic analysis. Embodiments may further include automatically generating at least one case splitting candidate based upon, at least in part, the one or more generated invariants.

System, method, and computer program product for automatically inferring case-split hints in equivalence checking of an electronic design

The present disclosure relates to a computer-implemented method for use in a formal verification of an electronic design. Embodiments may include receiving a reference model including a software specification, an implementation model at a register transfer level, and a property that analyzes equivalence between the reference model and the implementation model. The method may further include generating one or more case split hints based upon the reference model, that may be used to decompose the design state space into smaller partitions and performing an abstraction operation on a portion of design logic associated with one or more partitions in order to eliminate design elements that are irrelevant to a particular property. Embodiments may also include performing model checking on the abstract models to determine their accuracy.

System, method, and computer program product for sequential equivalence checking in formal verification

The present disclosure relates to a method for use in a formal verification of an electronic design. Embodiments may include receiving, using a processor, a specification model associated with an electronic design and generating, using a parser, an intermediate representation based upon, at least in part, the specification model. Embodiments may also include applying a machine generated semantic preserving program transformation to the intermediate representation to create a semantically transformed specification model and synthesizing the semantically transformed specification model to generate a formal verification model.

System, method, and computer program product for generating a formal verification model

Tools for ranking of generated properties are described. A plurality of circuit design properties are generated from a signal trace of the circuit design. A static analysis of the circuit design properties is performed against one or more circuit design constraints to determine whether the properties are true. Rankings for the circuit design properties are determined responsive to results of the static analysis. The ranking for a circuit design property represents a value of the circuit design property in validating correct functionality of the circuit design. At least some of the circuit design properties are presented in a user interface responsive to the rankings for the circuit design properties.

Functional property ranking

A model checking tool, which is used to test a circuit design, attempts to reach a target state from an initial state in the state-space of the circuit design using one or more intermediate states. Through an iterative process, the tool identifies intermediate states in the state-space of the circuit design that are used to generate starting states for subsequent iterations of the process. The intermediate states help to restrict the scope of the state-space search to reduce the time and memory requirements needed to reach the target state. The model checking tool also explores the state-space in parallel from a subset of computed restart states, which reduces the possibility of bypassing any essential intermediate or target states.

Guided exploration of circuit design states

A computer-implemented method and non-transitory computer readable medium for circuit design verification. Formal verification is performed on a circuit design to prove a correctness of a property of the circuit design. The circuit design has a cone of influence representing a portion of the circuit design capable of affecting signals of the property. A proof core of the circuit design is identified, the proof core being a portion of the cone of influence that is sufficient to prove the correctness of the property. A coverage metric is generated that is indicative of a level of formal verification coverage provided by the property based on the proof core of the circuit design.

Formal verification coverage metrics for circuit design properties

A computer-implemented method and non-transitory computer readable medium for circuit design verification. A property defined for a circuit design is received, the property having a cone of influence in the circuit design corresponding to a portion of the circuit design capable of affecting the property. Bounded reachability analysis is performed for the circuit design against a set of cover items. The set of cover items are classified into classified cover items based on results of the reachability analysis. Coverage information is generated indicating an amount of formal verification coverage provided by the property. The coverage information is generated based on a first set of the classified cover items that correspond to the cone of influence of the property and that are reached within a particular bound during the reachability analysis.

Formal verification coverage metrics of covered events for circuit design properties

The result of a property based formal verification analysis of a circuit design may include at least one counterexample for each property that is violated, which a user can use to debug the circuit design. To assist the user in this debugging process, a debugging tool applies one or more soft constraints to a counterexample trace that simplify the appearance of the trace when displayed as a waveform. The debugging tool thus facilitates a user's understanding of what parts of the counterexample trace are responsible for the property failure. Also described is a power analysis tool that increases the noise level of a trace for a circuit design in order to facilitate analysis of the circuit design's power characteristics.

Constraining traces in formal verification

A simultaneous satisfiability algorithm, or SSAT, allows simultaneous checks to be made efficiently for a number of literals, x, . . . ,xwhether xis true under any satisfying assignments of a formula (written in conjunctive normal form) built from the variables of these literals and other variables (or, equivalently whether xis a logical consequence of the formula). Thus, several related satisfiability checks are performed simultaneously in SSAT. Temporal induction algorithms allow the verification of the sequential behavior of finite state machines, e.g., hardware. Temporal induction algorithms may employ a SSAT solver to perform simultaneous model checking of several invariant (or safety) properties efficiently. These SSAT-based temporal induction algorithms are double-incremental, such that all learned clauses in the SSAT solver are re-used both across verified properties as well as across time frames.

Verification using simultaneous and inductive SAT algorithms

An approach for cut-point frontier selection and/or counter-example generation. Both a lazy and an eager cut-point frontier are identified. A reconvergence (or non-reconvergence) ratio is then computed for each of the frontiers and the one with the smaller (larger) reconvergence (non-reconvergence) ratio is selected as the next cut-point frontier. For another aspect, to generate a counter-example, in response to identifying a difference in output signals for a given cut-point frontier, values of eigenvariables and reconverging primary inputs are used to compute the corresponding values of the non-reconverging primary inputs. These corresponding values are then computed to be compatible with the internal signal values implied by the cut-point frontier selections that were made to expose the difference in the outputs.

Method and apparatus for cut-point frontier selection and for counter-example generation in formal equivalence verification

A method for facilitating the sequential verification of loop-free circuits by reducing the sequential verification problem to combinational verification, by constructing and comparing Timed Binary Decision. Diagrams (TBDDs) and Timed Binary Expression Diagrams (TBEDs). The TBEDs can be compared by using both BDDs and SAT solvers.

Application of the retimed normal form to the formal equivalence verification of abstract RTL descriptions for pipelined designs

A device, system and method for analysis of Very Large Scale Integration circuit designs. A computing platform may, for example, find one or more loops in a circuit design, functionally analyze the loops, and extract one or more Register-Transfer-level logical elements in relation to the analysis result. A computing platform may, for example, identify a group of at least one Channel Connected Sub-Network that forms at least one combinational loop, generate overall zero-delay collapsed functionality on an output of said group, identify one or more functional parts that form said group, and replace the group with one or more corresponding logically equivalent Register-Transfer-level devices.

Growing community of inventors

Haifa, Israel

Ziyad Hanna