Evgueni I Goldberg

7380226, May 27, 2008

Dec 29, 2004

11/027085

Evgueni I. Goldberg - Berkeley CA, US

Cadence Design Systems, Inc. - San Jose CA

G06F 17/50

716 5, 716 1, 716 2, 716 4, 716 7, 716 10, 703 14, 703 19

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.

7600211, Oct 6, 2009

Sep 25, 2006

11/527198

Evgueni Goldberg - Berkeley CA, US
Kanupriya Gulati - College Station TX, US

Cadence Design Systems, Inc. - San Jose CA

G06F 17/50

716 18, 716 1, 716 3, 716 4, 716 5, 716 7

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

7610570, Oct 27, 2009

Apr 19, 2006

11/407864

Evgueni Goldberg - El Cerrito CA, US

Cadence Design Systems, Inc. - San Jose CA

G06F 17/50

716 5, 716 3, 716 4

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.

7853903, Dec 14, 2010

Apr 3, 2006

11/397230

Evgueni Goldberg - Berkeley CA, US
Felice Balarin - Berkelely CA, US

Cadence Design Systems, Inc. - San Jose CA

G06F 17/50

716 4, 716 5, 703 14

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.

8438513, May 7, 2013

Dec 30, 2011

13/341564

Evgueni I. Goldberg - Boston MA, US
Panagiotis Manolios - Sharon MA, US

Northeastern University - Boston MA

G06F 17/50

716106, 716101, 716104, 716132

A new method is presented for eliminating existential quantifiers from a Boolean CNF (Conjunctive Normal Form) formula. This new method designs circuits by solving a quantifier elimination problem (QEP) by using derivation of dependency sequents (DDS). This new method begins with a first quantified conjunctive normal form formula, determines dependency sequents for the left branch and the right branch of a branching variable, resolves dependency sequents derived in both branches, and designs a circuit using a current formula having less variables than the first quantified conjunctive normal formula. Utility of this method includes verification, in particular, determining reachability of a state of a design.

7356519, Apr 8, 2008

Feb 27, 2004

10/789810

Evgueni Goldberg - Berkeley CA, US
Yakov Novikov - Minsk, BY

Cadence Design Systems, Inc. - San Jose CA

G06F 17/00

706 45, 706 12, 706 19, 706 21

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.