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

An apparatus for finding an optimal unification substitution for formulas in a technology library during integrated circuit design, comprising:

• (a) means for 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(x1, . . . , xp) of an identity, and an information I={t, h, r, a, p} on best application;
• (b) when said list L is not empty, means for extracting and removing first pair (ƒ′(A′1, . . . , A′n′), g′(B′1, . . . , B′m′)) from said list L;
• (c) means for removing head inverters and buffers from formulas ƒ′(A′1, . . . , A′n′) and g′(B′1, . . . , B′m′)) and means for obtaining a pair (ƒ(A1, . . . , An), g(B1, . . . , Bm));
• (d) when said ƒ is a commutative operation but neither a variable nor constant, and when heads of said formulas ƒ(A1, . . . , An) and g(B1, . . . , Bm) are equal, means for searching for a basic argument Aj of said formula ƒ(A1, . . . , An);
• (e) when said basic argument Aj is found, means for letting P be head of said Aj and means for setting i=1;
• (f) when head of Bi is equal to said P, means for making copy L′ of said list L and means for making copy S′ of said set S;
• and
• (g) means for forming a reduced pair (A′, B′) for pairs (ƒ(A1, . . . , An), ƒ(B1, . . . , Bn)) and (Aj, Bi) and means for adding said pairs (Aj, Bi) and (A′, B′) to said list L′.

A computer-readable medium having computer-executable instructions for performing a method for finding an optimal unification substitution for formulas in a technology library during integrated circuit design, said method 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(x1, . . . , xp) 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 f′(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 (ƒ(A1, . . . , An), g(B1, . . . , Bm));
• (d) when said ƒ is a commutative operation but neither a variable nor constant, and when heads of said formulas ƒ(A1, . . . , An) and g(B1, . . . , Bm) are equal, searching for a basic argument Aj of said formula ƒ(A1, . . . , An);
• (e) when said basic argument Aj is found, leffing P be head of said Aj and setting i=1;
• (f) when head of Bi 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 (ƒ(A1, . . . , An), ƒ(B1, . . . , Bn)) and (Aj, Bi) and adding said pairs (Aj, Bi) and (A′, B′) to said list L′.