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

Abstract

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