Cadence Design Systems, Inc.

Evgueni Goldberg

Felice Balarin

Kanupriya Gulati

Yakov Novikov

An improved method and mechanism for verification of an electrical circuit design is provided. The method and system simultaneously provides the coverage advantage of formal verification with the scaling efficiencies of simulation. In one approach, the method and system generates an intelligent set of test vectors off a resolution proof. The intelligent set of test vectors can be used to simulate the circuit design for complete coverage without having to test the entire set of possible variable assignments for the CNF formula corresponding to the circuit design.

Method and mechanism for performing simulation off resolution proof

An improved method and mechanism for designing and verifying an electrical circuit design is provided using an improved SAT-solver which uses complete assignments and systematic local search to provides improved performance. In one approach, the sat-solver maintains a complete assignment that is changed one variable at a time. A variable is fixed within the falsified set of clauses.

Method and mechanism for using systematic local search for SAT solving

A method of synthesis of a second circuit (N) that is toggle equivalent to a first circuit (N), comprising building up Nin topological order, starting from the input side of N, by producing a sequence of subcircuit designs Nthrough N, such that output toggling of circuit Nimplies output toggling of subcircuit Nfor every i=1, . . , k; and output toggling of Nstrictly implies output toggling of Nif i&#x3c;j.

Toggle equivalence preserving logic synthesis

A method and an apparatus to perform logic synthesis preserving high-level specification and to check that a common specification (CS) of two circuits is correct have been disclosed. In one embodiment, the method includes building a circuit Nthat preserves a predefined specification of a circuit N. In some embodiments, the method includes verifying that Nand Nindeed implement the same specification and so they are functionally equivalent.

Systems, methods, and apparatus to perform logic synthesis preserving high-level specification

A method and system for solving satisfiability problems is disclosed. In one embodiment, clauses in a satisfiability problem are organized as a chronologically ordered stack. In another embodiment, the activity of each variable in the satisfiability problem is monitored. An activity counter is maintained for each variable and is incremented each time the variable appears in a clause used in generating a conflict clause. In an embodiment, a branching variable is selected from among the variables in the top clause of the stack when the top clause is a conflict clause. In a further embodiment, one or more conflict clauses in the stack are removed when the search tree is abandoned. In a still further embodiment, the value assigned to a branching variable is selected for purposes of having a uniform distribution of positive and negative literals.

Growing community of inventors

Berkeley, CA, United States of America

Evgueni Goldberg