Patent ID: 8365114

Claim:
A method, comprising: recognizing two circuits, an original and a modified circuit, wherein said original circuit has a first logic and said modified circuit has a second logic, which said second logic comprises at least one desired logic change relative to said first logic, wherein both said circuits have logic gates, have inputs, and are capable to accept and propagate vectors and to produce outputs; detecting an equivalence line in said original circuit by using Combinatorial Equivalence Checking (CEC), wherein said first and second logic are equivalent from said inputs to said equivalence line; by using a computer, finding at least one point of change amongst said logic gates that are neighboring said equivalence line by Boolean Satisfiability (SAT) techniques involving Conjunctive Normal Form (CNF) Clauses of said logic gates that are neighboring said equivalence line together with said outputs of said two circuits, and combining said CNF clauses with selector Boolean variables, wherein setting to true any one of said selector Boolean variables allows for individual determination of whether one of said logic gates that are neighboring said equivalence line is amongst said at least one point of change, and limiting how many of said selector Boolean variables are simultaneously set to true, wherein said at least one point of change is potentially suitable for implementing said at least one desired logic change for said first logic, and wherein said at least one point of change has logic values; accepting said at least one point of change as at least one verified point of change if an observability condition is fulfilled, wherein said at least one verified point of change is suitable for implementing said at least one desired logic change, and wherein said observability condition is fulfilled if, for every said vector for which said outputs of said original and modified circuits differ, at least one of said logic values of said at least one point of change propagate to said output of said original circuit; and deriving a substitute logic for said at least one verified point of change in such manner that said second logic replaces said first logic in said original circuit.