Method and apparatus for finding optimal unification substitution for formulas in technology library

摘要

The present invention is directed to a method and apparatus to find an optimal unification substitution for formulas in a technology library. In an exemplary aspect of the present invention, a method for finding an optimal unification substitution for formulas in a technology library during integrated circuit design may include the following steps: (a) receiving input including a list L of pairs of formulas in standard form, a set S of substitutions for variables, a right part e(x₁, . . . , x_p) of an identity, and an information I={t, h, r, a, p} on best application; (b) when the list L is not empty, extracting and removing first pair (f′(A′₁, . . . , A′_n′), g′(B′₁, . . . , B′_m′)) from the list L; (c) removing head inverters and buffers from formulas f′(A′₁, . . . , A′_n′) and g′(B′₁, . . . , B′_m′)) and obtaining a pair (f(A₁, . . . , A_n), g(B₁, . . . , B_m)); (d) when the ƒ is a commutative operation but neither a variable nor constant, and when heads of the formulas f(A₁, . . . , A_n) and g(B₁, . . . , B_m) are equal, searching for a basic argument A_j of the formula f(A₁, . . . , A_n); (e) when the basic argument A_j is found, letting P be head of said A_j and setting i=1; (f) when head of B_i is equal to the P, making copy L′ of the list L and making copy S′ of the set S; and (g) forming a reduced pair (A′, B′) for pairs (f(A₁, . . . , A_n), f(B₁, . . . , B_n)) and (A_j, B_i) and adding the pairs (A_j, B_i) and (A′, B′) to the list L′.