Patent ID: 7003739

Claim:
A method for finding an optimal unification substitution for formulas in a technology library during integrated circuit design, comprising steps of: (a) receiving input, said input including a list L of pairs of formulas in standard form, a set S of substitutions for variables, a right part e(x 1 , . . . , x p ) of an identity, and an information I={t, h, r, a, p} on best application; (b) when said list L is not empty, extracting and removing first pair (ƒ′(A′ 1 , . . . , A′ n′ ), g′(B′ 1 , . . . , B′ m′ )) from said list L; (c) removing head inverters and buffers from formulas ƒ′(A′ 1 , . . . , A′ n′ ) and g′(B′ 1 , . . . , B′ m′ )) and obtaining a pair (ƒ(A 1 , . . . , A n ), g(B 1 , . . . , B m )); (d) when said ƒ is a commutative operation but neither a variable nor constant, and when heads of said formulas ƒ(A 1 , . . . , A n ) and g(B 1 , . . . , B m ) are equal, searching for a basic argument A j of said formula ƒ(A 1 , . . . , A n ); (e) when said 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 said P, making copy L′ of said list L and making copy S′ of said set S; and (g) forming a reduced pair (A′, B′) for pairs (ƒ(A 1 , . . . , A n ), ƒ(B 1 , . . . , B n )) and (A j , B i ) and adding said pairs (A j , B i ) and (A′, B′) to said list L′.