ИСТИНА

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.sub.1, . . . , x.sub.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'.sub.1, . . . , A'.sub.n'), g'(B'.sub.1, . . . , B'.sub.m')) from the list L; (c) removing head inverters and buffers from formulas f'(A'.sub.1, . . . , A'.sub.n') and g'(B'.sub.1, . . . , B'.sub.m')) and obtaining a pair (f(A.sub.1, . . . , A.sub.n), g(B.sub.1, . . . , B.sub.m)); (d) when the f is a commutative operation but neither a variable nor constant, and when heads of the formulas f(A.sub.1, . . . , A.sub.n) and g(B.sub.1, . . . , B.sub.m) are equal, searching for a basic argument A.sub.j of the formula f(A.sub.1, . . . , A.sub.n); (e) when the basic argument A.sub.j is found, letting P be head of said A.sub.j and setting i=1; (f) when head of B.sub.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.sub.1, . . . , A.sub.n), f(B.sub.1, . . . , B.sub.n)) and (A.sub.j, B.sub.i) and adding the pairs (A.sub.j, B.sub.i) and (A', B') to the list L'.